Thesis Topic Details
Topic ID: |
3265 | |
Title: |
Noninterference Models for Systems with Trusted Components | |
Supervisor: |
Toby Murray | |
Research Area: |
Formal Methods, Security | |
| Associated Staff | ||
|---|---|---|
Assessor: |
Gerwin Klein | |
| Topic Details | ||
Status: |
Active | |
Type: |
Research | |
Programs: |
CS CE BIOM BINF SE | |
Group Suitable: |
No | |
Industrial: |
No | |
Pre-requisites: |
The ideal candidate has some experience with formal methods and security, and ideally has experience with Isabelle/HOL. | |
Description: |
This project involves extending traditional models of noninterference to systems that contain trusted components, whose behaviour is relied upon in order to enforce security. Noninterference is a security property that is satisfied by a system when its low-classification components can learn nothing about its high-classification inputs, state and actions. Traditional models and noninterference definitions assume that all components within the system are potentially malicious and act arbitrarily, in that they may perform any action they have the authority to perform. For this reason they are ill-suited to systems that contain trusted components, who have the authority to violate the system's security property but are trusted not to do so. These kinds of systems are becoming more common as high-security systems become more mainstream. In particular, systems that change their security configurations at runtime, in response to user actions, rely on trusted components to accurately carry out the user's requests, and remain secure only when their trusted components behave as expected. Reasoning about noninterference in such systems requires a noninterference model that takes into account the actual behaviour of these trusted components. This project involves extending traditional models of noninterference to produce such a model, with specific application to the seL4 microkernel whose primary application domain is to support systems containing trusted components that it isolates from the system's untrusted ones. Any such extended noninterference framework would explicitly model the behaviour that each trusted component is relied upon to exhibit, and would likely involve developing invariants that would be proved of such components' behaviour in order to guarantee that noninterference holds for a whole system in which they are contained. Work currently in progress will yield a (traditional) noninterference theorem for the seL4 microkernel. It is hoped that this project would enable us to extend this theorem to systems containing trusted components. |
|
Comments: |
You will work in an international group of PhD students and researchers within the Trustworthy Systems project, at the Sydney/UNSW Laboratory, of NICTA. | |
| 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. |
||