TS News

News

Proof that seL4 enforces integrity established for RISC-V
2021-07-28 – The assurance story for seL4 on RISC-V keeps building. We first formally proved functional correctness: that the seL4 C code on RISC-V platforms behaves exactly as its specification says. We then established binary correctness: that the machine code running on the processor behaves exactly as the C code, and by extension, as the specification says. We now have established the crucial integrity property for seL4 on RISC-V: that the specification, and by extension the kernel binary, prevents an application running on top from modifying data without authorisation. In seL4 speak: seL4 provably enforces capability-based access control. “The integrity property is crucial for security: it is key to enforce the isolation of components running on top of the kernel”, says Gerwin Klein, seL4 verification expert and chair of the seL4 Foundation technical steering committee. “This is what allows critical components, like the network controller that has access to software-controlled brakes in a modern car, to securely run alongside untrusted software, like the entertainment system. With integrity proved, you know that an attack on or from a vulnerable untrusted part of the system cannot compromise the critical parts.” Integrity had been proved in the original seL4 verification on the Arm32 architecture. It is now also established for RISC-V architecture, making it the only 64-bit architecture that has an OS with such a comprehensive verification and security story. We thank Ryan Barry of Trustworthy Systems, main author of these proofs! We also gratefully acknowledge funding from the Australian Reseach Council through grant DP190103743 which has enabled this work. See Gernot's blog for more details. The proof is available on GitHub.

Proof that seL4 enforces integrity established for RISC-V

2021-07-28 – The assurance story for seL4 on RISC-V keeps building. We first formally proved functional correctness: that the seL4 C code on RISC-V platforms behaves exactly as its specification says. We then established binary correctness: that the machine code running on the processor behaves exactly as the C code, and by extension, as the specification says. We now have established the crucial integrity property for seL4 on RISC-V: that the specification, and by extension the kernel binary, prevents an application running on top from modifying data without authorisation. In seL4 speak: seL4 provably enforces capability-based access control.

“The integrity property is crucial for security: it is key to enforce the isolation of components running on top of the kernel”, says Gerwin Klein, seL4 verification expert and chair of the seL4 Foundation technical steering committee. “This is what allows critical components, like the network controller that has access to software-controlled brakes in a modern car, to securely run alongside untrusted software, like the entertainment system. With integrity proved, you know that an attack on or from a vulnerable untrusted part of the system cannot compromise the critical parts.”

Integrity had been proved in the original seL4 verification on the Arm32 architecture. It is now also established for RISC-V architecture, making it the only 64-bit architecture that has an OS with such a comprehensive verification and security story. We thank Ryan Barry of Trustworthy Systems, main author of these proofs! We also gratefully acknowledge funding from the Australian Reseach Council through grant DP190103743 which has enabled this work.

See Gernot's blog for more details. The proof is available on GitHub.

The Trustworthy Systems Group is now back at UNSW
2021-07-21 – The Trustworthy Systems (TS) grew to world fame in NICTA, with the design, implementation and verification of seL4 its defining achievement. When NICTA was absorbed into CSIRO's Data61 in mid-2015, TS became part of it, and was one of a small number of groups that defined Data61's international reputation. We attracted millions of dollars in funding every year from government organisations such as DARPA and industry players such as HENSOLDT Cyber. Despite all that, Data61 has withered TS down from over 50 people two years ago to less than twenty. In May CSIRO management finally announced that TS is no longer wanted, for reasons that are hard to fathom. We are extremely grateful to UNSW's School of Computer Science and Engineering for giving us a new home and some bridging funding that allows us to continue operate and rebuild. We will continue perform world-leading research and technology transfer on seL4 and its ecosystem, and support the seL4 community as part of the seL4 Foundation. Specifically we are keen to engage with organisations that can provide funding for our work.

The Trustworthy Systems Group is now back at UNSW

2021-07-21 – The Trustworthy Systems (TS) grew to world fame in NICTA, with the design, implementation and verification of seL4 its defining achievement. When NICTA was absorbed into CSIRO's Data61 in mid-2015, TS became part of it, and was one of a small number of groups that defined Data61's international reputation. We attracted millions of dollars in funding every year from government organisations such as DARPA and industry players such as HENSOLDT Cyber.

Despite all that, Data61 has withered TS down from over 50 people two years ago to less than twenty. In May CSIRO management finally announced that TS is no longer wanted, for reasons that are hard to fathom.

We are extremely grateful to UNSW's School of Computer Science and Engineering for giving us a new home and some bridging funding that allows us to continue operate and rebuild. We will continue perform world-leading research and technology transfer on seL4 and its ecosystem, and support the seL4 community as part of the seL4 Foundation. Specifically we are keen to engage with organisations that can provide funding for our work.

seL4 on RISC-V is verified to the binary
2021-05-05 – The seL4 Foundation and RISC-V International announced that the verified seL4 microkernel on the RV64 architecture has been proved down to the executable code by the Trustworthy Systems group, thanks to funding provided by HENSOLDT Cyber GmbH. This guarantees that the seL4 microkernel on RV64 will operate to specification even when built with an untrusted C compiler, GCC. For more details on binary verification of seL4 on RISC-V see Gernot's blog: seL4 on RISC-V Verified to Binary Code (and seL4 and RISC-V Foundations form an alliance).

seL4 on RISC-V is verified to the binary

2021-05-05 – The seL4 Foundation and RISC-V International announced that the verified seL4 microkernel on the RV64 architecture has been proved down to the executable code by the Trustworthy Systems group, thanks to funding provided by HENSOLDT Cyber GmbH. This guarantees that the seL4 microkernel on RV64 will operate to specification even when built with an untrusted C compiler, GCC.

For more details on binary verification of seL4 on RISC-V see Gernot's blog: seL4 on RISC-V Verified to Binary Code (and seL4 and RISC-V Foundations form an alliance).

Gernot has been appointed as one of ACM’s Distinguished Speakers
2021-05-04 Professor Gernot Heiser has been appointed as one of ACM's Distinguished Speakers, "Renowned International Thought Leaders Speaking on the Most Important Topics in Computing Today"! You can see the full list of speakers here. Congratulations to Gernot for joining this illustrious group!

Gernot Heiser named ICT Researcher of the Year
2021-04-20 Congratulations goes to Gernot Heiser on receiving the 2015 Digital Disruptor - ICT Researcher of the Year in what was an extremely competitive category..more

Show older articles