FM - 1 Hardware modelling in an extensible simulator

NICTA Project - Dr. Gerwin Klein (gerwin.klein@nicta.com.au) and David Cock (davec@cse.unsw.edu.au)

The aim of this project is to extend an existing cross-platform, automatically generated simulator (under development within NICTA) with a concrete system model. This would involve gaining a substantial technical understanding of an important piece of hardware (NIC, PCI controller), and implementing a model within the simulator of sufficient detail to be useful for systems (OS kernel) development. The student would work within an international team of both formal methods (FM) and operating systems (ERTOS) researchers, in particular the L4.verified and seL4 projects.

Demonstrating the feasibility of a generic simulator architecture for full-system simulation. A potential outcome of the research is an executable simulator model of an important piece of hardware (NIC, PCI controller, serial port)

For further information, please contact the supervisor or consider the following:

http://www.ertos.nicta.com.au/research/l4.verified/ - the l4.verified project.
http://www.ertos.nicta.com.au/research/sel4/ - the SEL4 project.

FM - 2 Verifying libc in Isabelle/HOL

NICTA Project - Dr Gerwin Klein (gerwin.klein@nicta.com.au) and Harvey Tuch (harvey.tuch@nicta.com.au)

The objective of this research is to formally verify a small number of basic C functions like memcpy, memset, etc. using a state-of-the-art C verification tool developed by the L4.verified project. This will involve developing formal specifications and proofs of correctness in the the interactive theorem prover Isabelle/HOL. The results of this work will be crucial to the verifcation of any non-trivial C applications in our tool. 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.

This work addresses the often neglected problem of verifying software written in system languages such as C. A successful outcome will provide useful experience in applied formal methods and lead to the first verified C library. In addition to the above mentioned specifications and proofs, a potential outcome of the research is discovered bugs in the C library and a possible publication.

For further information, please contact the supervisors or consider the following:

http://ertos.nicta.com.au/research/l4.verified/
http://www.mirror.cse.unsw.edu.au/pub/isabelle/

FM - 3 Formal Proof of Operating System Properties

NICTA Project - Dr. Gerwin Klein (gerwin.klein@nicta.com.au) and Thomas Sewell (tsewell@cse.unsw.edu.au)

With seL4, the NICTA ERTOS program has designed a new secure, embedded microkernel, based on L4. The L4.verified and seL4 projects have developed a complete formal specification of this operating system kernel. The L4.verified project has already proved certain safety and security properties of the specification, but many interesting properties remain uninvestigated.

This project would be ideal for a student with background in operating systems or mathematical proof to develop a knowledge of formal methods and contribute to a world first in system verification.

The student could address any of a growing list of uninvestigated properties, or one they devised themselves. An example would be to prove that a delete operation in the kernel never leaves any dangling references to the deleted object in the rest of the system. This project would contribute a complete proof or counterproof in an otherwise open research issue. A potential outcome of the research is a fully formal proof that a meaningful property does or does not hold for the given system specification.

For further information, please contact the supervisors or consider the following:

http://www.ertos.nicta.com.au/research/l4.verified/ - the l4.verified project.
http://www.mirror.cse.unsw.edu.au/pub/isabelle/ - the Isabelle/HOL interactive theorem prover.

FM - 4 Formalisation of a Security Model in Isabelle/HOL

NICTA Project - Dr. Gerwin Klein (gerwin.klein@nicta.com.au) and Dhammika Elkaduwe (dhammikae@cse.unsw.edu.au)

With seL4, the NICTA ERTOS program has designed a new secure, embedded microkernel, based on L4. As part of the proof of security associated with the seL4 and L4.verified projects, an appropriate version of the Take/Grant model of security found in the literature has been developed, using precise mathematical language.

However, it is well known that even using precise mathematical language, a number of errors can slip through, and even be published in mathematical journals.

This project aims to remove that possibility by formalising the model using the Isabelle/HOL theorem prover. A formalised security model would be of great value to a number of novel security approaches. The expected outcome is a fully formal model of a system's behaviour, conforming to the Take/Grant model advanced already.

For further information, please contact the supervisors for a copy of the Take/Grant model developed so far, or consider the following:

http://www.ertos.nicta.com.au/research/l4.verified/ - the l4.verified project.
http://www.ertos.nicta.com.au/research/sel4/ - the SEL4 project.

FM - 5 Integrating separation logic decision procedures in Isabelle/HOL

NICTA Project - Dr. Gerwin Klein (gerwin.klein@nicta.com.au) and Harvey Tuch (Harvey.tuch@nicta.com.au)

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. There is also scope for investigating new decision procedures for experienced students. 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.

This work addresses the often neglected problem of verifying 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. An expected outcome of the research is integrated decision procedures and examples together with a possible publication.

For further information, please contact the supervisors or consider the following:

http://ertos.nicta.com.au/research/l4.verified/
http://www.mirror.cse.unsw.edu.au/pub/isabelle/

FM - 6 Security testing of the seL4 Specification

NICTA Project - Dr. Gerwin Klein (gerwin.klein@nicta.com.au) and Thomas Sewell (tsewell@cse.unsw.edu.au)

With seL4, the NICTA ERTOS program has designed a new secure, embedded microkernel, based on L4. The L4.verified project aims to prove that the seL4 implementation and specification behave identically, making an insecure implementation impossible. However, the possibility of a security flaw inherent in the specification remains a concern.

This project will undertake penetration testing of the specification. The hope is that an independent analysis may find flaws that the designers missed.

The seL4 specification is written in Haskell. It can be tested alongside malicious code in a simulator, but is also concise enough that a student can gain familiarity with it in the timeframe available.

This is a rare opportunity to do real security research without focusing on implementation detail. The expected outcomes are a number of case studies of different classes of attacks, either detailing success and appropriate remedy or providing reasonable argument why the class of attacks is infeasible.

For further information, please contact the supervisor or consider the following:

http://www.ertos.nicta.com.au/research/l4.verified/ - the L4.verified project.
http://www.ertos.nicta.com.au/research/sel4/ - the seL4 project.
http://www.ertos.nicta.com.au/research/sel4/api.pml - the current seL4 specification.

FM - 7 IDE for Static Program Analysis

NICTA Project - Dr Ralf Huuck (ralf.huuck@nicta.com.au)

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. 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 real integrated development environments (IDEs) 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 contribution consists of making the Goanna program analyser much easier to use.

The project is in collaboration with a team of international researchers and students. An expected outcome of the research is IDE plugins and documentation.

For further information, please contact the supervisor or consider http://www.ertos.nicta.com.au/research/goanna/

FM - 8 Automatic Report Generation for Static Program Analyser

NICTA Project - Dr Ansgar Fehnker (ansgar.fehnker@nicta.com.au) and Dr Ralf Huuck (ralf.huuck@nicta.com.au)

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 errors with a web browser, easily linking similar or related bugs, ticking off false error reports and marking fixed problems. The contribution consists of improving the Goanna program analyser's output in order to make it easier to understand and manage by the user.

The project is in collaboration with a team of international researchers and students. An expected outcome of the research is implementation of report generation and management, documentation.

For further information, please contact the supervisor or consider http://www.ertos.nicta.com.au/research/goanna/

FM - 9 High-Performance XML Search for Static Program Analyser

NICTA Project - Dr Sebastian Maneth (sebastian.maneth@nicta.com.au)

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 detects (potential) bugs by performing elaborate search procedures.

The goal of this summer project is to improve the tool so that it uses less time for search in XML structures. We expect to slash search time by migrating to a fast, high-performance XPath library. The library has to be smoothly integrated into the tool to obtain optimal performance. The contribution consists of improving the Goanna program analyser's performance through implementing high-performance XML search.

The project is in collaboration with a team of international researchers and students. An expected outcome of the research is implementation of fast XML search (using an existing XPath library) documentation. For further information, please contact the supervisor or consider http://www.ertos.nicta.com.au/research/goanna/

[Top of Page]