From d3d6c204ec7db982293b0bc54418b201d0145191 Mon Sep 17 00:00:00 2001 From: "b@brck.nl" Date: Wed, 4 Nov 2026 12:01:10 +1100 Subject: [PATCH] update ongoing research update ongoing research - ts Signed-off-by: b@brck.nl --- Research/ongoing.html | 39 ++++++++++++++++++++++++++------------- 1 file changed, 26 insertions(+), 13 deletions(-) diff --git a/Research/ongoing.html b/Research/ongoing.html index 8e2f7f056..276281755 100644 --- a/Research/ongoing.html +++ b/Research/ongoing.html @@ -32,21 +32,34 @@ Heiser

- Trustworthy Systems (TS) is a research group in the School of Computer - Science and Engineering (CSE) at UNSW Sydney. TS works on building highly - secure operating systems for the real world. Their approach is based on - highly principled designs that support the use of rigorous formal methods to - ensure security and reliability without compromising performance. + The Trustworthy Systems (TS) group aims to make truly secure and safe + operating systems a reality. As a direct successor of the team that + originally created and verified seL4, it is focussed on principled and + verifiable seL4-based OS designs that achieve unprecedented security for + real-world systems without compromising performance.

- Currently, TS's main activities are: Time protection, a principled, - fundamental approach for the systematic prevention of timing channels and - its implementation and verification in seL4; LionsOS, an seL4-based, fast, - secure and adaptable operating system for embedded and cyber-physical - systems; Pancake, a new low-level programming language designed to enable - the implementation and verification of low-level systems code, such as - device drivers; the design of a provably-secure seL4-based general-purpose - OS. + TS’s approach is to re-think and re-develop system architecture from + scratch, using fine-grained modularity, strict separation of concerns and + radical simplicity. TS also contributes to on-going development of seL4, + evaluating and improving kernel performance, and adding missing features + required by real-world systems. +

+

+ TS’s current main activities are time + protection – hardware and kernel mechanisms for principled prevention of + microarchitectural timing channels, LionsOS, a + statically architected, provably-secure, deployable OS for + embedded/cyberphysical systems, Pancake, a + verification-friendly systems programming language with a verified compiler + that is used for implementing and verifying LionsOS, and Djawula, a + proof-of-concept of a general-purpose OS that can be proved to enforce a + fairly arbitrary security policy. TS open-sources all project code and + proofs.

' link="https://trustworthy.systems"