Trustworthy Systems Research Group @Data61
We will fundamentally change the way real-world software systems are built and engineered, with their trustworthiness assured to the highest degree possible — the certainty of mathematical proof — while being cheaper than traditional low- to medium-assurance systems.
High-assurance software means software for which we can give strong evidence (mathematical proof) that the software will do what it is supposed to do and nothing more. Such software does exist, but it is widely thought prohibitively expensive, and typically lacks performance as well as features.
Formally verified high-assurance software for the price of low assurance will fundamentally change how critical software is developed, and it will fundamentally change what critical software can do for humanity. Currently such software needs to be simple — we dare not make it too complex, because we cannot predict what it will do. If this changes, more intelligence and complexity can be brought to bear on making critical systems safer and more resilient.
Trustworthy software is also the foundation for fundamentally solving one of the core parts of the cybersecurity problem: Almost all present attempts at solving cybersecurity must lose in the long term, because they represent a race between attacker and defender where the attacker has the advantage. These include:
- Attempts to retrofit security or safety into systems not designed for them do not work. Instead, security and safety are software architecture and design properties.
- Reactive approaches (from malware scanners to intrusion detection) are a losing proposition, which accept that breaches happen in the first place and leave the defender at a disadvantage. We have demonstrated that it is possible to stop attacks, not just to react to them.
- Much of present security work targets symptoms, rather than underlying causes. For instance, patching vulnerabilities as they are discovered necessarily has the attacker at an advantage -- they need to only find one vulnerability, whereas the defender has to patch all. Formal proof is the only method that provides completeness of security analysis for specific properties and reduces attack vectors to well-defined assumptions.
Radically different, rigorous approaches are required for achieving real trustworthiness, which includes security, safety and dependability: systems must be built for trustworthiness from the ground up, and we must be able to give strong evidence, such as mathematical proof, that trustworthiness is achieved. This will only work in practice if it can be achieved without a complete rewrite — legacy system architectures must be morphed into inherently secure ones.
We have demonstrated that trustworthy software systems can be built and high assurance can be reached in real-world applications. The aim for the future is to achieve full trustworthiness with end-to-end theorems and wide-spread use of trustworthy (as opposed to just trusted) software.
The Trustworthy Systems team 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.
Past achievements of the Trustworthy Systems team 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 has deployed OKL4, its descendant of our L4-embedded microkernel, in billions of mobile devices.
- 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
On the Contacts page.