Advanced type-based static analysis for operating system verification

In recent work [RTAS 2021], we have demonstrated the benefits of a static analysis guided for analyzing low-level system programs, going so far as to be able to automatically verify the absence to the point of being 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 difficult problem when analyzing system programs, or more broadly, programs written in C, and type-based analysis provides a satisfactory solution with wide wide applicability (e.g. data structure management code [VMCAI 2022], dynamic language runtime dynamic language runtime, performance-oriented application code, etc.). The aim of this thesis is to extend the applications that can be made of the use of type-based static analysis. type-based static analysis.