SSRG News

We have released one of the main C verification tools in the L4.verified project under BSD license. The C-to-Isabelle parser reads C99 files into the theorem prover Isabelle/HOL and provides the basis for their formal verification.

Download the C parser here.

NICTA and German IT security specialist secunet Security Networks AG have entered a strategic research collaboration to develop high-security information technology (IT) products for the defence and government sectors. The research will combine secunet's experience in designing and building high-security devices with NICTA's expertise in formal verification and secure microkernel technology.

Download the full press release here.

SSRG students Etienne Le Sueur, Bernard Blackham, Martin Pflauminger and Aaron Carroll have won the 2011 Lantronix XPort Pro Design Contest with their e⁴Meter.

NICTA and OK Labs have announced the first joint public release of the formally verified seL4 microkernel (branded OKL4 Verified). The release, for non-commercial and evaluation use, contains seL4 kernel binaries for ARM and x86, documentation, user level examples, x86 Linux on top of seL4, and the formal specification of the kernel for the ARM platform.

NICTA press release
Download seL4
L4.verified project

OK Labs has announced that OKL4, derived from NICTA's L4-embedded microkernel, has now shipped in more than 1.1 billion mobile phones. This makes OKL4 one of the most widely-deployed OS kernels ever.

NICTA press release

We have released a snapshot of the vNUMA source for download.

A paper titled Improved device driver reliability through hardware verification reuse has been accepted for publication in the 16^th ASPLOS Conference. The paper is the result of a collaboration with Intel (Hillsboro, OR) lead by SSRG researcher Leonid Ryzhyk.