Please use this identifier to cite or link to this item:

Synthesis of Verified Architectural Components for Critical Systems Hosted on a Verified Microkernel

File Size Format  
0629.pdf 366.83 kB Adobe PDF View/Open

Item Summary

Title:Synthesis of Verified Architectural Components for Critical Systems Hosted on a Verified Microkernel
Authors:Hardin, David
Keywords:Cybersecurity and Software Assurance
Date Issued:07 Jan 2020
Abstract:We describe a method and tools for the creation of formally verified components that run on the verified seL4 microkernel. This synthesis and verification environment provides a basis to create safe and secure critical systems. The mathematically proved space and time separation properties of seL4 are particularly well-suited for the miniaturised electronics of smaller, lower-cost Unmanned Aerial Vehicles (UAVs), as multiple, independent UAV applications can be hosted on a single CPU with high assurance. We illustrate our method and tools with an example that implements security-improving transformations on system architectures captured in the Architecture Analysis and Design Language (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 proofs for filters are automatically lifted to proofs of the corresponding properties on the lazy streams that model 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.
Pages/Duration:10 pages
Rights:Attribution-NonCommercial-NoDerivatives 4.0 International
Appears in Collections: Cybersecurity and Software Assurance

Please email if you need this content in ADA-compliant format.

This item is licensed under a Creative Commons License Creative Commons