Thesis Topic Details

Topic ID:
3350
Title:
Separation Logic for OS Specifications
Supervisor:
Gerwin Klein
Research Area:
Formal Methods, Operating Systems
Associated Staff
Assessor:
June Andronick
Topic Details
Status:
Active
Type:
R & D
Programs:
CS CE BIOM BINF SE
Group Suitable:
No
Industrial:
No
Pre-requisites:
COMP4161
Description:
The aim of this topic is to investigate if and how separation logic is suitable for specifying high-level functional properties of an operating system kernel.

The L4.verified project has proved correctness of the C implementation of the seL4 microkernel with respect to an abstract operational specification. While this specification provides a good interface to higher-level proofs about the kernel, it is not convenient to use for proofs about user-level programs that interface with the kernel. Current Hoare logic properties shown about this kernel mostly concern invariant preservation or security, less abstract functional properties. The thesis is that separation logic provides a more convenient framework for specifying such properties.

The expected outcome is a new specification of seL4 in separation logic and a proof in Isabelle/HOL that a suitable existing specification layer of seL4 implements that specification.
Comments:
The work on this topic is part of NICTA's Trustworthy Systems project. More detail on this project is available at http://ssrg.nicta.com.au/projects/TS/
Past Student Reports
  Callum BANNISTER in s1, 2013
Separation Logic for OS Specifications
 

Download report from the CSE Thesis Report Library

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