Student Projects General Information
The Group and its Working Environment
Operating Systems and Formal Methods
The projects advertised on these pages are set within the Trustworthy Systems research group at UNSW, one of the foremost operating systems and formal methods research groups in the world.
Our research activities extend from embedded systems via microkernels through virtualization to general issues of system architecture and system security. The group is also interested in the investigation of architectural support for operating systems and languages. The group is well networked internationally and has collaborations and exchanges of visits with many leading private- and public-sector systems research groups.
One key feature of our group is that formal methods and operating systems practitioners work closely together.
Key research challenges now involve how to deal with concurrency in formal proofs; development of new ways to build reliable and trustworthy systems (including using new languages and language run-times), and ways to design systems that can have have provable system-level properties, while not having every line of code formally verified.
The group consists of about half a dozen UNSW academic staff, and a number of adjunct academics from universities we collaborate with. In addition we have a large number of full or part-time engineering/support staff (research assistants and engineers, some PhD qualified), PhD students, and a undergraduates and coursework Masters students.
We are well-equipped with state-of-the-art computing equipment, and have experience with a large range of computer architectures, especially x86, Arm and RISC-V. We have facilities for designing and building new hardware where necessary for research.
Trustworthy Systems research outcomes are being deployed in commercial products across defence, critical infrastructure, medical devices and autonomous vehicles.
Main Research Projects
Most of our research is around the seL4 microkernel we developed, the world's first protected-mode OS kernel with a proof of implementation correctness, followed by proofs of security enforcement and real-time properties. seL4 is still the world's most highly assured OS kernel.
Our research continues to improve seL4 and its assurance story (especially the prevention of information leakage through microarchitectural timing channels. But most of our research is on building and verifying complete systems based on seL4, combining system architecture, programming language support and improvement of verification techniques.
The full list of our main current (and past) research projects is on our projects page; almost all student projects are part of one of those.