Trustworthy Systems

Mathematically verified software kernels: Raising the bar for high assurance implementations

Authors

Daniel Potts, Rene Bourquin, Leslie Andresen, June Andronick, Gerwin Klein and Gernot Heiser

General Dynamics C4 Systems

NICTA

Abstract

We assert that the use of formal methods for software verification, coupled with high assurance architectures, is now the state of the art, and therefore should ‘set the bar’ for assured solutions. This approach is ready to be applied, in support of emerging security guidance documents, for use in a broad and diverse class of applications, from control systems of drones, to multi-domain commercial-off-the-shelf (COTS) mobile devices.

BibTeX Entry

  @techreport{Potts_BAAKH_14:tr,
    address          = {Sydney, Australia},
    author           = {Potts, Daniel and Bourquin, Rene and Andresen, Leslie and Andronick, June and Klein, Gerwin and
                        Heiser, Gernot},
    institution      = {NICTA},
    issn             = {1833-9646-8257},
    keywords         = {microkernel, security, safety, common criteria, assurance},
    month            = jul,
    paperurl         = {https://trustworthy.systems/publications/nicta_full_text/8257.pdf},
    title            = {Mathematically Verified Software Kernels: Raising the Bar for High Assurance Implementations},
    year             = {2014}
  }

Download