Trustworthy Systems

Synthesis of verified architectural components for autonomy hosted on a verified microkernel

Authors

Konrad Slind, David Hardin, Johannes Åman Pohjola and Michael Sproul

DATA61

Rockwell Collins Advanced Technology Center

UNSW Sydney

Abstract

We describe a method and toolchain for the creation of formally verified autonomy components that run on the verified seL4 microkernel. This synthesis and verification environment provides a basis to create safe and secure autonomous systems. We illustrate our method and tools with an example that implements security-improving transformations on system architectures captured in AADL. We show how input validation filter components can be synthesized from regular expressions, and verified to meet arithmetic constraints extracted from the AADL model. Such filters comprise efficient guards on messages to/from the autonomous system. The correctness of filters are automatically lifted to proofs of the corresponding properties on the lazy streams modelling the communications of the generated seL4 threads. Finally, we guarantee that the intent of the autonomy application logic is accurately reflected in the application binary code hosted on seL4 through the use of the verified CakeML compiler.

BibTeX Entry

  @inproceedings{Slind_HAS_20,
    address          = {Grand Wilea, Hawaii},
    author           = {Slind, Konrad and Hardin, David and {\AA}man Pohjola, Johannes and Sproul, Michael},
    booktitle        = {Hawaii International Conference on System Sciences},
    date             = {2020-1-7},
    doi              = {https://doi.org/10.24251/HICSS.2020.779},
    isbn             = {9780998133133},
    month            = jan,
    pages            = {6365-6374},
    paperurl         = {https://trustworthy.systems/publications/full_text/Slind_HAS_20.pdf},
    publisher        = {ScholarSpace / AIS Electronic Library},
    title            = {Synthesis of Verified Architectural Components for Autonomy Hosted on a Verified Microkernel},
    year             = {2020}
  }

Download