Accession Number : AD1027690

Title :   Verified OS Interface Code Synthesis

Descriptive Note : Technical Report,30 Sep 2014,29 Sep 2016


Personal Author(s) : Klein,Gerwin ; Murray,Toby ; Kumar,Ramana

Full Text :

Report Date : 01 Dec 2016

Pagination or Media Count : 38

Abstract : The outcome of the project is that they have solved some fundamental challenges, but more work is required to integrate these results into the larger proof framework of the seL4 microkernel to be directly usable in practice. Beyond the stated project goals, the solution approach required and enabled them to address a more fundamental challenge: the integration of different interactive theorem proving systems without sacrificing correctness guarantees. While again more work needs to be done to fully complete this integration in a way that is usable for a larger audience, this result means that the strong binary verification automation tools from the HOL4 theorem prover, which were used for the verified ML compiler CakeML, can now also be used in the Isabelle/HOL system that was used for the verified seL4 microkernel. This combination increases proof productivity and enables larger, more expressive systems to be verified in the future.

Descriptors :   coding , application software , compilers , automation , operating systems , instruction set architecture

Subject Categories : Computer Programming and Software

Distribution Statement : APPROVED FOR PUBLIC RELEASE