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.