Research
I am a postdoctoral researcher at the Max Planck Institute for Software Systems under the supervision of Professor Derek Dreyer.
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 my Coq mechanization project Cerise!
Publications
Iris-Wasm: Robust and Modular Verification of WebAssembly Programs
Xiaojia Rao, Aïna Linn Georges, Maxime Legoupil, Conrad Watt, Jean Pichon-Pharabod, Philippa Gardner, Lars Birkedal
In PLDI 2023: Programming Language Design and Implementation
pdf
Coq development
Cerise: Program Verification on a Capability Machine in the Presence of Untrusted Code
Aïna Linn Georges, Armaël Guéneau, Thomas Van Strydonck, Amin Timany, Alix Trieu, Dominique Devriese, Lars Birkedal
In JACM
pdf
Coq development
Le Temps des Cerises: Efficient Temporal Stack Safety on Capability Machines using Directed Capabilities
Aïna Linn Georges, Alix Trieu, Lars Birkedal
In OOPSLA 2022: Proceedings of the ACM on Programming Languages
pdf
Coq development
Proving full-system security properties under multiple attacker models on capability machines
Thomas Van Strydonck, Aïna Linn Georges, Armaël Guéneau, Alix Trieu, Amin Timany, Frank Piessens, Lars Birkedal, Dominique Devriese
In CSF 2022: Computer Security Foundations Symposium
pdf
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