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):

Report Date:

2015-06-01

Pagination or Media Count:

503.0

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.

Subject Categories:

  • Computer Programming and Software
  • Computer Systems

Distribution Statement:

APPROVED FOR PUBLIC RELEASE