- 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"