TS News

News

Gernot delivers keynote at ACM SYSTOR
2022-06-15 – TS group leader Gernot Heiser delivered a keynote at the ACM Systems and Storage Conference in Haifa, Israel. The talk, titled “Can we make trustworthy systems a reality?” examines the successes and challenges of taking the seL4 microkernel to the real world, and looks at current research done on and around seL4 at UNSW.

UNSW-SSRC collaboration to fortify systems and prevent hacking
2022-02-09 – UNSW has partnered with Secure Systems Research Center to implement ground-breaking cyber security technology. “This collaborative effort between UNSW and SSRC will aim to extend the formally verified seL4 microkernel to support tight integration of virtualised systems,” said UNSW Trustworthy Systems leader and John Lions Chair, Scientia Professor Gernot Heiser. Full UNSW announcement. Full SSRC announcement.

UNSW-SSRC collaboration to fortify systems and prevent hacking

2022-02-09 – UNSW has partnered with Secure Systems Research Center to implement ground-breaking cyber security technology.

“This collaborative effort between UNSW and SSRC will aim to extend the formally verified seL4 microkernel to support tight integration of virtualised systems,” said UNSW Trustworthy Systems leader and John Lions Chair, Scientia Professor Gernot Heiser.

Full UNSW announcement.
Full SSRC announcement.

Proof that seL4 enforces confidentiality established for RISC-V
2021-12-02 – In July, we announced that the assurance story for seL4 on RISC-V keeps building, with the completion of the proof that seL4 enforces integrity, following the earlier proofs of functional correctness and binary correctness for seL4 on RISC-V. The next step in the assurance stack is now also completed for RISC-V with the proof that seL4 enforces confidentiality, i.e. that seL4 provably enforces information flow control, when it is correctly configured to do so. “This completes the 3 big CIA security properties for seL4 on RISC-V: confidentiality, integrity and availability. While integrity ensures there is no unauthorised interference with private data, confidentiality ensures there is no unauthorised access to private data”, says Gernot Heiser, chair of the seL4 Foundation. Special thanks to TS's Ryan Barry, main author of these proofs! We also gratefully acknowledge funding from the Australian Reseach Council through grant DP190103743 which has enabled this work. The proof is available on GitHub.

Proof that seL4 enforces confidentiality established for RISC-V

2021-12-02 – In July, we announced that the assurance story for seL4 on RISC-V keeps building, with the completion of the proof that seL4 enforces integrity, following the earlier proofs of functional correctness and binary correctness for seL4 on RISC-V.

The next step in the assurance stack is now also completed for RISC-V with the proof that seL4 enforces confidentiality, i.e. that seL4 provably enforces information flow control, when it is correctly configured to do so.

“This completes the 3 big CIA security properties for seL4 on RISC-V: confidentiality, integrity and availability. While integrity ensures there is no unauthorised interference with private data, confidentiality ensures there is no unauthorised access to private data”, says Gernot Heiser, chair of the seL4 Foundation.

Special thanks to TS's Ryan Barry, main author of these proofs! We also gratefully acknowledge funding from the Australian Reseach Council through grant DP190103743 which has enabled this work. The proof is available on GitHub.

New partnership formed to protect human rights organisations from cyber-attacks
2021-11-29 – UNSW Sydney has signed a research agreement with Swiss technology company Neutrality to develop cyber network safeguards for organisations whose integrity and trust is essential in protecting people. “This project aims at protecting communications of humanitarian and other non-government organisations from cyber-attacks, which often result in loss of lives”, said UNSW Trustworthy Systems leader and John Lions Chair, Scientia Professor Gernot Heiser. “Trustworthy Systems will work with Neutrality in the development of such secure communication, leveraging the mathematically proved security enforcement provided by our seL4 microkernel technology.” Full UNSW announcement.

New partnership formed to protect human rights organisations from cyber-attacks

2021-11-29 – UNSW Sydney has signed a research agreement with Swiss technology company Neutrality to develop cyber network safeguards for organisations whose integrity and trust is essential in protecting people.

“This project aims at protecting communications of humanitarian and other non-government organisations from cyber-attacks, which often result in loss of lives”, said UNSW Trustworthy Systems leader and John Lions Chair, Scientia Professor Gernot Heiser. “Trustworthy Systems will work with Neutrality in the development of such secure communication, leveraging the mathematically proved security enforcement provided by our seL4 microkernel technology.”

Full UNSW announcement.

Alaska Center for Energy Power joins the Laot team
2021-10-27 – The Alaska Center for Energy and Power (ACEP) has joined the Laot project team. ACEP will conduct tests and demonstrations in their Fairbanks facility.

Show older articles