TS News

News

Mathieu Paturel speaks at ApSys '23 in Korea
2023-09-18 – Undergraduate team member Mathieu Paturel spoke at ApSys ‘23 on behalf of Trustworthy Systems and our research. He had these words to say about the experience: "I was really fortunate to go to Seoul, Korea, to present some of the work we did with my former lecturer and supervisor, Zoltan Kocsis, and fellow team member Isitha Subasinghe , at the Asia Pacific Systems Workshop '23. The paper is called "First steps in verifying the seL4 Core Platform". During my taste of research project, I started writing a tool that used SMT solvers to automatically prove a key part of the correctness of the seL4 microkit (previously known as the Core Platform). The benefit is that the SMT solvers do the proof for us, so we don't have to write and maintain them ourselves; the downside is that SMT solvers aren't as smart as humans, and so we can't expect them to prove statements that are too complicated. In our case, we were able to express our conditions just right so that it was attainable. Being an undergraduate presenting the work felt pretty special, I feel pretty proud of that. To me, it just shows how amazing the people at Trustworthy Systems are: full of kindness and care, and of course, technical skills." Congratulations to Mathieu for presenting at his first international conference.

Mathieu Paturel speaks at ApSys '23 in Korea

2023-09-18 – Undergraduate team member Mathieu Paturel spoke at ApSys ‘23 on behalf of Trustworthy Systems and our research. He had these words to say about the experience:

"I was really fortunate to go to Seoul, Korea, to present some of the work we did with my former lecturer and supervisor, Zoltan Kocsis, and fellow team member Isitha Subasinghe , at the Asia Pacific Systems Workshop '23. The paper is called "First steps in verifying the seL4 Core Platform". During my taste of research project, I started writing a tool that used SMT solvers to automatically prove a key part of the correctness of the seL4 microkit (previously known as the Core Platform). The benefit is that the SMT solvers do the proof for us, so we don't have to write and maintain them ourselves; the downside is that SMT solvers aren't as smart as humans, and so we can't expect them to prove statements that are too complicated. In our case, we were able to express our conditions just right so that it was attainable. Being an undergraduate presenting the work felt pretty special, I feel pretty proud of that. To me, it just shows how amazing the people at Trustworthy Systems are: full of kindness and care, and of course, technical skills."

Congratulations to Mathieu for presenting at his first international conference.

Trustworthy Systems Travels
2023-07-21 – This mid-year period has seen Gernot Heiser and other TS members present around the world. After the ACM Software System Award, Gernot Heiser participated in the IFIP Working Group 10.4 meeting on the Future of Dependable Computing and Fault Tolerance in Arcos de Valdevez, Portugal. Gernot and Ivan Velickovic delivered a seL4 tutorial at the 53rd Annual IEEE/IFIP International Conference on Dependable Systems and Networks (DSN). Gernot also gave a keynote, titled "Intelligent Vehicle Security Needs a Verified Operating System” at the DSN-affiliated Workshop on Safety and Security of Intelligent Vehicles and participated in a panel discussing intelligent vehicle security. Gernot gave a talk titled “Secure Systems Design on seL4” at the RITICS-Space meeting, organised by Imperial College’s Research Institute in Trustworthy Inter-Connected Cyber-Physical Systems in London, UK. Gernot attended the 17th Usenix Symposium on Operating Systems Design and Implementation in Boston, USA and participated in the SOSP Program Committee meeting. Gernot, together with June Andronick, visited UK’s Defence Science & Technology Lab (Dstl) in Salisbury, UK for discussions about the development and deployment of seL4-based systems. Gernot visited Airbus Defence & Space in Manching near Ingolstadt, Germany for discussions around seL4. (This photo is of Gernot Heiser outside the Airbus site with a Barracuda drone)

Trustworthy Systems Travels

Gernot Heiser outside the airbus site with a Barracuda drone

2023-07-21 – This mid-year period has seen Gernot Heiser and other TS members present around the world.

After the ACM Software System Award, Gernot Heiser participated in the IFIP Working Group 10.4 meeting on the Future of Dependable Computing and Fault Tolerance in Arcos de Valdevez, Portugal.

Gernot and Ivan Velickovic delivered a seL4 tutorial at the 53rd Annual IEEE/IFIP International Conference on Dependable Systems and Networks (DSN). Gernot also gave a keynote, titled "Intelligent Vehicle Security Needs a Verified Operating System” at the DSN-affiliated Workshop on Safety and Security of Intelligent Vehicles and participated in a panel discussing intelligent vehicle security.

Gernot gave a talk titled “Secure Systems Design on seL4” at the RITICS-Space meeting, organised by Imperial College’s Research Institute in Trustworthy Inter-Connected Cyber-Physical Systems in London, UK.

Gernot attended the 17th Usenix Symposium on Operating Systems Design and Implementation in Boston, USA and participated in the SOSP Program Committee meeting.

Gernot, together with June Andronick, visited UK’s Defence Science & Technology Lab (Dstl) in Salisbury, UK for discussions about the development and deployment of seL4-based systems.

Gernot visited Airbus Defence & Space in Manching near Ingolstadt, Germany for discussions around seL4. (This photo is of Gernot Heiser outside the Airbus site with a Barracuda drone)

Gernot Heiser received ACM award on behalf of team
2023-06-19 – Gernot was in San Francisco last week to accept the ACM Software System award on behalf of the team. More information from our previous news item is below: The Association for Computing Machinery (ACM) has awarded the prestigious ACM Software System Award to TS members Gernot Heiser and Kevin Elphinstone, and others. The ACM Software System Award recognises the development of a software system that has had a lasting influence, reflected in contributions to concepts, in commercial acceptance, or both. It carries a prize of US$35,000. Professor Heiser and his team receive the award for the development of the first industrial-strength, high-performance operating system to have been the subject of a complete, machine-checked proof of functional correctness. A huge congratulations goes out to the whole team: Gernot Heiser, Kevin Elphinstone, University of New South Wales Gerwin Klein, June Andronick, Rafal Kolanski, Proofcraft Harvey Tuch, Google David Cock, ETH Zurich Philip Derrin, Qualcomm Dhammika Elkaduwe, University of Peradeniya Kai Engelhardt, Toby Murray, University of Melbourne Michael Norrish, Australian National University Thomas Sewell, University of Cambridge Simon Winwood, Galois You can read more about it on the UNSW website and the ACM website.

Gernot Heiser received ACM award on behalf of team

Some of the team receiving the ACM SSA award

2023-06-19 – Gernot was in San Francisco last week to accept the ACM Software System award on behalf of the team. More information from our previous news item is below:

The Association for Computing Machinery (ACM) has awarded the prestigious ACM Software System Award to TS members Gernot Heiser and Kevin Elphinstone, and others.

The ACM Software System Award recognises the development of a software system that has had a lasting influence, reflected in contributions to concepts, in commercial acceptance, or both. It carries a prize of US$35,000. Professor Heiser and his team receive the award for the development of the first industrial-strength, high-performance operating system to have been the subject of a complete, machine-checked proof of functional correctness.

A huge congratulations goes out to the whole team:

Gernot Heiser, Kevin Elphinstone, University of New South Wales

Gerwin Klein, June Andronick, Rafal Kolanski, Proofcraft

Harvey Tuch, Google

David Cock, ETH Zurich

Philip Derrin, Qualcomm

Dhammika Elkaduwe, University of Peradeniya

Kai Engelhardt, Toby Murray, University of Melbourne

Michael Norrish, Australian National University

Thomas Sewell, University of Cambridge

Simon Winwood, Galois

You can read more about it on the UNSW website and the ACM website.

TS students honoured in CSE awards
2023-06-19 – Two TS team members have been honoured in the most recent CSE Awards. Patrick Hao has been awarded the Arista Networks COMP9242 Prize. Gordon Tsun Wang Sau has been awarded third place in the Jane Street COMP3141 Prize. A big congratulations to Patrick and Gordon! More information and a full list of winners is here

TS Researchers receive ACM Software System Award
2023-05-05 – The Association for Computing Machinery (ACM) has awarded the prestigious ACM Software System Award to TS members Gernot Heiser and Kevin Elphinstone, and others. The ACM Software System Award recognises the development of a software system that has had a lasting influence, reflected in contributions to concepts, in commercial acceptance, or both. It carries a prize of US$35,000. Professor Heiser and his team receive the award for the development of the first industrial-strength, high-performance operating system to have been the subject of a complete, machine-checked proof of functional correctness. A huge congratulations goes out to the whole team: Gernot Heiser, Kevin Elphinstone, University of New South Wales Gerwin Klein, June Andronick, Rafal Kolanski, Proofcraft Harvey Tuch, Google David Cock, ETH Zurich Philip Derrin, Qualcomm Dhammika Elkaduwe, University of Peradeniya Kai Engelhardt, Toby Murray, University of Melbourne Michael Norrish, Australian National University Thomas Sewell, University of Cambridge Simon Winwood, Galois You can read more about it on the UNSW website and the ACM website.

TS Researchers receive ACM Software System Award

Researchers and developers of the sel4 microkernel

2023-05-05 – The Association for Computing Machinery (ACM) has awarded the prestigious ACM Software System Award to TS members Gernot Heiser and Kevin Elphinstone, and others.