Sun 23 Jun 2019 16:15 - 16:45 at 106B - Coinduction and Testing Chair(s): Lennart Beringer
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

Displayed time zone: Tijuana, Baja California change

15:45 - 16:45
Coinduction and TestingDeepSpec at 106B
Chair(s): Lennart Beringer Princeton University
15:45
30m
Talk
Coinductive Reasoning about Interaction Trees
DeepSpec
Chung-Kil Hur Seoul National University
16:15
30m
Talk
Coverage Guided, Property Based Testing
DeepSpec
Leonidas Lampropoulos University of Pennsylvania