About us
Espace utilisateur
INSTN offers more than 40 diplomas from operator level to post-graduate degree level. 30% of our students are international students.
Professionnal development
Professionnal development
Find a training course
INSTN delivers off-the-self or tailor-made training courses to support the operational excellence of your talents.
Human capital solutions
At INSTN, we are committed to providing our partners with the best human capital solutions to develop and deliver safe & sustainable projects.
Home   /   Thesis   /   Advanced type-based static analysis for operating system verification

Advanced type-based static analysis for operating system verification

Computer science and software Cyber security : hardware and sofware Engineering sciences Technological challenges


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.


Département Ingénierie Logiciels et Systèmes (LIST)
Laboratoire pour la Sûreté du Logiciel
Top envelopegraduation-hatlicensebookuserusersmap-markercalendar-fullbubblecrossmenuarrow-down