About Trustworthy Systems
We use rigorous formal methods to develop trustworthy software systems—systems that come with provable security, safety and reliability guarantees.
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 of Data61 in CSIRO.
Our group consists of about 40–50 people from all over the world and diverse personal backgrounds.
Our primary office is at the UNSW campus in Sydney, Australia.
Education and research training
The Trustworthy Systems group strongly believes in a tight integration of research and education, and consequently has a strategic education agenda, aimed 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 Data61's and their university'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
- November 2016: Gernot Heiser is inducted to the Australian Academy of Technology and Engineering (ATSE).
- October 2016: Distinguished Paper of OOPSLA 2016 for 'Hybrid STM/HTM for nested transactions on OpenJDK' to Keith Chapman, Tony Hosking, and Eliot Moss.
- October 2016: ACM SIGPLAN Most Influential Paper of OOPSLA 2006 for ‘The DaCapo benchmarks: Java benchmarking development and analysis’ to S. M. Blackburn, R. Garner, C. Hoffmann, A. M. Khan, K. S. McKinley, R. Bentzur, A. Diwan, D. Feinberg, D. Frampton, S. Z. Guyer, M. Hirzel, A. Hosking, M. Jump, H. Lee, J. E. B. Moss, A. Phansalkar, D. Stefanovic ́, T. VanDrunen, D. von Dincklage, and B. Wiedermann
- 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 got made "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
- July 2008: Jens-Wolfhard Schicke wins the ICE'08 Best student/young researcher paper award for "Symmetric and asymmetric asynchronous interaction".
- 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)
- November 2005: Best Paper Award at WICSA'05 for Customized Benchmark Generation Using MDA
- April 2005: USENIX'05 Best Student-Paper Award for Itanium—a system implementor's tale
Contacts
On the Contacts page.