Concurrent Data Structure

Picture of Peter Hoefner

17 Apr 2024

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.

You are on Aboriginal land.

The Australian National University acknowledges, celebrates and pays our respects to the Ngunnawal and Ngambri people of the Canberra region and to all First Nations Australians on whose traditional lands we meet and work, and whose cultures are among the oldest continuing cultures in human history.

arrow-left bars search times