Turnstile: A High-Assurance Cross Domain Platform

Presented as part of the 2007 HCSS conference.

Abstract

Turnstile is a high-assurance cross domain platform whose initial application is as a guard accreditable to DCID 6/ PL5. The Turnstile guard is high-performance, robust, compact, and affordable. The Turnstile architecture is based on the Rockwell Collins AAMP7G microprocessor, which has achieved NSA MILS certification based in part on a formal proof of its separation kernel implemented in microcode. The Turnstile design exploits the AAMP7G’s proven partitioning capabilities to separate the core guard function from other auxiliary function (boot/configuration, audit, health monitoring, etc.), thus allowing the guard function to be independently analyzed using a combination of formal methods (SPARK,ACL2). The Turnstile architecture also includes I/O offload engines, SELinux-based single board computers connected to the AAMP7G by means o analyzable guard data mover hardware. The offload engines can host customer-developed I/O processing applications without jeopardizing the integrity of the core guard function.

This talk describes the Turnstile architecture, design, and formal analysis, as well as a typical use case.