Skip to main content
CSIRO Logo Data 61 logo

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

Contacts

On the Contacts page.