You are here

High assurance hardware state machine trusted computing base



OBJECTIVE: Cybersecurity systems need to take advantage of high assurance provided by state machines used for aviation and safety critical systems. Offeror shall research a high assurance state machine trusted computing base for a high assurance operating system. 

DESCRIPTION: Safety critical systems use state machines to achieve high computer security assurance levels. State machines make security reviews for EAL6 or higher tractable. Current generation aviation systems were not developed with strong computer security requirements. Past cyber threats, [1]-[2], current cyber treats, Spectre [3] and Meltdown [4], and future cyber treats need to be countered. Embedded system designs are typically based on commodity hardware optimized exclusively for speed – leading to critical cyber vulnerabilities that can have devastating effects on safety and mission effectiveness. This has also led to the unsustainable “Perimeter, Patch, Pray” Information Assurance strategy [5] that is simply impractical for fielded aviation and missile systems. We are interested in researching a separation kernel-like operating system consisting of a hardware state machine as the trusted computing base and a high assurance operating system. In terms of computer virtualization concepts: the trusted computing base is a hardware state machine and the OS can be compared to a guest operating system. Recent developments in the open source hardware and software communities have created the open source RISC-V [6] and OpenPiton [7] microprocessors and high assurance open source operating system, seL4 [8]. Open source architectures provide for more thorough security reviews compared to closed source systems [9]. Open source architectures also provide for lower life cycle system cost. We are interested in leveraging the open source communities for this research topic area. Preference will be given for open source hardware and operating system modules. 

PHASE I: For the Phase I proposal, offeror shall describe the feasibility of using a hardware and software co-design to create a high assurance state machine as the trusted computing base for a high assurance operating system. (1) Propose high assurance state machine trusted computing base concept. (2) Propose an operating system to take advantage of trusted computing base. (3) Propose a system architecture describing: hardware, microprocessor, state machine, operating system, and application software. (4) Describe the cybersecurity advantages of (3) over current commodity microprocessors and operating systems. (5) A plan to achieve a cybersecurity security rating of at least EAL6. (6) Describe potential Army, medical, and commercial applications; and (7) Provide a business model to market the proposed system. For the phase I effort, the offeror shall demonstrate the feasibility and security benefits of creating a high assurance hardware state machine trusted computing base and high assurance OS. (1) Develop models, simulations, prototypes, etc. to determine technical feasibility of developing a high assurance system (2) Deliver a System Architecture and Description Report; and (3) Deliver an EAL Certification Plan Report. 

PHASE II: Offeror shall develop a high assurance computer system based on offeror’s proposal and phase I effort. It is highly recommended that the offeror team with a government prime contractor. The offeror shall demonstrate high assurance computer system running an Army application (like Joint Multi-Role Technology Demonstrator [19]). The Offer shall propose potential applications for a system demonstration and implement an application with government concurrence. Offeror shall deliver a year 1 report and a year 2 report describing artifacts, documents, verification tests, etc. completed following the plan in the Phase I document EAL Certification Plan Report. Offeror shall deliver 2 prototype systems to the government point of contact for test and evaluation with all software tools and licenses (if required) to build and use the system. Offeror shall provide 2 days of on-site training for the system. 

PHASE III: Offeror will develop and market high assurance system based on phase II development work and marketing plan from phase I. Offeror will achieve EAL6 or greater for high assurance computer system. Offeror will integrate high assurance hardware/OS system into an Army Aviation or Missile subsystem currently under development or via technology refresh. 


1: [1] S. King, et al.: "SubVirt: implementing malware with virtual machines," IEEE Symposium on Security and Privacy, pp. 1-14, 21-24 May 2006.

2:  R. Fannon: An analysis of hardware-assisted virtual machine based rootkits, Thesis, Naval Postgraduate School, June 2014.

3:  .G. Klein., et al.: "seL4: formal verification of an OS kernel," Proceedings of the ACM SIGOPS 22nd symposium on Operating systems principles, Big Sky, Montana, pp. 207-220, October 11 - 14, 2009.

4:  M. Lipp, et al.: "Meltdown," Cornel University Library, 3 Jan 2018.

5:  Darpa: "Baking Hack Resistance Directly into Hardware," 4/10/2017.

6:  A. Waterman, et. al. "The RISC-V Compressed Instruction Set Manual Version 1.9 (draft)" (PDF). RISC-V.


8:  8: G. Klein., et al.: "seL4: formal verification of an OS kernel,"Proceedings of the ACM SIGOPS 22nd symposium on Operating systems principles, Big Sky, Montana, pp. 207-220, October 11 - 14, 2009.

9:  9: R. Smith, "A Contemporary Look at Saltzer and Schroeder's 1975 Design Principles", IEEE Security & Privacy, Vol. 10, No. 5, pp. 20-25, Nov.-Dec. 2012

10:  10: P. Jungwirth, et al.: "Cyber defense through hardware security", Proc. SPIE 10652, Disruptive Technologies in Information Sciences, 106520P (9 May 2018)

11:  doi: 10.1117/12.2302805


13:  11: T. Nakano: "Hardware Implementation of a Real-time Operating System," IEEE TRON Project International Symposium, Tokyo, Japan, pp. 34-42, 28 Nov - 2 Dec 1995

14:  12:

15:  13: M. McCoyd, et al.: "Building a Hypervisor on a Formally Verifiable Protection Layer,"

16:  DARPA, "Clean-slate design of Resilient, Adaptive, Secure Hosts (CRASH)," DARPA-BAA-10-70, June 2010.

17:  15: J. Alves-Foss,et al.: A New Operating System for Security Tagged Architecture Hardware In Support of Multiple Independent Levels of Security (MILS) Compliant Systems, University of Idaho, Center Secure and Dependable Systems, Air Force Research Lab Tech Report AFRL-RI-RS-TR-2014-088, APRIL 2014.

18:  16: J. Song, and J. Alves-Foss. "Security tagging for a zero-kernel operating system." System Sciences (HICSS), 2013 46th Hawaii International Conference on. IEEE, 2013.

19:  R. Shioya, et al.: "Low-Overhead Architecture for Security Tag," IEEE Pacific Rim International Symposium on Dependable Computing, pp. 135-142, Shanghai, China, 16-18 Nov. 2009

20:  18: P.Jungwirth, et al.: "Hardware Security Kernel for Cyber Defense," SPIE Defense + Security Conference, Baltimore, MD, April 2019.


KEYWORDS: Assurance, Cyber Resilience, Embedded Systems, Trusted Computing, State Machine 

US Flag An Official Website of the United States Government