PLDI 2019 (series) / DeepSpec 2019 (series) / DeepSpec 2019 /
Coverage Guided, Property Based Testing
The complete formal verification of safety-critical real-time systems is highly desirable because the consequences of failures are dire (loss of lives or failure of the mission). Despite the rich literature in both the temporal reasoning of real-time systems and the formal verification of the correctness and security of OS kernels, the connection of the two still remains a challenge to this day. First of all, formalizing temporal properties at the implementation level (a mixture of C and assembly code) is non-trivial. Secondly, the temporal behavior of one component could be influenced by the rest of the system, making the temporal isolation proof difficult to compose and scale. Last but not least, the introduction of partitioned scheduling leads to more complexity in the temporal reasoning and the security proof. In this talk, we present a novel compositional framework for reasoning about temporal properties of real-time systems at the implementation level. For temporal isolation, we use virtual timeline, a variant of the supply bound function used in the real-time scheduling analysis, to connect the scheduling with concrete states of one component and to encapsulate interferences from other components. For spatial isolation, we extend the existing non-interference proof of CertiKOS to handle the preemptive setting. We also address the information flow security of partitioned scheduling, in particular the non-interference property in case of dynamic partition scheduling, which mixes both temporal and spatial isolation. Using this framework, we successfully verify a real-time OS kernel, which extends CertiKOS, a single-processor non-preemptive kernel, with a verified timer interrupt handler and a real-time scheduler. We not only prove its functional correctness but also show that this new kernel enjoys temporal and spatial isolation. All the proofs are implemented in the Coq proof assistant.
Sun 23 Jun
|15:45 - 16:15|
Chung-Kil HurSeoul National University
|16:15 - 16:45|
Leonidas LampropoulosUniversity of Pennsylvania