Advanced type-based static analysis for operating system verification

Job description: 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 DeepL.com (free version)

Your profile: 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.