Honours Thesis Projects
Introduction
The thesis topics listed here are available to strong final-year undergraduate students. They are mostly associated with research projects and generally quite challenging; many topics have the potential to lead to a publication, and in average we get about one paper a year from the work of one (or more) undergraduate thesis students. Students who are not aiming for excellence are in the wrong place here.
We guarantee a thesis topic to any student who has obtained a HD grade in UNSW's Operating Systems or Advanced Operating Systems course, no matter what their other grades are! This does not mean that an OS HD is a prerequisite, but we do expect our students to have s strong track record in relevant courses.
Strong computer Science Honours students may qualify for the John Lions Computer Science Honours Award.
Note that the below list is constantly updated, new topics are added as we identify them as work on various research projects proceeds. Topics marked are recent additions.
- Topics supervised by Gernot Heiser
- How to apply
- Info for students looking for a special project (COMP3901/3902)
- Info for postgraduate coursework students
Present topics supervised by Gernot Heiser (official list)
-
Core management in Lions OS
A processor core consumes energy, whether it is doing useful work or not, unless it is in a “deep sleep” state. Transitioning into or out of such sleep states takes time (and energy), making a pure core-local energy management inefficient. Instead the OS should aim to maximise the period cores are in deep sleep. This requires monitoring overall CPU utilisation, and off-lining lowly utilised cores by migrating their activities to other cores.
The structure of Lions OS supports this approach: It has a highly modular design, with individual modules strictly sequential (executing on a single core) and modules communicating via shared memory, synchronised by semaphores. This means most modules are completely location transparent and can easily be migrated to a different core.
The aim of this thesis is to design and implement the mechanisms for core migration in the seL4 Microkit, which is the framework in which Lions OS is implemented. Depending on progress, the next step would be to implement a core manager, which monitors load an consolidates or spreads activities as required by load.
-
Native high-performance file-system API for seL4
The seL4 device driver framework (sDDF) provides a high-performance I/O framework for seL4. A fairly mature networking interface (that outperforms Linux) has been developed in this framework.
This project is to rethink the I/O API for seL4-based systems that interfaces to a native or virtualised storage back-end and minimises overheads. While the primary API does not need to be Posix-like, eg is likely asynchronous, a Posix-like wrapper should be provided for those who prefer to use this inefficient model.
The project is to develop such a system, perform detailed evaluation of performance against a native Linux baseline, and perform a security assessment.
-
PD Templates for the Microkit
The seL4 Microkit is a minimal abstraction layer on top of seL4 that vastly simplifies the programming model (at the expense of reducing the application domain to cyberphysical/embedded/IoT systems). It comes with an SDK that further simplifies its use. The Microkit forms the basis of Lions OS, a high-performance, adaptable and verifiable OS for cyberphysical systems under development at TS.
The Microkit (and Lions OS) intentionally require a static system architecture: all modules and their possible interactions are known at system build time. But this should not require that all code running on the system needs to be known in advance. There is a need for PD templates, which are slots with pre-defined (mandatory) access rights and resource allocations in which a program can be loaded at run time. Furthermore, it should be possible to degrade the predefined (maximum) access rights to a smaller set of (discretionary) rights authorised for the specific program to be loaded.
To support such PD templates, the following is needed:
- Templates are left uninitialised at system startup time;
- at PD start time, the actual PD is set up with the rights and resources of the template;
- the PD is made to execute a trusted loader program, passing it the path of the executable that is meant to run in the PD;
- the loader reads a signed privileges section in the program to be loaded, and removes any access rights not explicitly authorised;
- the loader then loads the program, sets it up for execution, and unloads itself.
The project is to design, implement and evaluate this PD template support for the Microkit.
-
Driver VMs: Re-use of unmodified Linux device drivers in seL4
While seL4 drivers for performance- or security-critical devices are best written from scratch, and the seL4 device driver framework (sDDF) makes this relatively easy, re-writing all drivers is neither feasible nor necessary, given the wealth of drivers available in Linux. We are therefore interested in re-using unmodified Linux drivers, by encapsulating each Linux driver into an individual driver VM. Such a VM will run a minimal Linux guest that contains little more than the driver to be re-used. It makes use of the Linux virtIO interface.
The challenge is to integrate such a driver VM seamlessly into the sDDF in a way that is performant without the rest of the system having to trust the driver to behave correctly. Give the large size of the Linux code base, such a driver must be considered malicious, and it must be prevented, by design, to cause more damage than denial of service.
The project is to develop such a driver VM framework for one or more device classes, perform detailed evaluation of performance against a native Linux baseline, and perform a security assessment.
Jointly supervised with Peter Chubb
-
Secure OS for Sunswift
This topic is to evaluate requirements on an operating system for the Sunswift solar racing car, and design and implement such a system on the seL4 Core Platform. The project will done in close collaboration with Sunswift developers and will support/prototype a number of real Sunswift subsystems. Design work includes a threat analysis and effective passive defences against cyber attacks.
-
Optimise seL4 multicore IPC
performance
IPC on single-core seL4 is highly optimised. On multicore systems, IPC should only be used intra-core, and that case should ideally be no slower than single-core. In particular, concurrent IPCs running on different cores should not interfere. In practice, IPC operates inside the kernel lock, which leads to artificial contention (and thus performance degradation) and slows down even the uncontented case.
This project is to investigate the changes needed to take the IPC fastpath outside the kernel lock, and optimise and evaluate performance. Of particular concern are the exact conditions under which IPC can be performed outside the lock, and what is needed to ensure this is safe, considering that IPC operations from callers on different cores to a passive server will compete for the endpoint. A design that completely removes cross-core IPC from the API is a valid option.
-
Optimise/develop IRQ fast-path in seL4
Project allocated!
Most topics can lead to publications.
How to apply:
Contact the relevant supervisor.
Note for OS related topics: We promise a thesis topic to every interested student who has obtained a HD grade in COMP3231/COMP9201 Operating Systems or COMP9242 Advanced Operating Systems. If necessary we will define additional topics to match demand.
We will not turn down any students doing exceptionally well in OS courses. However, this does not mean that an HD in OS or Advanced OS is a prerequisite for doing a thesis with me. Interested students with lower OS marks are welcome to talk to me if they feel they can convince me that they will be able to perform well in an OS thesis.
Keep in mind that these topics are all research issues and generally at the level of Honours Theses. They are not suitable for marginal students or students with a weak understanding of operating systems. We expect you to know your OS before you start.
Topics for a Special Project (COMP3901/3901):
Some undergraduate thesis topics are also suitable for a special project (typically with reduced scope/expectations). But generally Taste of Research topics are a better match for this. Talk to us if you're interested!
Information about research theses
Postgraduate thesis topics:
Undergraduate thesis topics are also suitable for coursework Master's projects. Same conditions apply: You must have a pretty good track record in OS courses for OS and FM related topics.