Project Title
Making it real: seL4 security proofs.
Name of Academic Supervisor
Gerwin Klein
Email of Academic Supervisor
gerwin.klein@nicta.com.au
Name of Joint Supervisor(s)
Dhammika Elkaduwe
Email of Joint Supervisor(s)
dhammikae@cse.unsw.edu.au
CSE or NICTA Project
NICTA
Research Area
Formal Methods
Abstract of Research Project
The L4.verified project has recently completed a mechanically verified security analysis of the seL4 micro kernel. As is usual in the literature, this security analysis works on a high, abstract level. The project has also completed a precise specification of the seL4 API and is in the process of verifying that the C code running on hardware correctly implements this API. It is the task of this summer project to formally connect the two levels such that the security proof in the end fully applies to the C code. This is an ideal project to become familiar with the area of formal security proofs and can be developed into a thesis project.
You will work with and be guided by an international research project with a group of PhD students and researchers in Formal Methods and Operating Systems.
Novelty and Contribution
Even in high security software certification, security proofs usually only work on high level models. This summer project, together with the rest of the L4.verified project, would achieve one of the first security proofs that formally connects to real code.
Expected Outcomes
A formal mapping of operations in the seL4 API to the security model together with a relation mapping concrete API states to abstract security states. Optionally, a formal proof in the Isabelle/HOL theorem prover, on one or more API operations that they preserve the above mapping.
Reference Material/Links
http://www.ertos.nicta.com.au/research/l4.verified/ - the L4.verified project.
http://mirror.cse.unsw.edu.au/pub/isabelle/ - the Isabelle/HOL interactive theorem prover.
Project Title
Integrating Separation Logic Decision Procedures in Isabelle/HOL
Name of Academic Supervisor
Gerwin Klein
Email of Academic Supervisor
gerwin.klein@nicta.com.au
Name of Joint Supervisor(s)
Harvey Tuch
Email of Joint Supervisor(s)
htuch@cse.unsw.edu.au
CSE or NICTA Project
NICTA
Research Area
Formal Methods
Abstract of Research Project
Separation logic provides a concise specification language for pointer-based programs. As part of the L4.verified project we have developed a state-of-the-art C verification tool that supports specifications in this logic, based on the interactive theorem prover Isabelle/HOL. In the literature a number of decision procedures that are able to automatically verify some properties exist for fragments of separation logic. The objective of this work is to identify the C fragments that are applicable and to implement some of these decision procedures in our framework. This project is an integral and important part of the verification of the L4 microkernel at NICTA. You will work with the developers of L4 and Isabelle in an international team of PhD students and researches in the NICTA Embedded, Realtime and Operating Systems program and the NICTA Formal Methods program.
Novelty and Contribution
This work addresses the often neglected problem of verifying full correctness properties of software written in system languages such as C. A successful outcome will provide a contribution in the understanding of how interactive verification techniques can benefit from decision procedures in systems software verification.
Expected Outcomes
Implementation of one or more decision procedures and a demonstration of combination with tactical proofs in Isabelle/HOL. There is also scope for investigating new decision procedures for experienced students.
Reference Material/Links
http://nicta.com.au/research/projects/l4.verified/ - the L4.verified project
Project Title
User interface design for a high-performance, retargetable architectural simulator.
Name of Academic Supervisor
Gerwin Klein
Email of Academic Supervisor
gerwin.klein@nicta.com.au
Name of Joint Supervisor(s)
David Cock
Email of Joint Supervisor(s)
david.cock@nicta.com.au
CSE or NICTA Project
NICTA
Research Area
Formal Methods
Abstract of Research Project
The aim of this project is to develop a user interface for debugging system-level code in our locally-developed retargetable architectural simulator. You will evaluate the available options (Eclipse plugin – www.eclipse.org vs. Custom-built GUI), take into account usability requirements, and then deliver a frontend module to integrate with the existing (Python based) runtime framework.
You will be working with an international project team (l4.verified/seL4), which is undertaking cutting-edge research in high reliability embedded systems.
Novelty and Contribution
When successfully completed, it is intended that this frontend will be used in the low-level implementation of the next-generation secure microkernel seL4, as well as on other embedded systems work within NICTA, and be included in a publicly-released open-source version.
Expected Outcomes
- Evaluation of interface options for system-level debugging
- Development of a user-interface frontend according to evaluation results
Reference Material/Links
Project Title
Formal specification of software for component connection
Name of Academic Supervisor
Rob van Glabbeek
Email of Academic Supervisor
Robert.vanGlabbeek@nicta.com.au
Name of Joint Supervisor(s)
Email of Joint Supervisor(s)
CSE or NICTA Project
NICTA
Research Area
Formal Methods
Abstract of Research Project
Component systems are gaining traction in the embedded systems space. The CAmkES project has developed such a component system for the L4 microkernel and this summer project aims to bring formal modelling to bear on such CAmkES systems.
The task is: Given an informal specification of software for connecting components, turn this into a formal specification that is more suitable for formal verification of desirable properties. Document the design decisions that lead to the formal specification and validate them in terms of the informal specification.
Novelty and Contribution
This project is one of the first steps of enabling full formal verification on component systems.
Expected Outcomes
A small case study on formalising a specific component system.
Reference Material/Links
http://www.ertos.nicta.com.au/research/camkes/ - the CAmkES project
Project Title
Isabelle Enhancements
Name of Academic Supervisor
Gerwin Klein
Email of Academic Supervisor
Gerwin.Klein@nicta.com.au
Name of Joint Supervisor(s)
Simon Winwood
Email of Joint Supervisor(s)
sjw@cse.unsw.edu.au
CSE or NICTA Project
L4.Verified
Research Area
Formal methods
Abstract of Research Project
Large verification projects can benefit from improved tool support for 'proof engineering', i.e., utilities to manage the complexity of large numbers of proofs. This project will involve developing such utilities as extensions to the Isabelle theorem prover. Initially, this project will develop a tool to track forward dependencies for theorems such that the user can find out which theorems potentially need to be reproved when a particular lemma or definition changes. The basic tracking information for this already exists in Isabelle. The task is to interpret this information correctly and print it in human readable form.
This project is ideal to get to know the internals of a leading edge interactive theorem prover.
Novelty and Contribution
This project will contribute to the usefulness of Isabelle in large projects.
Expected Outcomes
Implementation of proof engineering tools for managing large proofs.
Reference Material/Links
http://www.ertos.nicta.com.au/research/l4.verified/ - the L4.verified project.
http://mirror.cse.unsw.edu.au/pub/isabelle/ - the Isabelle/HOL interactive theorem prover.
Project Title
Smart VCG: Automation of Monadic Hoare Logic
Name of Academic Supervisor
Gerwin Klein
Email of Academic Supervisor
Gerwin.klein@nicta.com.au
Name of Joint Supervisor(s)
Thomas Sewell
Email of Joint Supervisor(s)
tsewell@cse.unsw.edu.au
CSE or NICTA Project
NICTA
Research Area
Formal Methods
Abstract of Research Project
This project aims to develop an automatic tool that will simplify the proving of monadic hoare problems. Given a precondition, postcondition, and monadic program, such a problem requires a proof that the postcondition is satisfied after the program runs on any state satisfying the precondition.
The L4.verified has encountered many such problems. Although the theoretical approach required is well-known, implementing this approach well is an interesting pragmatic problem. Currently, our locally developed tools require significant unnecessary manual intervention. Such intervention could be eliminated with a carefully crafted tool, yielding simpler and more elegant proofs.
You will work in an international research project with a group of PhD students and researchers in Formal Methods and Operating Systems.
Novelty and Contribution
Although the theoretical background of this task is well explored, there is plenty of room for pragmatic contribution. Techniques and algorithms discovered would be of significant interest in the applied formal methods community.
Expected Outcomes
The expected outcome is the development of one or more automated tools useful in solving monadic hoare problems.
Reference Material/Links
http://www.ertos.nicta.com.au/research/l4.verified/ - the L4.verified project.
http://mirror.cse.unsw.edu.au/pub/isabelle/ - the Isabelle/HOL interactive theorem prover.
Project Title
Error Trace Generator for Static Program Analyser
Name of Academic Supervisor
Dr Ansgar Fehnker
Email of Academic Supervisor
ansgar.fehnker@nicta.com.au
Name of Joint Supervisor(s)
Dr Ralf Huuck
Email of Joint Supervisor(s)
ralf.huuck@nicta.com.au
CSE or NICTA Project
NICTA
Research Area
Formal Methods
Abstract of Research Project
The goal of the Goanna project is to improve the quality of system software by automatically detecting software defects (bugs). Our prototype tool analyses C/C++ source code and prints warnings much like compilers do, i.e. it tells to programmer that a certain property is violated in a specific line of the source code.
The goal of this summer project is to improve the tool so that it gives better understandable traces of how the suspicious line would be reached in the program (without actually having to execute it). Such a trace is of great value to the programmer, as it tells what is happening before the suspicious code.
The project is in a team of international researchers, engineers and students.
Novelty and Contribution
The contribution consists of improving the Goanna program analyser to be more valuable to the user.
Expected Outcomes
Implementation of error traces and documentation.
Reference Material/Links
Goanna project:
http://www.ertos.nicta.com.au/research/goanna/
SKILL PREREQUISITES:
Excellent programming skills. Experience with functional programming, C/C++ or model checkers a plus.
Project Title
Warning Suppression for Static Program Analyser
Name of Academic Supervisor
Dr Ralf Huuck
Email of Academic Supervisor
ralf.huuck@nicta.com.au
Name of Joint Supervisor(s)
Dr Ansgar Fehnker
Email of Joint Supervisor(s)
ansgar.fehnker@nicta.com.au
CSE or NICTA Project
NICTA
Research Area
Formal Methods
Abstract of Research Project
The goal of the Goanna project is to improve the quality of system software by automatically detecting software defects (bugs). Our prototype tool analyses C/C++ source code and prints warnings much like compilers do. Some of these warnings are annoying to programmers, because the warnings are false positives or indicate problems that the programmers are well aware of.
The goal of this summer project is to improve the tool so that it can suppress certain warnings or types of warnings. The tool should suppress the warnings even if the line numbers change, and show the warnings again if the affected code changes significantly.
The project is in a team of international researchers, engineers and students.
Novelty and Contribution
The contribution consists of improving the Goanna program analyser to be more valuable to the user.
Expected Outcomes
Implementation of warning suppression mechanism and documentation.
Reference Material/Links
Goanna project:
http://www.ertos.nicta.com.au/research/goanna/
SKILL PREREQUISITES:
Excellent programming skills. Experience with functional programming, script programming and C/C++ a plus.
Project Title
Automatic Report Generation for Static Program Analyser
Name of Academic Supervisor
Dr Ansgar Fehnker
Email of Academic Supervisor
ansgar.fehnker@nicta.com.au
Name of Joint Supervisor(s)
Dr Ralf Huuck
Email of Joint Supervisor(s)
ralf.huuck@nicta.com.au
CSE or NICTA Project
NICTA
Research Area
Formal Methods
Databases
Abstract of Research Project
The goal of the Goanna project is to improve the quality of system software by automatically detecting software defects (bugs). Our prototype tool analyses C/C++ source code and prints warnings much like compilers do.
The goal of this summer project is to improve the tool so that it generates more sophisticated error reports in an easy to inspect format. It would be nice if programmers could browse source codes and the corresponding error messages with a web browser, easily linking similar or related bugs, ticking off false error reports and marking fixed problems.
The project is in a team of international researchers, engineers and students.
Novelty and Contribution
The contribution consists of improving the Goanna program analyser's output in order to make it easier to understand and manage by the user.
Expected Outcomes
Implementation of report generation and management, documentation.
Reference Material/Links
Goanna project:
http://www.ertos.nicta.com.au/research/goanna/
SKILL PREREQUISITES:
Excellent programming skills, knowledge of C/C++. Experience with functional programming, web technologies, or databases a plus.
Project Title
IDE for Static Program Analysis
Name of Academic Supervisor
Dr Ralf Huuck
Email of Academic Supervisor
ralf.huuck@nicta.com.au
Name of Joint Supervisor(s)
Dr Felix Rauch
Email of Joint Supervisor(s)
felix.rauch@nicta.com.au
CSE or NICTA Project
NICTA
Research Area
Formal Methods
Abstract of Research Project
The goal of the Goanna project is to improve the quality of system software by automatically detecting software defects (bugs). Our prototype tool analyses C/C++ source code, as well as embedded ARM assembly. Currently, it is a stand-alone command-line tool, which is explicitly started by the programmer or manually integrated into the development environment.
The goal of this summer project is to integrate the Goanna tool into
a real integrated development environment (IDE) like Eclipse or
Microsoft Visual Studio. The IDE should support to individually select the properties that Goanna should check and to display valuable feedback on the location and causes of found program defects.
The project is in a team of international researchers, engineers and students.
Novelty and Contribution
The contribution consists of making the Goanna program analyser much easier to use.
Expected Outcomes
IDE plugins and documentation.
Reference Material/Links
Goanna project:
http://www.ertos.nicta.com.au/research/goanna/
SKILL PREREQUISITES:
Excellent programming skills, knowledge of C/C++ and functional programming. Experience with IDEs a plus.
[Top of Page]
