Seminars
View all Seminars | Download ICal for this eventVerification of a Generative Separation Kernel
Series: Ph.D (Engg.) Thesis Defence - ON-LINE
Speaker: Mr. Inzemamul Haque Ph.D Student Dept. of CSA
Date/Time: Aug 20 14:30:00
Location: On Google Meet
Faculty Advisor: Prof. Deepak D'Souza
Abstract:
In this thesis we present a technique to formally verify the
functional correctness of template-based generative systems. A
generative system is one in which a specialised system is generated
for each given input specification. In a template-based generative
system, the generated systems have a common template code, and the
components of this template are generated based on the given input
specification. Many safety-critical systems today are of this nature,
with an important class being that of separation kernels. A
separation kernel is a small specialized microkernel that provides a
sand-boxed execution environment for a given set of processes called "subjects", and are commonly used in aerospace and defence
applications.
The verification goal in the context of generative systems is to show
that for every valid input specification the generated system refines
an abstract specification that is generated according to the input
specification.
The key stepping stone in our theory is the notion of a parametric
Abstract Data Type or "machine". These are similar to classical
machines except that they have parameters on which the behaviour of
the machine depends. We propose a notion of refinement for such
machines, which we call conditional parametric refinement, which
essentially says that whenever the parameter values of the abstract
and concrete parametric machines satisfy a given condition, the
resulting machines enjoy a refinement relation. We define refinement
conditions for this notion of refinement and show that they are sound
and complete for total and deterministic machines. The refinement
conditions are similar in structure to the classical case and can be
discharged using standard Floyd-Hoare logic in a programmatic setting.
We use this framework to propose a two-step verification approach for
template-based generative systems. Such a system naturally corresponds
to a parametric machine, where the template corresponds to the
definition of operations of the machine and generated components
correspond to values for the parameters of the machine. In a similar
way we construct an abstract parametric machine whose parameter values
are generated based on the input specification. The first step of our
approach is independent of the input specification and checks that the
that the concrete parametric machine conditionally refines the
abstract parametric machine, subject to a condition C on the parameter
values generated. In the second step, which is input-specific, we check
that for a given input specification, the generated abstract and
concrete parameter values actually satisfy the condition C. Whenever
this check passes for a given input specification, we can say that the
generated system refines the abstract system. This gives us an
effective verification technique for verifying generative systems that
lies somewhere between verifying the generator and translation
validation.
We demonstrate the effectiveness of our technique by applying it to
verify the Muen Separation Kernel. Muen is an open-source
template-based generative separation kernel which uses hardware
support for virtualization to implement separation of subjects. We
chose to model the virtualization layer (in this case Intel's VT-x
layer) along with the rest of the hardware components like registers
and memory, programmatically in software. Using the templates which
Muen generator utilizes we constructed a parametric machine and
carried out the first step of conditional parametric refinement for
Muen, using the Spark Ada verification tool. This was a substantial
effort involving about 20K lines of source code and annotation. We
have also implemented a tool that automatically and efficiently
performs the Step 2 check for a given separation kernel
configuration. The tool is effective in proving the assumptions,
leading to machine-checked proofs of correctness for 16 different
input configurations, as well as in detecting issues like undeclared
sharing of memory components in some seeded faulty configurations.
Details for joining online on Google Meet:
Link: https://meet.google.com/xkj-bugw-cxf
Please note that the meeting will be recorded as per Institute
requirements. By joining the link you are giving your consent to the
recording.
Speaker Bio:
Host Faculty: