24-credit only
The seL4 microkernel is the only formally verified microkernel and has significant interest from Defence in Australia, the US and the UK for providing a secure platform for military systems. Keeping the verification up-to-date with current hardware trends requires a deep analysis of the code and an understanding of microarchitectural features. This project will involve choosing key data structures and operating system services that may be impacted by emerging processors, and potentially identifying vulnerabilities in current software. The topic is part of a Defence-funded project involving researchers at UQ, ANU, and DSTG.