The principal aim of Sec is to enable execution of untrusted software components in an environment operating under a user-defined security policy such that these untrusted components can not violate the security policy. For a user to place trust into the supposedly secure execution of an untrusted component, the user must trust the execution engine to confine the effects of the untrusted code within the boundaries determined by the security policy. Hence, the execution engine is part of the trusted computing base (TCB). In the security community, it is well know that the trust in the TCB grows when the TCB becomes smaller.1
A shortcoming of mainstream commercial platforms, such as the Java Virtual Machine and .NET's CLR, is the considerable size of the TCB. The size of those platforms is due to the comparably high-level of abstraction of the executed byte codes (i.e., JVM bytecode and ILX, respectively). Execution of such byte codes requires a large amount of sophisticated machinery, which is exactly what the TCB should not contain.
Surprisingly, the high-level of abstraction of aforementioned byte codes has, in part, been motivated by the desire for secure execution of untrusted code. The reasoning was that it is easier to test conformity vis-a-vis a security policy for high-level than for low-level codes, as the former enjoy a richer set of semantic properties. What has been overlooked is that they are not of much value if the user places little trust in them due to the complexity of the software implementing these semantic properties; i.e., the software that performs the conformity test and executes the byte code.
Recent research concerned with typed intermediate languages and certifying compilers has shown how low-level codes with suitable annotations - called a certificate - can provide similar guarantees as high-level byte code.2 In essence, the certificate, which may take the form of types or proof objects, provide the semantic guarantees that usually distinguish high-level from low-level codes. The TCB is minimised by choosing the certificate such that its integrity can be easily and cheaply checked at load time. Hence, the software that generates the low-level code and the certificate need not be trusted per se; only the certificate checker and the execution engine of the low-level code need to be trusted. The formal basis for asserting the validity of a certificate checker comes from the areas of proof theory and automated theorem proving, both of which have made significant advances in the last ten years. Moreover, it has been demonstrated that the trusted code base for a certificate checker can be kept very small. By choosing a low-level, instead of a high-level code for portable binaries, we can achieve a much smaller TCB than that of a typical high-performance JVM implementation. In summary, the pivotal element of Sec's approach is to use certifying compilation to reduce the size of the core infrastructure, thus, minimising the TCB.
Certifying compilers have one main weakness: They can only generate certificates for properties that can be asserted by an automated analysis. Hence, they fulfil their full potential only when the source code is in a very high-level language, but even for such languages there are fundamental limits to the properties that can be automatically checked. Currently, a significant amount of research is aimed at pushing the boundaries, so certificates for a wider range of properties can be inferred automatically. However, this will only change the limits, but not entirely eliminate them.
The limitation of static analysis motivates the combination of certifying compilers with other techniques to enforce security policies.2 In particular, execution monitoring by reference monitors can be used to check at runtime that aspects of a given security policy are not violated by a software component. The two technical difficulties with execution monitoring are that (1) a reference monitor needs to be invoked before an instruction that may potentially compromise a security policy and (2) the reference monitor must be protected against subversion by the monitored software component. Both difficulties can be approached purely in software or with hardware support. In a pure software approach, the reference monitor needs to be inlined into the monitored code, which makes it hard to protect the reference monitor against subversion (e.g., self-modifying code) without extra assertions about the monitored code (e.g., the code may be a high-level byte code or it is low-level code generated by a particular compiler). In a hardware-supported approach, hardware (such as conventional memory management unit) is used to trap offending instructions and to protect associated monitoring software (such as the operating system) from subversion. However, the fact that the reference monitor is typically located in a separate address space leads to extra context switching costs.
Schneider et al.2 argue for a combination of type systems, inlined reference monitors (i.e., purely software-based reference monitors), and certifying compilers. In other words, they concentrate on software and, in particular, on language-based techniques. They do not consider to include hardware-based and operating-system mediated techniques.
In addition to the research opportunities that still exist for purely language-based techniques, there appears to be a distinct lack of research that attempts to reconcile language-based and OS-mediated techniques. This is surprising as both approaches have complementary strength. Language-based techniques excel when a software component comes with rich semantic properties (e.g., if it is written in a language with a rich type structure, as provided by ML and Haskell and, to a lesser extent, by Java and C#). Although, it has been demonstrated that language-based techniques can be applied to low-level code,3 this usually requires manual intervention. OS-mediated techniques do not depend on inferring static properties of software components, which gives them an advantage on components that lack such properties (e.g., high-level code using unsafe features and low-level code). Moreover, some properties, such as for example time and space bounds, are notoriously hard to determine statically. Hence, they make the use of OS-mediated techniques attractive even for components generated from a high-level language.
In particular, the following two features of our approach clearly distinguish us from other projects:
The second feature means that we certify code whose abstraction level is similar to assembly (which distinguishes us from JVM-based approaches), but which is still independent of any single architecture (which distinguishes us from most TAL work).
firstname.lastname@example.org• Last modified: Sat May 10 00:35:05 EST 2003 >