Your System is Secure? Prove it! continued

CC compliance is evaluated to a particular evaluation assurance level (EAL). These range from EAL1, the easiest (requiring little more than a demonstration that the system has undergone some testing), to EAL7, the toughest. The goal of a CC evaluation is to obtain certification from an accredited authority that the system satisfies all the required criteria for a particular PP at a certain EAL. A higher evaluation level means a more thorough examination of the system. This does not, however, guarantee more security; it means only that a more thorough and systematic attempt is made to eliminate vulnerabilities.

A number of operating systems have been certified under CC, including Mac OS to EAL3, versions ofWindows, Linux, and Solaris to EAL4, and the hypervisor of IBM’s z-Series to EAL5. The Green Hills Integrity microkernel is said to be undergoing evaluation to EAL6.

But what does this mean? At the toughest assurance level, EAL7 (which to my knowledge has not yet been achieved by any OS that provides memory protection), CC evaluation is characterized as “formally verified design and tested.” In a nutshell, this means two things:

  1. The system has an unambiguous specification. At EAL7 this must be in the form of a formal (mathematical) model, and there has to be a formal proof that the specification satisfies the requirements of the PP (e.g., that no unauthorized flow of data is possible in the system).
  2. There is a correspondence between the mathematical model and the actual implementation of the system. This is established by a combination of means, including a formal highlevel design, an at least semiformal low-level design, formal or semiformal correspondence between them, a detailed mapping of design to implementation, and comprehensive independent testing.

Download complete White Paper

More White Papers and Publications

▲ Back to Top