Advanced type-based static analysis for operating system verification

  • Cyber security : hardware and sofware,
  • phD
  • CEA-List
  • Paris – Saclay
  • Level 7
  • 2024-10-01
  • LEMERRE Matthieu (DRT/DILS//LSL)

In recent work [RTAS 2021], we have demonstrated the value of static analysis guided by an advanced dependent type system for the analysis of low-level system programs, going so far as to be able to automatically verify the absence of privilege escalation in an embedded operating system kernel as a consequence of the type-safety of the kernel code. Memory management is a particularly challenging problem when analyzing system programs, or more broadly, programs written in C, and type-based analysis provides a satisfactory solution with wide applicability (e.g. data structure management code [VMCAI 2022], dynamic language runtime, performance-oriented application code, etc.). The aim of the thesis is to extend the applications that can be made of the use of type-based static analysis. [RTAS'21] No Crash, No Exploit: Automated Verification of Embedded Kernels. O. Nicole, M. Lemerre, S. Bardin, X. Rival (Best paper) [VMCAI'22] Lightweight Shape Analysis based on Physical Types, O. Nicole, M. Lemerre, X. Rival [POPL'23] SSA Translation Is an Abstract Interpretation, M. Lemerre (Distinguished paper). Translated with (free version)

Master's degree in computer science or engineering. Background in static verification/analysis, programming in OCaml, knowledge of C or assembler, would be an advantage.


Contact us

We will reply as soon as possible...