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, conjoint staff from aligned companies, and collaboration partners at the Australian National University, the University of Melbourne, and the University of Adelaide. In addition we have a 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.

Systems

The project pages here refer to a number of systems we are working on. This is a short overview of them, with links to more information.

seL4

... is our formally verified, high-performance, microkernel. Most of our work uses seL4. Maintaining and extending seL4 is a cooperative effort between systems and formal methods practitioners, with significant input from PhD and Honours students.

Linux

... needs no introduction. It is a second focus point of the group's research. Some successes include the design and implementation of fast context switching on the StrongARM processor (50 times faster than in standard Linux), and removal of the 2TB Filesystem limit.