Paper Info
Title
Clean-Slate Development of Certified OS Kernels
Abstract
The CertiKOS project at Yale aims to develop new language-based technologies for building large-scale certified system software. Initially, we thought that verifying an OS kernel would require new program logics and powerful proof automation tools, but it should not be much different from standard Hoare-style program verification. After several years of trials and errors, we have decided to take a different path from the one we originally planned. We now believe that building large-scale certified system software requires a fundamental shift in the way we design the underlying programming languages, program logics, and proof assistants. In this talk, I outline our new clean-slate approach, explain its rationale, and describe various lessons and insights based on our experience with the development of several new certified OS kernels.
Year
DOI
Venue
2015
10.1145/2676724.2693180
CPP
Keywords
Field
DocType
horizontal composition,correctness proofs,program verification.,abstraction layer,vertical composition,formal methods,certified os kernels
System software,Trial and error,Programming language,Computer science,Program logic,Algorithm,Automation,Os kernel,Constructed language,Abstraction layer,Certification
Conference
Citations 
PageRank 
References 
1
0.36
17
Authors
1
Name
Order
Citations
PageRank
Zhong Shao189768.80