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.
