Advanced Development of Certified OS Kernels

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.

Open PDF

Document Details

Document Type
Technical Report
Publication Date
Jun 01, 2015
Accession Number
ADA622345

Entities

People

  • Zhong Shao

Organizations

  • Yale University

Tags

Communities of Interest

  • C4I
  • Cyber
  • Engineered Resilient Systems

DTIC Thesaurus Topics

  • Air Force
  • Application Software
  • Computer Program Documentation
  • Computer Program Reliability
  • Computer Programming
  • Computer Programs
  • Computer Science
  • Computers
  • Kernels (Operating System)
  • Language
  • Linear Programming
  • Lists (Data Structures)
  • Microarchitecture
  • Network Protocols
  • Operating Systems
  • Programming Languages
  • System Software

Fields of Study

  • Computer science

Readers

  • Mathematical Modeling and Probability Theory.
  • Parallel and Distributed Computing.