Thesis Topic Details

Topic ID:
3210
Title:
Evolvable Trustworthy System
Supervisor:
Gernot Heiser
Research Area:
Industrial Optimization
Associated Staff
Assessor:
Kevin Elphinstone
Topic Details
Status:
Active
Type:
Research
Programs:
CS CE SE
Group Suitable:
No
Industrial:
No
Pre-requisites:
COMP9242 or outstanding result in COMP3231
Description:
The Trusted Platform Module (TPM) specified by the Trusted Computing Group (TCG) and implemented on many PC platforms supports a secure boot and remote attestation (where an external agent can ascertain that the system is in a particular software configuration). However, the TCG approach has been a considered a failure for end-user devices, as it does nothing to ensure that the "trusted" software is trustworthy and does not support upgrading it when it has found to be vulnerable.
The formally-verified seL4 microkernel presents an opportunity to make TPMs useful: seL4 is truly trustworthy, so attesting that it is running provides real assurance of trustworthiness. seL4 itself can then be used to instantiate a trusted software stack, and protect it from untrusted components, and it can be used to upgrade the trusted software securely.

This thesis is to build a demonstrator of an seL4-based, evolvable trustworthy system. This will require implementing TPM-facilitated secure boot of seL4 and some trusted base which can be remotely attested. If time allows, demonstrate secure software evolution.
Comments:
--
Past Student Reports
 
No Reports Available. Contact the supervisor for more information.

Check out all available reports in the CSE Thesis Report Library.

NOTE: only current CSE students can login to view and select reports to download.