Accession Number : ADA622345


Title :   Advanced Development of Certified OS Kernels


Descriptive Note : Final rept. Sep 2010-Dec 2014


Corporate Author : YALE UNIV NEW HAVEN CT


Personal Author(s) : Shao, Zhong


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


Report Date : Jun 2015


Pagination or Media Count : 503


Abstract : The PI and his team at Yale have successfully developed (1) a clean - slate CertiKOS hypervisor kernel that runs on multicore platforms and supports Linux and ROS applications; (2) a new certified programming methodologies and tools that can verify contextual correctness, liveness, and security properties in a unified setting; (3) a fully verified single - core CertiKOS in Coq; (4) new semantics and logics for reasoning about information flow control with declassification, resource analysis, and fine-grained concurrent programs; and (5) new proof assistant language VeriML and Coq Ltac libraries.


Descriptors :   *COMPUTER LOGIC , *COMPUTER PROGRAM VERIFICATION , *KERNEL FUNCTIONS , *SOFTWARE ENGINEERING , COMPUTER NETWORK SECURITY , COMPUTER PROGRAM RELIABILITY , COMPUTERIZED SIMULATION , EXPERIMENTAL DESIGN , INFORMATION EXCHANGE , NETWORK ARCHITECTURE , NETWORK FLOWS , OPERATING SYSTEMS(COMPUTERS) , PERFORMANCE(ENGINEERING) , PROGRAMMING LANGUAGES , QUANTITATIVE ANALYSIS , REASONING , SEMANTICS


Subject Categories : Computer Programming and Software
      Computer Systems


Distribution Statement : APPROVED FOR PUBLIC RELEASE