Accession Number : AD1027690


Title :   Verified OS Interface Code Synthesis


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


Corporate Author : NATIONAL ICT AUSTRALIA LIMITED EVELEIGH Australia


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


Full Text : https://apps.dtic.mil/dtic/tr/fulltext/u2/1027690.pdf


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