I do ✨formal methods✨
Publications
-
"Formal specification and verification of security mechanisms for the RISC-V architecture"Matthieu BatyA big old thesis with many words and some pictures. It is about the formal verification of hardware using proof assistants.
-
"A generic framework to develop and verify security mechanisms at the microarchitectural level: application to control-flow integrity"Matthieu Baty, Pierre Wilke, Guillaume Hiet, Arnaud Fontaine and Alix TrieuIn which we describe our methodology for reasoning about arbitrary Kôika developments, illustrated on the implementation of a simple hardware-based shadow stack on a pipelined RISC-V processor.Not the catchiest title, I know.