Building Certified Concurrent OS Kernels.
Operating system (OS) kernels form the backbone of system software. They can have a significant impact on the resilience and security of today’s computers. Recent efforts have demonstrated the feasibility of formally verifying simple general-purpose kernels, but they have ignored the important issue...
| Published in: | Communications of the ACM Vol. 62; no. 10; pp. 89 - 100 |
|---|---|
| Main Authors: | , , , , , , , |
| Format: | Article |
| Published: |
Association for Computing Machinery
Oct2019
|
| Subjects: | |
| Online Access: | View this record in EBSCOhost |
| fields | @attributes: recordID: 1 pdfLink: plink: https://search.ebscohost.com/login.aspx?direct=true&db=hlh&AN=138800269&site=ehost-live header: @attributes: shortDbName: hlh uiTerm: 138800269 longDbName: Humanities International Complete uiTag: AN controlInfo: bkinfo: jinfo: jid: 00010782 ACM jtl: Communications of the ACM issn: 00010782 maglogo: N pubinfo: dt: Oct2019 vid: 62 iid: 10 pid: 68 pub: Association for Computing Machinery artinfo: ui: 138800269 10.1145/3356903 ppf: 89 ppct: 11 formats: tig: atl: Building Certified Concurrent OS Kernels. aug: au: Ronghui Gu Zhong Shao Hao Chen Jieung Kim Jérémie Koenig Xiongnan (Newman) Wu Sjöberg, Vilhelm Costanzo, David affil: Columbia University, New York, NY, USA. Yale University, New Haven, CT, USA. CertiK, Cambridge, MA, USA. su: Kernel operating systems Computer multitasking Computer security Software frameworks Computer programming sug: subj: Kernel operating systems Computer multitasking Computer security Software frameworks Computer programming ab: Operating system (OS) kernels form the backbone of system software. They can have a significant impact on the resilience and security of today’s computers. Recent efforts have demonstrated the feasibility of formally verifying simple general-purpose kernels, but they have ignored the important issues of concurrency, which include not just user and I/O concurrency on a single core, but also multicore parallelism with fine-grained locking. In this work, we present CertiKOS, a novel compositional framework for building verified concurrent OS kernels. Concurrency allows interleaved execution of programs belonging to different abstraction layers and running on different CPUs/threads. Each such layer can have a different set of observable events. In CertiKOS, these layers and their observable events can be formally specified, and each module can then be verified at the abstraction level it belongs to. To link all the verified pieces together, CertiKOS enforces a so-called contextual refinement property for every such piece, which states that the implementation will behave like its specification under any concurrent context with any valid interleaving. Using CertiKOS, we have successfully developed a practical concurrent OS kernel, called mC2, and built the formal proofs of its correctness in Coq. The mC2 kernel is written in 6500 lines of C and x86 assembly and runs on stock x86 multicore machines. To our knowledge, this is the first correctness proof of a general-purpose concurrent OS kernel with fine-grained locking. pubtype: Periodical doctype: Article src: R language: English refInfo: copyright: @attributes: flag: Y dt: @attributes: year: 2019 holdings: @attributes: islocal: N |
|---|