Skip to main content

TS

Formal verification at scale

Authors

Gerwin Klein, June Andronick, Ihor Kuz, Toby Murray, Gernot Heiser and Matthew Fernandez

DATA61

Intel

Abstract

We present a method for building specific classes of provably trustworthy systems with minimal proof effort. The method concentrates proof effort at the architecture level, providing security and correctness theorems at the binary level. We illustrate how this method can be applied not only to building new systems but also to retrofitting existing systems, such as the mission computer of an autonomous helicopter. We build on the verified seL4 microkernel, exploit its strong security mechanisms to enforce software component boundaries, and use a component-based approach with automatic code/proof co-generation to enforce system-level security and correct kernel configuration. After the initial investment into kernel verification and component framework verification, the proofs for such systems can be almost entirely automatic.

BibTeX Entry

  @article{Klein_AKMHF_toappear,
    publisher        = {ACM},
    author           = {Klein, Gerwin and Andronick, June and Kuz, Ihor and Murray, Toby and Heiser, Gernot and Fernandez,
                        Matthew},
    note             = {(to appear)},
    year             = {0},
    title            = {Formal Verification at Scale},
    type             = {Journal Article - Refereed},
    journal          = {Communications of the ACM}
  }

Download

Served by Apache on Linux on seL4.