By John McHale
SAN DIEGO, 25 Nov. 2008. Officials from Green Hills Software announced last month that their Integrity real-time operating system (RTOS) achieved the National Security Agency's highest level for software security. Green Hills officials made the announcement during the MILCOM conference and exhibition in San Diego.
The Green Hills RTOS, used in avionics applications, was certified by the National Information Assurance Partnership (NIAP), a U.S. government initiative operated by the National Security Agency (NSA), to Common Criteria Evaluation Assurance Level (EAL) 6+, High Robustness.
The whole process cost millions of dollars and took more than three years to complete, says Dan Mender, director of business development at Green Hills Software. No one has ever achieved a Common Criteria level this high, he adds. EAL 7 is the highest level.
"The EAL 7 is a measurement of the assurance, or confidence, in the software," says David Kleidermacher, chief technology officer at Green Hills Software. "The confidence of EAL6+ is so high that the U.S. government would use it to protect the most sensitive information on a computer that can be attacked by the most sophisticated (e.g. nation states, organized crime) adversaries. To get to this confidence level, the testing and analysis is extreme, meaning there is practically no possibility for a security defect that an adversary could use to subvert the system.
"At EAL 5, the testing and analysis is not nearly as extreme," Kleidermacher continues. "A key difference is the lack of a formal methods requirement. Without a formal proof of the security policy, the likelihood of a security flaw is much higher. Therefore, the likelihood of an attack is much higher. The type of attack is orthogonal. There is higher probability that some sort of flaw will exist and can be used for nefarious purposes."
Windows and Linux are only EAL 4+ and other RTOS vendors are not certified to any level, but they say they are pursuing it, Mender says.
According to a Green Hills public release only an EAL6+ High Robustness operating system is certified to protect classified information and other high value resources at risk of attack from hostile and well-funded attackers.
According to the Green Hills release the Common Criteria states that "EAL4 is the highest level at which it is likely to be economically feasible to retrofit to an existing product line." Integrity was designed for EAL7 -- the highest level of security.
"Integrity was designed from the ground up to meet EAL 7," Kleidermacher says. This certification was performed against the U.S. government Separation Kernel Protection Profile (SKPP), a U.S. government protection profile specifying high robustness."
In other words it reflects "the strength of security that the U.S. government requires for protecting high value resources against highly sophisticated attackers," he continues. "High robustness was mapped to Common Criteria EAL 6, augmented with requirements from EAL 7 (including formal methods), and with extended requirements as well. The industry uses EAL6+ for brevity.
"To go from EAL6+ to EAL7, a few of the assurance requirements would be modified," Kleidermacher says. "The key EAL 7 requirements relating to formal methods are in the SKPP. An example of a requirement that is not is in the area of secure delivery."
"EAL6+ requires that the customer be able to detect if the operating system has been modified," he notes. "This is obvious - we don't want someone to able to insert a hidden Trojan into the code. EAL7 requires prevention of modification. The SKPP authors saw no reason to increase the assurance level for this requirement. Once you are assured that you can detect a modification, you can simply refuse to install or run it."
The security gap between EAL4+-certified products and SKPP-certified products is immense, Green Hills officials say. EAL4+ does not even require examination of the product source code.
SKPP requirements include the use of formal methods to mathematically prove the security policies, formal specifications, formal correspondence between design and implementation, complete test coverage of all functional requirements, and penetration testing by the NSA, which has complete access to the source code.
"There is a formal model that maps to the operating system implementation – like an alternate reality," Kleidermacher says. "The formal model is written in a special language that is amenable to theorem proving. The security policy to be proven is also written in the special language. For the SKPP, a key theorem was the information separation policy: there cannot be any information flow between two security domains (partitions or processes) that have no explicit connection between them. The theorem prover does its job by examining each state, computing the change of state due for every operating system operation, and then observing that no information from one partition has transferred to another partition.
The INTEGRITY operating system is also certified under RTCA/DO-178B Level A, the highest level of avionics safety certification granted by the Federal Aviation Administration and the European Aviation Safety Agency.
The Integrity RTOS flies on the F-35 Joint Strike Fighter and was selected for NASA's Orion Crew Exploration Vehicle.
