Isolation Techniques for Untrusted Software Navy SBIR FY2010.2 Sol No.: Navy SBIR FY2010.2 Topic No.: N102-184 Topic Title: Isolation Techniques for Untrusted Software Proposal No.: N102-184-0497 Firm: DornerWorks, Ltd. 3445 Lake Eastbrook SE Grand Rapids, Michigan 49546 Contact: Steven VanderLeest Phone: (616) 822-4976 Web Site: http://www.dornerworks.com Abstract: 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. Benefits: Benefits include 1) advances formal methods approaches, providing the next step towards practical viability of proof-based verification and validation of real, complex systems; 2) simultaneously integrates security, safety, and performance for the first time; 3) first known attempt to adapt an open-source hypervisor to the ARINC 653 software partitioning standard, 4) novel method of reducing cost of achieving high levels of assurance by effective targeting of source code (a profile configuration)., 5) first step towards an innovative "diff-impact " tool to provide tracking and traceability for generation of certification and assurance artifacts. This study will advance our ARLX platform, providing a sustainable, low-cost, full-featured real-time operating system, eliminating dependence on a sole proprietary source. Xen and Linux are widely supported and are familiar to many developers. ARLX's low cost also encourages innovation from smaller parties unable to afford or justify expensive commercial packages. Beyond military, aerospace, and defense applications, we anticipate commercial applications using ARINC 653 for commercial avionics applications, along with other industries that can benefit from software partitioning and separation kernels such as health care, medical devices, energy infrastructure, and financial business sectors. Return