About Trustworthy Systems

We use rigorous formal methods to develop trustworthy software systems—systems that come with provable security, safety and reliability guarantees.

• Vision
• Who we are
• Education and research training
• Achievements
• Formal awards
• Contacts

Vision

Our vision is to fundamentally change how software systems are engineered in the real world.

We pursue results that are:

• Relevant: producing software systems that are suitable for real-world use—with high performance as well as protection from realistic threats and failure scenarios.
• Verified: we use world-leading formal methods, based on sound mathematical theories and proofs, to back our claims of trustworthiness.
• Cost-effective: our methods provide better assurance at a lower cost compared to traditional software engineering practices. Much of our research is focused on reducing the cost even further.

We aim to shift the software industry away from ad-hoc, unreliable engineering practices, and towards more principled and trustworthy methods. We would like verified software to become a default choice, especially in safety- and security-critical systems.

We work with government and commercial partners, as well as the broader software engineering community, to drive this change.

Who we are

Trustworthy Systems is a research group at the School of Computer Science and Engineering (CSE) of UNSW Sydney.

Our group consists of about 20 staff and research students and a varying number of undergraduate thesis students and research assistants. Our people come from all over the world and from diverse personal backgrounds.

Education and research training

The Trustworthy Systems group strongly believes in a tight integration of research and education, and consequently has a strategic focus on students, undergraduate as well as postgraudate. We aim at producing graduates with world-class knowledge and skills in our research areas. These graduates power our own research, spread skills to Australian industry, and enhance the group's reputation when taking jobs overseas.

Achievements

Past achievements of the Trustworthy Systems group include:

• Demonstration that complex, real-world high-assurance systems such as autonomous helicopters and autonomous trucks can be built and engineered using formal techniques, based on our verified high-performance platform, the seL4 microkernel.
• World's first formal proof of functional correctness of a complete, general-purpose operating-system kernel, plus a proof that the kernel binary is a correct translation of the C implementation;
• Formal proofs of isolation properties (integrity and confidentiality) of the seL4; together with the above this establishes a complete proof chain from high-level security properties to the kernel binary, making seL4 the first provably secure OS kernel;
• First-ever sound and complete timing analysis of a protected multi-tasking operating system kernel
• Design and implementation of a high-performance capability-based secure microkernel (seL4) that integrates kernel and user resources in the same protection and management framework;
• All recent Apple iOS devices ship with a security processor controlled by a fork of our L4-embedded microkernel;
• A new approach to the design of device drivers which eliminates the majority of typical driver bugs by construction (Dingo);
• A comprehensive approach to accurate energy management via dynamic voltage and frequency scaling that does not rely on pre-characterisation or inaccurate models of the hardware (Koala);
• Highest message-passing performance ever reported on a number of architectures.
• Our spinout company Open Kernel Labs (acquired by General Dynamics in 2012) has deployed OKL4, its descendant of our L4-embedded microkernel, in billions of mobile devices.

Formal awards

• May 2021: Gernot Heiser is included in the ACM Distinguished Speakers list
• February 2021: Gernot Heiser with ETH Zurich co-authors wins the Best Paper Award at DATE'21 for their paper Microarchitectural Timing Channels and their Prevention on an Open-Source 64-bit RISC-V Core.
• October 2019: TS researchers win the ACM SIGOPS Hall of Fame Award for their landmark paper seL4: Formal Verification of an OS Kernel published at SOSP 2009.
• June 2019: Johannes Åman Pohjola wins the Best Paper award at FORTE'19 for his paper Psi-calculi revisited: Connectivity and compositionality.
• April 2019: TS PhD student Qian Ge and co-authors, including Gernot Heiser, win the Best Paper Award at EuroSys 2019 for their paper Time protection: The missing OS abstraction.
• January 2019: TS Alumnus Thomas Sewell wins the John Makepeace Bennett Award for the Australasian Distinguished Doctoral Dissertation, awarded annually by the Computing Research and Education Association of Australasia (CORE). His dissertation produced the binary translation toolchain that is a core part of seL4's verification story.
• August 2018: TS PhD student Qian Ge and co-authors, including Gernot Heiser, win the Best Paper Award at APSys'18 for their paper No security without time protection: We need a new hardware-software contract.
• June 2017: The Cross-Domain Desktop Compositor (CDDC), developed in a collaboration of TS with DST Group wins the national iAwards in two categories:
  1. Infrastructure & Platforms Innovation of the Year
  2. Research & Development Project of the Year.
  The iAwards are an annual program of the Australian Information Industry Association (aiia) that recognises and rewards technology innovations that have the potential to, or are already having, a positive impact on the community.
• November 2016: Gernot Heiser is inducted to the Australian Academy of Technology and Engineering (ATSE).
• July 2016: First place to Adam Walker in SyntComp'16 with Simple BDD Solver, third year in a row, and second place to Alex Legg with TermiteSAT in the parallel execution track.
• April 2016: Thomas Sewell, Felix Kam, and Gernot Heiser win Outstanding Paper Award for 'Complete, High-Assurance Determination of Loop Bounds and Infeasible Paths for WCET Analysis' at RTAS'16.
• January 2016: Gernot Heiser is named an IEEE Fellow.
• July 2015: First place to Adam Walker in SyntComp'15 with Simple BDD Solver, second year in a row.
• March 2015: Rob van Glabbeek is elected "foreign member" of the Royal Holland Society of Sciences and Humanities
• December 2014: Gernot Heiser is made a Fellow of the ACM.
• November 2014: David Cock wins the CiSRA best student research paper award for The Last Mile, an empirical study of timing channels on seL4.
• September 2014: Engineers Australia names Gernot Heiser their Entrepreneur of the Year.
• July 2014: First place to Adam Walker in SyntComp'14 with Simple BDD Solver
• June 2014: Engineers Australia lists Gernot Heiser as one of the Top-100 Most Influential Engineers
• April 2014: Bernard Blackham wins the 2013 ACM SIGBED Paul Caspi Memorial Dissertation Award.
• January 2014: Bernard Blackham wins the John Makepeace Bennett Award for Australasian Distinguished Doctoral Dissertation.
• July 2013: Aaron Carroll wins the Best Student Paper Award at APSys'13 for The Systems Hacker's Guide to the Galaxy: Energy Usage in a Modern Smartphone.
• April 2013: Bernard Blackham and Gernot Heiser win the RTAS'13 Best Paper Award for Sequoll: a Framework for model checking binaries.
• December 2012: Gernot Heiser and Kevin Elphinstone jointly win UNSW's Vice Chancellor's Award for Teaching Excellence for their Advanced Operating Systems course.
• September 2012: Best paper award at FM'12 for Decentralised LTL Monitoring
• October 2011: CISRA Project Prize to Anna Lyons
• October 2011: Goanna was evaluated as the leading static analysis tools detecting more than twice as many serious bugs as the next best published competitor. Report on the Third Static Analysis Tool Exposition (SATE 2010), NIST Special Publication 500-283, Oct 2011
• August 2011: June Andronick wins the MIT TR-35 for the 35 young innovators under 35 who are tackling important problems in transformative ways.
• April 2011: The verified seL4 kernel makes the MIT TR-10, the world's top ten emerging technologies in 2011.
• Aug 2010: Innovation Hero Award by Sydney University's Warren Centre for Advanced Engineering for Gernot Heiser
• Feb 2010: NICTA's Richard A Newton Impact Award for Research Excellence to the seL4 and L4.verified team for the formal verification of the seL4 microkernel.
• October 2009: Best-Paper Award at SOSP'09 for seL4: Formal verification of an OS kernel
• September 2009: Gernot Heiser wins the Engineering, Mathematics and Computer Sciences Category of the NSW Scientist of the Year 2009 Award
• August 2008: ACSAC'08 Best Paper Award for Pre-virtualization: Soft layering for virtual machines
• May 2008: NICTA's Richard A Newton Impact Award for Research Excellence to Gernot Heiser for research leading to the creation of Open Kernel Labs
• November 2007: CISRA Award for best research paper to ERTOS PhD student Harvey Tuch
• May 2007: iAward, Category Applications and Infrastructure Tools to Gernot Heiser by the Australian Information Industry Association (AIIA)
• April 2005: USENIX'05 Best Student-Paper Award for Itanium—a system implementor's tale

Contacts

On the Contacts page.