Sec is a research and development project exploring novel
approaches to the safe and efficient execution of a mixture of trusted
and untrusted software components in a multi-language environment. Sec
uses a combination of language-based and OS-mediated techniques to
guarantee user-defined safety policies.
- Certified mobile code
Certified code carries a statement of its safety properties in a
form that can be automatically checked before execution.
Certified code in Sec is architecture-neutral, but low-level. Unlike
the bytecode of the Java Virtual Machine, Sec is language
independent and much closer to actual machine code, thus, minimising
the trusted computing base.
- Gaps in certificates
Some compilers can only generate weak certificates. Certificates for
some safety properties are difficult or impossible to generate
automatically. Hence, certificates can lack some of the assertions a
user wants of untrusted code. Sec closes gaps in certificates by
means of protection mechanisms provided by the underlying operating
Sec is a joint venture of the CORG, DiSy, and PLS research groups at
the University of New South Wales
with funding from the Australian
Research Council and links to the ERTOS (Embedded, Real-Time and
Operating Systems) and Formal Methods programs of NICTA as well as Gelato.
Last modified: Wed May 14 12:39:51 EST 2003