Séminaire en ligne, 21 octobre 2021
Pour assister à la rencontre, se rendre sur https://ent-services.ens-lyon.fr/entVisio/ choisir Chocola dans le menu déroulant, mettre son nom comme identifiant, et Bruxelles sans majuscule comme dernier champ. Autoriser les popups, et changer de navigateur au besoin.
10h: accueil et problèmes de connexion 10h15: début de l'exposé 11h15: questions et discussion 12h: adieu et problèmes de déconnexion Merci aux auditeurs de couper micro et caméra (sauf éventuellement, lorsqu'ils souhaitent poser une question). Les questions peuvent aussi être posées dans la fenêtre de chat.
En cas de problème ou de question, écrire à chocola-gestion chez ens-lyon.fr.
Programme
- 10:15 – 11:45
-
Armaël Guéneau (Aarhus)
A capability machine is a kind of CPU with hardware support for fine-grained privilege separation. Practical designs and prototypes for such machines are seeing recent development as part of the CHERI project (University of Cambridge, SRI, ARM) (cheri-cpu.org, morello-project.org), making capability machines a promising target for designing and building new software with security in mind. In this talk, I will present some of the work done at Aarhus University and KU Leuven on developing formal principles for reasoning about security properties of code running on capability machines. I will show how one can prove functional correctness of programs that interact with untrusted (and possibly malicious) code while leveraging capabilities to protect their private state. The key aspects of this methodology are a program logic for reasoning about known code, and a logical relation providing a /universal contract/ of unknown code.
The whole work has been mechanized in Coq using the Iris framework.
