Your System is Secure? Prove it! continued

There is also a requirement that the system under evaluation be “simple”. This is a reflection of the security principle of least authority (POLA) and economy of mechanisms, which imply that a system’s trusted computing base (TCB) be as small and simple as possible.

Testing Required

CC, even at EAL7, relies on testing. Although mathematical proofs are required for security properties of the system’s API, there is no proof that these properties hold for the actual implementation. This is why testing is still required. Testing, as Dijkstra famously stated, “can only show the presence, not the absence, of bugs.” Hence, even a system certified at EAL7 must be suspected to contain security flaws.

Why does CC not go further and require an actual correctness proof of the implementation? After all, formal proofs for computer programs have been around for decades.

Presumably the answer is that it was not considered feasible. Formal code proofs, doable for small algorithms, scale very poorly with code size. Systems that are undergoing CC certification at EAL6 or EAL7 are typically separation kernels, very simple OS kernels whose sole purpose is to provide strict (static) partitioning of resources among subsystems. A typical separation kernel consists of maybe 4,000 lines of code (LOC), which may be small as kernels go but is huge as far as formal verification is concerned.

The Next Step

So, are we stuck with trusting the security of our computer systems to traditional debugging approaches such as testing and code inspection, enhanced by model checking (a class of formal methods that may be able to prove the absence of certain categories of bugs but not all bugs)?

Download complete White Paper

More White Papers and Publications

▲ Back to Top