Skip to main content

About Us

Trustworthy Systems Research Group @Data61

Vision

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.

We build on our widely deployed kernel technology and systems research, as well as our expertise in applied formal methods, illustrated by the seL4 microkernel and its formal proof of correctness

Research Training

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.

Achievements

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.

Formal awards

Contacts

On the Contacts page.

Served by Apache on Linux on seL4.
Served by Apache on Linux on seL4.