TS News

News

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

seL4 is verified on RISC-V
2020-06-09 – Trustworthy Systems is extremely pleased to announce that we have completed the functional correctness proof of seL4 on the RV64 ISA. Congratulations to our awesome Proof Engineering Team on achieving this major milestone for seL4! And many thanks to HENSOLDT Cyber for making it possible. We now have the refinement proof from the seL4 formal spec to the C implementation, putting RV64 on the same level as x64 in terms of seL4 verification. The binary verification, which extends this refinement to the binary code of the kernel is progressing, stay tuned for more news on that in the foreseeable future. You can find more details about the verification of seL4 on RISC-V on Gernot's blog

seL4 is verified on RISC-V

2020-06-09 – Trustworthy Systems is extremely pleased to announce that we have completed the functional correctness proof of seL4 on the RV64 ISA. Congratulations to our awesome Proof Engineering Team on achieving this major milestone for seL4! And many thanks to HENSOLDT Cyber for making it possible.

We now have the refinement proof from the seL4 formal spec to the C implementation, putting RV64 on the same level as x64 in terms of seL4 verification. The binary verification, which extends this refinement to the binary code of the kernel is progressing, stay tuned for more news on that in the foreseeable future.

You can find more details about the verification of seL4 on RISC-V on Gernot's blog

Show older articles