-
The most widely deployed mobile virtualization solution
Data Sheets
Open Kernel Labs Blog
November 20, 2008
What does CC EAL6+ mean?
Green Hills has just announced that they received an EAL6+ security certification under the Common Criteria (CC) Separation Kernel Protection Profile (SKPP) for their Integrity microkernel OS. Integrity is the first OS to reach this level, and I congratulate the GHS folks on this impressive success. It must have cost them a mint, industry rule-of-thumb is $1k per line of code (so, say $5M total!) It's also a validation of the microkernel approach (as used in our OKL4), as there is a snowball-in-hell's chance of achieving this with any other OS design.
But what does it mean?
CC is a framework for security evaluation of IT systems. There are seven levels of evaluation, from EAL1 (most shallow) to EAL7 (most thorough). Evaluation is against security requirements defined in a protection profile (PP), where the SKPP is presently the only PP applicable to operating systems which is suitable for the highest levels of certification.
So, what do those EALs really mean?
EAL4, even though it is the middle one, means very litte in reality. Which is evidenced by the fact that systems like Linux and Windows have been EAL4+ certified (the "+" means "with extra stuff") and everyone knows how many security holes they have. It's basically a glorified (and very expensive) ISO-9000 process (and EAL4 is the first level where anyone actually looks at the source code).
At EAL5 things start getting halfway serious. You need a semi-formal (UML-style) representation of the functional specification and the top-down design. The idea is that you need to show that you took a systematic approach to specifying and designing the system. Of course, that doesn't mean that the specification is any good, or that the design will actually produce something that meets the spec. And it means even less that the implementation is anywhere near correct. "Informal" (read hand-waving) arguments are used to match the implementation to the design, and beyond that CC relies on good old — you guessed it — testing. Just like Microsoft and the Linux folks do.
At EAL6 (this is what Green Hills did), the main added requirement is a formal statement of requirements. Meaning there is a mathematical model of the security requirements of the system. This is then somehow linked to the (semi-formal) design and the semi-formal spec. And informal (i.e.hand-waving) arguments are used to link this to the implementation. And — yes — more testing.
As Dijkstra famously remarked almost 40 years ago: "testing proves the presence, not the absence of errors".
Surely, EAL7 fixes that?
Well, not really. Sure, at EAL7 you need a formal spec (i.e. a mathematical model of the functionality of the system) and a formal design (mathematical model of the structure). The spec must be formally (mathematically) proven to meet the requirements, and the design must be formally proven to implement the spec. But how about the implementation? Well, there is — who would have thought — yet more testing.
So, despite all those nice models, IOS-9000-style stuff, code inspection, etc, etc, the correctness of the implementation still comes down to testing. Remember what Dijkstra said?
So this is the highest, and so far unachieved, evaluation level of CC. Is this really the best that can be done?
Nope, we can do better, as is being shown in NICTA's L4.verified project. This is working on a complete, formal proof chain, from security requirements to implementation (C and assembler code). About a year ago, the proof chain reached from the requirements to the (low-level) design — essentially what CC EAL7 requires. In the meantime the NICTA team hasn't been idle, and has almost closed the gap. The compete formal verification of the implementation is a month or two away.
Once this is done, the world will have its first general-purpose operating-system kernel that has been fully formally verified — mathematically proven to meet its security requirements, all the way down to the actual code. The world will have its first truly secure operating system.
Stay tuned.
Posted by Gernot Heiser on November 20 at 11:23 PM
blog comments powered by Disqus
About Gernot Heiser:
Gernot Heiser, Co-founder and Consulting Scientist, never thought he would be in the business world. Prior to NICTA's creation in 2003, Dr Heiser was a full-time faculty member at the University of New South Wales. However, this die-hard academic couldn’t pass up the opportunity to see the commercialization of this research. Gernot still loves teaching, almost as much as he loves good wine and good food. And anyone will tell you that Gernot knows his wine.