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 system.

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.