Isolation Techniques for Untrusted Software

Our project addresses the problem of simultaneous achievement of safety, security, and performance. The study we propose will elicit a better understanding of the implicit trade-offs between the three and explore a promising path forward to optimize all three on a modern computer platform. Our approach is an implementation of the ARINC 653 software partitioning standard as our separation kernel, developed using the open source virtualization technology of the Xen hypervisor and a Linux-based privileged domain 0. For the feasibility study of Phase 1, we target a core set of features (an Agile story) encompassing the CPU scheduler as a key part of the separation kernel. This feature set is analyzed using formal methods with the Isabelle proof assistant. Security is evaluated under the rigor of the Common Criteria, while the safety assurance of this approach is evaluated through a rigorous audit under the DO-178B flight certification standard (with an actual FAA Designated Engineering Representative). In addition, performance is assessed through a hybrid HW/SW measurement technique.