LSV Seminar
The LSV seminar takes place on Tuesday at 11:00 AM. The usual location is the conference room at Pavillon des Jardins (venue). If you wish to be informed by e-mail about upcoming seminars, please contact Stéphane Le Roux and Matthias Fuegger.
The seminar is open to public and does not require any form of registration.
Seminar
Mechanized Program Verification on a Capability Machine in the Presence of Untrusted Code
- Date
- 08.12.2020, 11:00
- Place
- online
- Speaker
- Armael Gueneau (Aarhus University)
A capability machine is a kind of CPU which supports fine-grained privilege separation using capabilities (a pointer carrying a certain amount of authority). In this talk, I will present a methodology for verifying the functional correctness of capability machine programs that call (or are called by) unknown and potentially malicious code. The key aspects to the approach is a program logic for reasoning about known code, and a logical relation which provides a specification for unknown code. I will then hint at how we extend this methodology to reason about a secure calling convention enforcing a secure stack policy and the well-bracketedness of function calls. This work has been entirely mechanized in Coq using the Iris framework (https://github.com/logsem/cerise)(https://github.com/logsem/cerise-stack)