Show simple item record

dc.contributor.advisorD'Souza, Deepak
dc.contributor.authorHaque, Inzemamul
dc.date.accessioned2020-09-02T05:15:50Z
dc.date.available2020-09-02T05:15:50Z
dc.date.submitted2020
dc.identifier.urihttps://etd.iisc.ac.in/handle/2005/4571
dc.description.abstractA Separation Kernel is a small specialized microkernel that provides a sand-boxed execution environment for a given set of processes (also called \subjects"). The subjects may communicate only via declared memory channels, and are otherwise isolated from each other. A generative separation kernel is one in which a specialized separation kernel is generated for each system con figuration. Separation kernels are typically used in safety-critical and security-critical systems in the avionics and military domains, and it is of utmost importance to have a high level of assurance regarding the correct working of the separation kernel. In this thesis we present a formal veri fication of the functional correctness of the Muen separation kernel which is representative of the class of modern separation kernels that leverage hardware virtualization support and are generative in nature. The nature of generativeness is template-based, in that the kernel is essentially based on a fixed template of code and various constant data-structures are filled-in by the kernel generator. Although there is a great deal of work in verifi cation of OS kernels in the past two decades, applying those techniques to a separation kernel like Muen becomes challenging because of its generative nature. The use of hardware virtualization support poses another challenge. We propose a veri fication framework called conditional parametric re finement to reason about the functional correctness of template-based generative systems. Conditional parametric re finement extends classical re finement to parametric programs which are programs with uninitialized variables. This is a two-step technique for parametric programs. We first perform a general verifi cation step (independent of the input spec) to verify that the parametric program re fines a parametric abstract specifi cation, assuming certain natural conditions on the parameter values (for example injectivity of the page tables) that are to be fi lled in. This first step essentially tells us that for any input speci fication P, if the parameters generated by the system generator satisfy the assumed conditions, then the generated system is correct vis-a-vis the abstract specifi cation. In the second step, which is input-speci fic, we check that for a given input speci fication, the assumptions actually hold for the generated parameter values. This gives us an effective veri fication technique for verifying generative systems. We applied this technique to verify the Muen Separation Kernal. 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. We carried out the first step of conditional parametric refi nement for Muen, using the Spark Ada veri fication tool. The effort involved about 20K lines of source code and annotation. We have also implemented a tool that automatically and effciently performs the Step 2 check for a given separation kernel con figuration. The tool is effective in proving the assumptions, leading to machine-checked proofs of correctness for 16 different input con figurations, as well as in detecting issues like undeclared sharing of memory components in some seeded faulty con figurationsen_US
dc.language.isoen_USen_US
dc.rightsI grant Indian Institute of Science the right to archive and to make available my thesis or dissertation in whole or in part in all forms of media, now hereafter known. I retain all proprietary rights, such as patent rights. I also retain the right to use in future works (such as articles or books) all or part of this thesis or dissertationen_US
dc.subjectconditional parametric re finementen_US
dc.subjectMuenen_US
dc.subjectparametric programsen_US
dc.subjectSpark Adaen_US
dc.subject.classificationResearch Subject Categories::TECHNOLOGY::Information technology::Computer science::Computer scienceen_US
dc.titleVerification of a Generative Separation Kernelen_US
dc.typeThesisen_US
dc.degree.namePhDen_US
dc.degree.levelDoctoralen_US
dc.degree.grantorIndian Institute of Scienceen_US
dc.degree.disciplineEngineeringen_US


Files in this item

This item appears in the following Collection(s)

Show simple item record