You are here

Open Source High Assurance System


TECHNOLOGY AREA(S): Electronics 

OBJECTIVE: Current commodity computer hardware and software are proprietary. A thorough security review cannot be performed on systems with undisclosed components. Offeror shall research high assurance computer security based on a completely open hardware and software platform following Saltzer and Schroeder’s open design principles from 1975. 

DESCRIPTION: Today's Aviation systems are based on computer architectures that were not designed with security as a requirement … leading to inherent vulnerabilities in both hardware and software that add significant air worthiness and mission risk. Embedded system designs are typically based on commodity hardware optimized almost exclusively for speed – not security – leading to critical cyber vulnerabilities [1] that can have devastating effects on safety and mission effectiveness. This has also led to the unsustainable “Perimeter, Patch, Pray” Information Assurance strategy that is simply impractical for fielded aviation and missile systems. Commodity hardware is proprietary. It is difficult to impossible to perform a thorough security review, when the hardware implementation is not provided. The Illinois Malicious Processor [2] illustrates the security issues from an undisclosed design. Saltzer and Schroeder in 1975 [3] stated that the design for a secure computer system should not be “secret”. “Open design: The hardware design should not be secret. The mechanisms should not depend on the ignorance of potential attackers, but rather on the possession of specific, more easily protected, keys … ” In 1883, Kerckhoff [4] made a similar statement for secret codes: “It [the system] should not require secrecy, and it should not be a problem if it falls into enemy hands.” Current computer architectures are based on proprietary hardware and software. In terms of Saltzer and Schroeder, the design is “secret.” Proprietary hardware and software prevents a thorough security review. With a completely open hardware and software system, a thorough security review is possible. Recent developments in machine generated formal proofs provides automatic formal high assurance statements. The Army needs open hardware and software architectures that provide for high performance, rigorous security reviews, and high assurance computer security. Recent developments in the open source hardware and software communities have provided the open source microprocessor, the RISC-V [5]-[8], and a formally verified, open source operating system, seL4 (secure extended L4) [9]-[12]. RISC-V is well-established with HDL code and a complete set of software development tools. The seL4 microkernel has a 20 year development history [12]. seL4 is a microkernel with 8,700 lines of C code and 600 lines of assembly code [11]. A machine generated formal proof-of-correctness demonstrates a high computer assurance level for seL4. RISC-V and seL4 are two open source examples; offeror is free to consider other hardware and OS open source components. 

PHASE I: For the Phase I proposal, offeror shall describe the feasibility of creating a high assurance open computer hardware and software architecture based on the “open design principles” from Saltzer and Schroeder in 1975 [3]: (1) Propose open source hardware and open source OS for a high assurance system. (2) describe the project development tools; (3) provide a plan to achieve an Evaluation Assurance Level Six (EAL6) [13] or higher rating for the operating system; (4) describe potential Army Applications (Joint Multi-Role Technology Demonstrator [16]) and commercial applications; and (5) 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 open computer hardware and software architecture based on the “open design principles” from Saltzer and Schroeder in 1975 [3]. (1) Develop models, simulations, prototypes, etc. to determine technical feasibility of developing a high assurance (EAL6 [13]) computer system based on open source hardware and an open source operating system; (2) deliver an Architecture Description and Requirements Specification Report; and (3) deliver an EAL6 Certification Plan Report. 

PHASE II: Offeror shall develop a high assurance computer system based on the “open design principles” from Saltzer and Schroeder [3] and 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 (Joint Multi-Role Technology Demonstrator [16]). 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 "EAL6 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 hardware/OS system based on phase II development work and marketing plan from phase I. Offeror will achieve EAL6 [13] for high assurance computer system. Offeror will integrate high assurance hardware/OS system into an Army Aviation subsystem currently under development or via technology refresh. 


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

2:  doi: 10.1117/12.2302805


4:  S. King, et al.: "Designing and implementing malicious hardware," University of Illinois at Urbana Champaign, Urbana, IL 61801, 2008.

5:  J. Saltzer and M. Schroeder: "The protection of information in computer systems," Proceedings of the IEEE, 63(19):1278-1308, Sept. 1975.



8:  Wikipedia: RISC-V,

9:  CHISEL: Constructing Hardware in a Scala Embedded Language,

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

11:  seL4 microkernel.

12: "L4 microkernel family."

13:  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.

14:  K. Elphinstone and G. Heiser: "From L3 to seL4 what have we learnt in 20 years of L4 microkernels?," ACM Symposium on Operating Systems Principles Farmington, PA, pp. 133-150, 03 - 06 November 2013.

15: "Evaluation Assurance Level,"

16:  W. Keegan: "Separation Kernels Enable Rapid Development of Trustworthy Systems," COTS Journal, pp. 1-3, February 2014.

17:  C. Herley and P.C. van Oorschot: "SoK: Science, Security, and the Elusive Goal of Security as a Scientific Pursuit," Microsoft Research and Carleton University, ‎2017.


KEYWORDS: Open Source, RISC-V, SeL4, High Assurance, Safety Critical, Aerospace, Cybersecurity, Operating System 


Dr. Patrick Jungwirth 

(410) 278-6174 

Thomas Barnett 

(256) 876-4361 

US Flag An Official Website of the United States Government