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 Data61, the largest and most active Operating Systems research group in the southern hemisphere and the Asia-Pacific region and one of the foremost 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.
In 2017 we have fourteen full time research staff, all conjoint Data61 and university appointments (most UNSW, but also ANU, University of Melbourne, and University of Adelaide), twenty-three full or part-time engineering/support staff (research assistants and engineers, some PhD qualified), eight PhD students, and a varying number of undergraduates and Masters of Engineering students.
We are well-equipped with state-of-the-art computing equipment, and have experience with a large range of computer architectures, from ARM to Itanium. We have facilities for designing and building new hardware where necessary for research.
Trustworthy Systems research outcomes are being deployed in commercial products, and the group has a track record of getting Linux kernel patches accepted.
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.
... 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.
... 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.
... is a real-time operating system (RTOS) targetted at microcontrollers without an MMU. It is a static RTOS that also has a formal model and has been the target of some verification.
... is an extremely small and high-performance operating system microkernel, and predecessaor to seL4. There are various variants of L4 under active development, a list of these is maintained at L4HQ. The TS group has in the past implemented the first 64-bit version (on MIPS, still holds the performance record for single-issue CPUs) and the first multiprocessor version (on Alpha) of this kernel. We no longer work on L4, but focus on seL4