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 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:
- Infrastructure &
Platforms Innovation of the Year
- 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
On the Contacts page.