Thesis Topic Details

Topic ID:
3215
Title:
Formal functional specification of security critical component in Isabelle/HOL
Supervisor:
June Andronick
Research Area:
Formal Methods, Operating Systems
Associated Staff
Assessor:
Gerwin Klein
Topic Details
Status:
Active
Type:
Research
Programs:
CE BIOM BINF SE
Group Suitable:
Yes
Industrial:
No
Pre-requisites:
Good background in formal logic is essential. Experience with Isabelle preferable.
Description:
A prototype of a secure networking switch system has been built on the seL4 microkernel. The system securely isolates network communication of classified information. A high level security model of the system has been defined in Isabelle/HOL and it has been proved that, at this model level, no data could flow from one network to another. The proof relies on the correctness of the only trusted component of the system (a part from the kernel itself). In other words, it relies on the assumption that the C code of the component in the prototype refines its high level security model.

The aim of the project is to tackle the first main step in validating this assumption: providing a more detailed functional specification of the component, as an intermediate level between the C code and the high-level security model.
Comments:
You will work as part of a significant research project with a team of international PhD students and researchers at NICTA Kensington.
Past Student Reports
  Nelson Mandela BILLING in s2, 2011
Formal functional specification of security critical component in Isabelle HOL
 

Download report from the CSE Thesis Report Library

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