Gernot Heiser and ETH Zurich co-authors win Best Paper award at DATE'21
2021-10-10 The paper “Microarchitectural Timing Channels and their Prevention on an Open-Source 64-bit RISC-V Core” by Nils Wistoff, Moritz Schneider, Frank K. Gurkaynak, Luca Benini and Gernot Heiser won Best Paper at the Tier-1 Design, Automation and Test in Europe (DATE) conference.

Gernot explains why seL4 is safe – and the role of TS

2021-09-28 – Following CSIRO's abandoning of TS and the seL4 technology TS developed, the seL4 community and the seL4 Foundation have grown a lot. This has led to concerns that the broader participation might have the potential to undermine the integrity of seL4. In his latest blog, Gernot explains why there is no reason for such concern, and how TS is re-building to continue driving the research that keeps seL4 define the state of the art.

TS services receive interim endorsement from the seL4 Foundation
2021-08-22 – The seL4 Foundation has given interim endorsement to TS as a trusted provider for services around seL4.

seL4 protects world's most secure drone from DEFCON hackers

2021-08-13 – On 6 August DARPA brought the “SMACCMcopter” to DEF CON and invited the assembled hacker elite to attack it. The SMACCMcopter was the research vehicle of the Air Team at DARPA's HACMS program. The Trustworthy Systems team worked with project partners to deploy seL4 and leverage formal methods to protect the drone from cyber attacks. The result? Predictably, sel4's verified security enforcement defeated the hackers comprehensively. As DARPA said: “Formal methods FTW!”

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.