Research
I am a PhD student at the Logic and Semantics group at Aarhus University under the supervision of Professor Lars Birkedal.
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!
Publications
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
Aïna Linn Georges, Alix Trieu, Lars Birkedal
In OOPSLA 2022: Proceedings of the ACM on Programming Languages
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 submission
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
News
Passed the qualifying exam - January 27, 2021