Trustworthy Systems Research Group @Data61
We will change the practice of design and implementation of software systems, by enabling affordable, routine design and implementation of large and complex software, with strong whole-of-system guarantees for safety- or security-critical systems and integrated, adaptive architectures that directly address business needs for enterprise ecosystems.
The strong trend towards more complexity and at the same time more reliance on software systems is unbroken and accelerating. In the embedded space, this leads to immediate safety and security concerns. In the enterprise space, the need for integration, adaptability, and business platforms is already a major factor for business impact. Mobile devices with security requirements and enterprise applications with evolving adaptation needs are connecting both problem spaces and further compound the problem. Over the whole spectrum there is a strong need to develop and deploy trustworthy software quickly and cost effectively.
Data61's Trustworthy Systems Research Group aims to achieve fundamental, game-changing improvements in the design, implementation, and verification of software systems scaling from the embedded to the enterprise space. We will apply rigorous techniques at various abstraction levels of software systems, to achieve solid and practically meaningful guarantees, for provable security, safety, and reliability properties of critical systems.
We build on our widely deployed kernel technology and systems research, and proven world-class expertise in applied formal methods, illustrated by the seL4 microkernel and its formal proof of correctness.
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:
- 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
- Two papers accepted to SOSP'09 (including a best-paper award). These are the first papers from Australia in the 42-year history of the top OS conference;
- 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.