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 | ||
| 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. |
||