Skip to main content


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


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

General Dynamics C4 Systems



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

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