Formal verification of a real-time operating system

Abstract

Errors caused by the interaction of computer systems with the physical world are hard to mitigate but errors related to the underlying software can be prevented by a more rigorous development of software code. In the context of critical systems, a failure caused by software errors could lead to consequences that are determined to be unacceptable. At the heart of a critical system, a real-time operating system is commonly found. Since the reliability of the entire system depends upon having a reliable operating system, verifying that the operating systems functions as desired is of prime interest. One solution to verify the correctness of significant properties of an existing real-time operating system microkernel (FreeRTOS) applies assisted proof checking to its formalized specification description. The experiment consists of describing real-time operating system characteristics, such as memory safety and scheduler determinism, in Separation Logic — a formal language that allows reasoning about the behaviour of the system in terms of preconditions and postconditions. Once the desired properties are defined in a formal language, a theorem can be constructed to describe the validity of such formula for the given FreeRTOS implementation. Then, by using the Coq proof assistant, a machine-checked proof that such properties hold for FreeRTOS can be carried out. By expressing safety and deterministic properties of an existing real-time operating systems and proving them correct we demonstrate that the current state-of-the-art in theorem-based formal verification, including appropriate logics and proof assistants, make it possible to provide a machine-checked proof of the specification of significant properties for FreeRTOS.