Treffer: Advanced Development of Certified OS Kernels
Title:
Advanced Development of Certified OS Kernels
Authors:
Contributors:
YALE UNIV NEW HAVEN CT
Source:
DTIC
Publication Year:
2015
Collection:
Defense Technical Information Center: DTIC Technical Reports database
Subject Terms:
Computer Programming and Software, Computer Systems, 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, CERTIFIED SOFTWARE, CERTIFIED OS KERNELS, CERTIFIED COMPILERS, ABSTRACTION LAYERS, MODULARITY, DEEP SPECIFICATIONS, PROGRAM VERIFICATION, CERTIFIED RESOURCE BOUND ANALYSIS, CONCURRENCY, RELAY-GUARANTEE REASONING, SIMULATION AND REFINEMENT
Document Type:
Fachzeitschrift
text
File Description:
text/html
Language:
English
Availability:
Rights:
Approved for public release; distribution is unlimited.
Accession Number:
edsbas.F87D4477
Database:
BASE
Weitere Informationen
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. ; Sponsored in part by DARPA.