I research the use of program logics to formally reason about capability machines. I investigate how to use capability machines to provably and efficiently enforce various security properties.
In particular, I use the Iris framework to mechanically prove deep semantic properties of capability machines. These properties range from local state encapsulation to stack safety properties.
Check out our Coq mechanization project Cerise!
Efficient and Provable Local Capability Revocation using Uninitialized Capabilities
Aïna Linn Georges, Armaël Guéneau, Thomas Van Strydonck, Amin Timany, Alix Trieu, Sander Huyghebaert, Dominique Devriese, Lars Birkedal
In POPL 2021: ACM SIGPLAN Symposium on Principles of Programming Languages
pdf Coq development
Le Temps des Cerises: Efficient Temporal Stack Safety on Capability Machines using Directed Capabilities [Technical Report]
Aïna Linn Georges, Alix Trieu, Lars Birkedal
Passed the qualifying exam - January 27, 2021