See the list of all my publications

PhD: Automatic Verification of tasks schedulers

The defense version of my manuscript and of my slides are available online.

Abstract

The aim of this thesis is the verification of task schedulers for operating systems through static analysis based on abstract interpretation. Operating systems are collections of software present on almost every computer. Their purpose is to allow other programs to run without having to manage low-level problems such as memory. Due to this central role, operating systems have become critical components of IT infrastructures: any error in the operating system can have consequences on other programs, potentially causing the entire computer to crash.

One component at the core of an operating system is the task scheduler. This component is responsible for determining, according to a predefined policy, which task can execute at what time. These components use unbounded dynamic data-structures to store the necessary elements for their operation. These data-structures allow elements to be easily moved between them. Verifying a task scheduler requires designing an analysis capable of accurately representing these data-structures and their contents.

The first part of this thesis describes a toy imperative language that explicitly manipulates memory. We then provide the concrete semantics of this language, followed by a presentation of a numerical static analysis to determine the range of numerical variables and a shape analysis capable of reasoning about unbounded inductive data-structures.

The second part is devoted to presenting a relational abstract domain capable of reasoning about symbolic sequences. This domain expresses constraints on the contents of these sequences, such as their lengths, extreme values, and sorted characteristics.

The third part presents the combination of the shape analysis described in the first part with the sequence domain. This combination enhances the expressiveness of the analysis. It is now capable of proving the partial functional correctness of complex algorithms, such as sorting algorithms on lists or binary trees, as well as list libraries drawn from real applications.

The final part of this thesis presents the application of the analysis to an instance of the FreeRTOS task scheduler. The first step in the verification process is formalizing the properties we seek to establish on the scheduler’s functions. The second step aims to show that the specified properties are verified by the instance’s functions using the analysis.

Internships

Detecting race conditions in the Linux Kernel using memory barriers

The Linux Kernel uses pairs of memory barriers to avoid race conditions. When a novel element is added then a value \(A\) is set before a second one \(B\). And the code uses a memory barrier to ensure that \(B\) is not assigned before \(A\). When the value \(A\) must be read, the program first checks whether \(B\) was correctly set. And a second memory barrier separates the two reads. These barriers ensure that neither the compiler nor the CPU could reorder these read/write operations.

During a 6-month internship, I worked with Baptiste Lepers at the university of Sydney on the detection of race conditions in the Linux kernel using incorrectly matched memory barriers.

See (Lepers et al., 2023) for more details.

Precise analysis of finite state machine in the Astrée analyzer

Critical systems, like those used in cars or aircraft, utilize finite state machines to model control and command functions. These systems are also required to be proven free of “crashs” (formally, undefined behavior). To do so, abstract interpretation based static analyses over approximates the state of the program at any point. In the case of automaton, the control flow is not explicitly visible in the code. It depends on the states transition, that is to say the assignment of some variables.

During a 5-month internship at AbsInt, I extended the Astrée analyzer to take into account finite state machines. This extension is capable to detect and precisely analyse generated implementation of finite state machine by using dynamic partitioning.

See (Giet et al., 2019) for more details.

Decision procedures for modal logic

During a 2-month internship at ISAE-Supaéro under the direction of Christophe Garion and Rémi Delmas, I implemented a generic satisfiability solver for the K-Modal logic. I later extended it to prove satisfiability of a family of epistemic logics.

See (Delmas et al., 2018) for more details (article in french).

Bibliography