Your System is Secure? Prove it! …

                              Your System is Secure? Prove it!
                                                   Gernot Heiser

                                NICTA and University of New South Wales
                                        and Open Kernel Labs
                                          Sydney, Australia
                                        gernot@nicta.com.au


   Computer security is an old problem which has                   and can then select any system that is certified to
lost none of its relevance -- as is evidenced by                   match that PP.
the annual Security issue of ;login:. The systems                      CC compliance is evaluated to a particular eval-
research community has increased its attention to                  uation assurance level (EAL). These range from
security issues in recent years, as can be seen by                 EAL1, the easiest (requiring little more than a
an increasing number of security-related papers                    demonstration that the system has undergone some
published in the mainstream systems conferences                    testing), to EAL7, the toughest. The goal of a CC
SOSP, OSDI, and USENIX. However, the focus is                      evaluation is to obtain certification from an accred-
primarily on desktop and server systems.                           ited authority that the system satisfies all the re-
   I have argued two years ago in this place that                  quired criteria for a particular PP at a certain EAL.
security of embedded systems, whether mobile                       A higher evaluation level means a more thorough
phones, smart cards, or automobiles, is a loom-                    examination of the system. This does not, how-
ing problem of even bigger proportions, yet there                  ever, guarantee more security; it means only that a
does not seem to be a great sense of urgency about                 more thorough and systematic attempt is made to
it. Although there are embedded operating-system                   eliminate vulnerabilities.
(OS) vendors working on certifying their offerings                     A number of operating systems have been cer-
to some of the highest security standards, those sys-              tified under CC, including Mac OS to EAL3, ver-
tems do not seem to be aimed at, or even suitable                  sions of Windows, Linux, and Solaris to EAL4, and
for, mobile wireless devices.                                      the hypervisor of IBM's z-Series to EAL5. The
                                                                   Green Hills Integrity microkernel is said to be un-
                                                                   dergoing evaluation to EAL6.
Establishing OS Security                                               But what does this mean? At the toughest assur-
                                                                   ance level, EAL7 (which to my knowledge has not
The accepted way for establishing system secu- yet been achieved by any OS that provides memory
rity is through a process called assurance. Assur- protection), CC evaluation is characterized as "for-
ance examines specification, design, implementa- mally verified design and tested." In a nutshell, this
tion, operation, and maintenance of a system.                      means two things:
   The most widely used assurance process is the
international standard called the Common Criteria                    1. The system has an unambiguous specification.
for IT Security Evaluation, or Common Criteria                           At EAL7 this must be in the form of a formal
(CC) for short. CC evaluation is performed against                       (mathematical) model, and there has to be a
a protection profile (PP), which represents a stan-                      formal proof that the specification satisfies the
dardized set of security properties the system un-                       requirements of the PP (e.g., that no unautho-
der evaluation is expected to meet. The idea is that                     rized flow of data is possible in the system).
purchasers of IT systems define their security re-                   2. There is a correspondence between the math-
quirements through a PP (or a combination of PPs)                        ematical model and the actual implementation
   
    NICTA is funded by the Australian Government's Back-
                                                                         of the system. This is established by a com-
ing Australia's Ability initiative, in part through the Australian       bination of means, including a formal high-
Research Council.                                                        level design, an at least semiformal low-level
2


     design, formal or semiformal correspondence        powerful construct than a separation kernel, as it
     between them, a detailed mapping of design to      is a platform on which a general-purpose OS can
     implementation, and comprehensive indepen-         be implemented. A well-designed microkernel is a
     dent testing.                                      superset of a separation kernel, in that it can pro-
                                                        vide the same functionality, plus more. However, it
  There is also a requirement that the system un-       is inherently more complex: A minimal microker-
der evaluation be "simple". This is a reflection of     nel that has sufficient functionality to support high-
the security principle of least authority (POLA) and    performance systems of (virtually) arbitrary func-
economy of mechanisms, which imply that a sys-          tionality weighs in at some 7,000­10,000 LOC.
tem's trusted computing base (TCB) be as small
                                                           In spite of this, complete formal verification of
and simple as possible.
                                                        a microkernel is nearing completion at NICTA. In
                                                        a project that has been running since January 2004,
Testing Required                                        the API of seL4, the latest member of the L4 micro-
                                                        kernel family, has been formalized as a mathemat-
CC, even at EAL7, relies on testing. Although           ical model in a theorem prover. A number of se-
mathematical proofs are required for security prop-     curity properties have been proved about this API,
erties of the system's API, there is no proof that      with more to come: The aim is to provide a com-
these properties hold for the actual implementation.    plete set of proofs corresponding to at least one of
This is why testing is still required. Testing, as      the CC PPs. The seL4 kernel can then be used as
Dijkstra famously stated, "can only show the pres-      the basis of systems whose TCB is truly trustwor-
ence, not the absence, of bugs." Hence, even a sys-     thy.
tem certified at EAL7 must be suspected to contain         The implementation proof is progressing concur-
security flaws.                                         rently with the security proofs of the API. It uses
   Why does CC not go further and require an ac-        the refinement approach, which is a multistep pro-
tual correctness proof of the implementation? After     cedure involving intermediate representations (be-
all, formal proofs for computer programs have been      tween the specification and the code). Each refine-
around for decades.                                     ment step proves that the lower-level representation
   Presumably the answer is that it was not consid-     has all the relevant properties of the higher level.
ered feasible. Formal code proofs, doable for small        In the case of seL4, there are three levels: The
algorithms, scale very poorly with code size. Sys-      formal specification is the highest and the actual
tems that are undergoing CC certification at EAL6       C and assembler code of the kernel implementa-
or EAL7 are typically separation kernels, very sim-     tion is the lowest. The intermediate level (which
ple OS kernels whose sole purpose is to provide         roughly corresponds to CC's lowlevel design) has
strict (static) partitioning of resources among sub-    a concrete meaning too: It corresponds to a pro-
systems. A typical separation kernel consists of        totype of the kernel implemented in the functional
maybe 4,000 lines of code (LOC), which may be           programming language Haskell, which serves as an
small as kernels go but is huge as far as formal ver-   executable specification for porting and evaluation
ification is concerned.                                 purposes.
                                                           The first refinement step is completed; the sec-
                                                        ond (and final) one is in progress and is due for
The Next Step
                                                        completion during the second quarter of 2008.
So, are we stuck with trusting the security of             This still leaves a gap: It assumes that the cor-
our computer systems to traditional debugging ap-       rectness of the implementation is established by
proaches such as testing and code inspection, en-       showing the correctness of the code (C and as-
hanced by model checking (a class of formal meth-       sembler). Although CC makes the same assump-
ods that may be able to prove the absence of certain    tion, this nevertheless leaves the C compiler and
categories of bugs but not all bugs)?                   the assembler as trusted components in the loop.
  I think not. One of the most exciting develop-        Given the quality, size, and complexity of a typical
ments in this respect is that it now seems feasi-       C compiler, this is still an uncomfortable level of
ble to fully verify the implementation of a com-        trust.
plete microkernel. A microkernel is a much more            The problem could be solved by performing a
                                                        3


third refinement step, from C/assembler to actual
machine code. This would require a considerable
effort, but it is inherently no more difficult (most
likely easier) than the previous refinement steps.
However, there is promising work performed else-
where on compiler verification. A verified com-
piler could be leveraged to close the gap without a
further refinement step on the kernel.


Let's Get Serious about Security!
Security has far too long been treated with in-
sufficient rigor, given what's at stake. CC, de-
spite best intentions, could actually be counter-
productive there. By stopping short of the require-
ment for formal verification at the highest assur-
ance level, CC have the potential to create a false
sense of security. After all, a system certified to
EAL7 can rightly be claimed to have passed the
highest hurdle of security evaluation. The prob-
lem is that this is still incomplete, and a potential
of security flaws remains.
   If complete formal verification is possible, it
must become a requirement.


Further reading
The approach taken in designing and implementing
seL4 is described by K. Elphinstone et al., "Ker-
nel Development for High Assurance", 11th Work-
shop on Hot Topics in Operating Systems, San
Diego, May 2007, USENIX. Further information
on seL4 can be found on the project Web site, http:
//ertos.org/research/sel4/, and the Web site of
the verification project, http://ertos.org/research/
l4.verified/.
   The Common Criteria are available at http://
csrc.nist.gov/.