SeminarsView all Seminars | Download ICal for this event
Verification 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
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:
Please note that the meeting will be recorded as per Institute requirements. By joining the link you are giving your consent to the recording.