I do ✨formal methods✨

• 2024.12

  Thesis

  Defense
  "Formal specification and verification of security mechanisms for the RISC-V architecture"

  Matthieu Baty

  A big old thesis with many words and some pictures. It is about the formal verification of hardware using proof assistants.

---

• 2023.05

  Paper

  Slides

  CSF'23
  "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 Trieu

  In 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.