Skip to main content

About Us

Trustworthy Systems Research Group @Data61

Vision

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

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:

  • 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.

Formal awards

Contacts

On the Contacts page.