Research
Software Systems

Taste of Research (ToR) 2016-2017 Summer Project Proposals

Applications

Applications for summer research in Trustworthy Systems for the topics below can be made through

Projects

 

Formal Methods

Theorem Proving

Automating Formal Proofs (+USyd)

Gerwin Klein, Daniel Matichuck

Abstract: Isabelle is an interactive theorem prover which combines automated and human reasoning through the use of proof methods (or tactics). These methods allow users to make high-level decisions on how to progress in a proof without worrying about the formal details. Powerful proof methods are required for large proof undertakings, such as the L4.verified project at NICTA.

Eisbach is an in-development prototype of a high-level language for writing proof methods in Isabelle, which is historically done in Standard ML. It is influenced by Coq’s Ltac, but distinguishes itself by leveraging Isabelle’s existing automation and backtracking infrastructure.

The aim of this project is to investigate useful applications for Eisbach, with several possible domains to explore: An existing suite of NICTA-developed separation logic tactics could be re-implemented and extended, or a similar investigation can be done against the verification-condition generator used in the L4.verified proof; Or a novel proof method can be developed solve, for example, word arithmetic proofs that appear frequently in the verification of C programs.

Novelty: This will be one of the first larger-scale uses of the new Eisbach proof language and the resulting feedback will contribute to its further development.
Outcome: Automated proof tactics for previously manual proofs in one or more of the specified application domains, ideally reducing proof size and time for those applications.

Reference Material Links:
Trustworthy Systems project: http://www.ssrg.nicta.com.au/projects/TS/
Software Systems Research Group (SSRG): http://www.ssrg.nicta.com.au/
seL4: http://ertos.nicta.com.au/research/sel4/
Isabelle: http://mirror.cse.unsw.edu.au/pub/isabelle/

Machine learning for proof script generation.

Yutaka NagashimaGerwin Klein

Abstract: Isabelle is an interactive theorem prover. At Data61, we are developing a domain specific language, Isarring, to specify high level proof strategies for Isabelle. Given a proof strategy, Isarring's runtime system tries to generate human-readable fast-to-replay proof scripts using backtracking proof-search.

The goal of this project is to improve the proof script generation of Isarring's runtime system with machine learning. Isabelle already uses a machine learning tool, MaSh, when it invokes external first-order theorem provers through the command, Sledgehammer. In this project, we improve Isarring's runtime system using MaSh.

Novelty: Upon successful completion of the project, this work will combine the power of backtracking search and machine learning to produce human-readable fast-to-replay proof scripts in Isabelle.

Outcome: Better proof automation for Isabelle.

Reference Material Links:
Isabelle/HOL: http://mirror.cse.unsw.edu.au/pub/isabelle/index.html

 

Formal Verification of Concurrent Programs Flying Quadcopters

June Andronick, Corey Lewis

Abstract>NICTA is famous for its formal verification of the seL4 microkernel, which for the first time formally proved the correctness of 10,000 lines of C code for a general purpose operating system (OS) kernel. However, it is not feasible to use seL4 on less powerful hardware - such as small medical implant devices or extremely resource-constrained spacecraft. For these purposes NICTA, in collaboration with Breakaway Consulting, is currently in the process of building and formally verifying a small, versatile, high-assurance real-time OS called eChronos. This OS is embedded in quadcopters as part of a large project, funded by DARPA, with industry and university partners from the US.

One of the main challenges involved in this work is reasoning about concurrency. This project would include investigating different approaches that could be used to verify concurrent programs which use eChronos. In particular, we would aim to develop a framework that automates much of the reasoning involved in this verification.

Novelty: Addressing the concurrency challenge in the formal verification of real-world embedded programs.

Outcome:The expected outcome of the project is a framework for verifying the correctness of concurrent programs running on top of eChronos.

Improving automation in concurrent software verification (+USyd)

June Andronick, Corey Lewis

Abstract: NICTA is currently modelling and verifying a small real-time operating system, eChronos. The reasoning about interleaved execution between tasks' code and interrupt code is done using a classical concurrency reasoning method, known as Owicki-Gries, empowered by the automation of a modern interactive theorem prover, Isabelle. Still, this requires manual annotation of each step in the parallel program, for each property shown. Proofs for these annotations could be re-used instead of being reproved for different properties. In this project, you will investigate increasing the automation of practical concurrency verification by allowing re-use of previously proved annotations.

Novelty: Your work will contribute to the general feasibility and scalability of practical concurrent software verification.

Outcome: Your work will directly impact the efficiency of the framework and proofs developed for the verification of eChronos.

Reference Material Links: http://ssrg.nicta.com.au/projects/TS/echronos/

Implement and Verify a CakeML Compiler Optimisation

Ramana Kumar

Abstract:
CakeML is a functional programming language (similar to OCaml or Standard ML) with a formal specification (a definition in logic) and a mechanically verified (proven correct) compiler and runtime system. The CakeML compiler is at the forefront of research on verified compilers for functional programming languages, aiming for end-to-end correctness with good performance and reasonable cost. It is the basis for an approach to building high-assurance computer software using interactive theorem provers.

The design of the CakeML compiler allows for various optimisation passes to be implemented as local source-to-source transformations over one of the compiler's intermediate languages. Implementing and verifying one such optimisation is a good way to improve the CakeML compiler while gaining experience with theorem proving and compiler writing.

There are many specific examples of optimisations to add (including: pointer equality testing, pattern-match exhaustiveness checking, splitting large functions, simplifying redundant if-expressions, improving instruction selection for conditional jumps, and encoding stack-layout bitmap indices in return addresses). Do one or more of those, or design and verify your own optimisation!

Novelty:   Following the success of CompCert for C, interest in optimising verified compilers is taking off. CakeML is the most realistic verified compiler for a functional programming language. Verified optimisations are an opportunity to improve the state of the art in verified compilation.

Outcome:   A new compiler optimisation added to the verified CakeML compiler. Benchmarks demonstrating an improvement in the compiled code.

Reference Material Links:
CakeML: https://cakeml.org
HOL: https://hol-theorem-prover.org
More detailed CakeML project ideas: https://cakeml.org/projects.html
CompCert: http://compcert.inria.fr

Implement and Verify Enhancements to CakeML

Ramana Kumar

Abstract:
CakeML is a functional programming language (similar to OCaml or Standard ML) with a formal specification (a definition in logic) and a mechanically verified (proven correct) compiler and runtime system. CakeML is the basis for an approach to building high-assurance computer software using interactive theorem provers. The aim of the project is end-to-end correctness with good performance and reasonable cost, and ultimately scaling formal methods up to large-scale applications.

Formally specifying a programming language is a serious endeavour, and the CakeML language currently lacks many features of full-blown (but underspecified) programming languages. There are opportunities for enhancements at many levels, including the concrete syntax, the type system, the built-in primitive operations, and the standard library. Examples of features we would like to add include: explicit type annotations, expression-level let-polymorphism, user-defined infix operators, nested modules, named module interfaces (signatures), and records. Specify and verify one of these features, or design your own enhancement to CakeML!

Novelty:   Scaling formal semantics up to realistic programming languages is an exciting area of research, making theorem proving relevant to a larger class of applications.

Outcome:   An extension to CakeML's formal specification, and, ideally, a corresponding extension to CakeML's verified compiler.

Reference Material Links:
CakeML: https://cakeml.org
HOL: https://hol-theorem-prover.org
More detailed CakeML project ideas: https://cakeml.org/projects.html

Proof Engineering on CakeML proofs

Ramana Kumar

Abstract:
CakeML is a functional programming language (similar to OCaml or Standard ML) with a formal specification (a definition in logic) and a mechanically verified (proven correct) compiler and runtime system. The CakeML proofs are a substantial formal development (over 100,000 lines of proof script) that is starting to reach the size where scalability issues become relevant. The discipline of proof engineering, which is to proof development as software engineering is to large-scale software development, can be applied; this project is to do so.

Although some of the work to be done here is simply tweaking and refactoring, there are also many opportunties for creative ideas about how to structure and manage large formal developments, or for particular approaches to generating certain definitions or proofs automatically.

Novelty:   Large scale proofs are an exciting combination of software engineering methodology with formal methods.

Outcome:   Improvements to the speed or size of CakeML proofs, and, ideally, new approaches to dealing with large formal developments.

Reference Material Links:
CakeML: https://cakeml.org
HOL: https://hol-theorem-prover.org

Open Theory Import for Isabelle/HOL (+USyd)

Ramana Kumar, Gerwin KleinRafal Kolanski

Abstract: 
The goal of the OpenTheory project is to allow specifications and proofs to be shared between different theorem prover implementations of higher order logic. Currently, this proof exchange format is supported by the provers HOL Light, HOL4, and ProofPower. The aim of this project is to extend the interactive theorem prover Isabelle/HOL with import facilities for the OpenTheory format, so that Isabelle users can access and re-use the large libraries of proofs written in any of these three provers. 

There exists an initial attempt at OpenTheory import for a previous version of OpenTheory and of Isabelle/HOL from 2011. The task of this project would be to design and implement a new mechanism for modern versions of the exchange format and the prover.

The project requires knowledge of functional programming in a language such as ML, OCaml, or Haskell. The implementation language for this project is standard ML.

Novelty:  Proof exchange formats are an exciting new research and engineering direction for interactive provers. The contribution of this project would be to extend the family of provers that can communicate with each other.

Outcome:  A standard ML implementation of OpenTheory import for the prover Isabelle/HOL

Reference Material Links:

Isabelle: http://mirror.cse.unsw.edu.au/pub/isabelle/
OpenTheory: http://www.gilith.com/research/opentheory/

Verification of native C functions in Cogent. (+USyd)

Gerwin Klein

Abstract: The goal of this project is to verify the correctness of C functions that are called by Cogent programs.

Cogent is a purely functional domain-specific language with linear types. From a well-typed Cogent program, the Cogent compiler generates efficient C code, a formal specification of the program’s purely functional semantics and a machine-checked proof of compilation correctness against that specification. Hence, we can automatically guarantee the absence of several well-known errors statically by writing programs in Cogent.

SSRG has implemented multiple file systems in Cogent. In the development of these file systems, the Cogent foreign function interface allowed us to call C functions from Cogent code where they can be best implemented in C. The goal of this project is to verify that these C functions fit into the Cogent framework using Isabelle/HOL.

Novelty: Upon successful completion of the project, this work will fill the last missing piece of the verification of fully verified file systems. To the best of our knowledge, these will be the world's first implementations of such systems.

Outcome: Machine-checked fully verified file systems.

Reference Material Links:

http://ssrg.nicta.com.au/
http://ssrg.nicta.com.au/projects/TS/filesystems.pml

 

Protocols

Automatic Translation of Routing Protocol Specifications (+USyd)

Peter Höfner, Rob van Glabbeek

Abstract: Wireless Mesh Networks (WMNs) are a promising technology that is currently being used in a wide range of application areas, including Public Safety, Transportation, Mining, etc. Typically, these networks do not have a central component (router), but each node in the network acts as an independent router, regardless of whether it is connected to another node or not. They allow reconfiguration around broken or blocked paths by “hopping” from node to node until the destination is reached. Unfortunately, the performance of current systems often does not live up to the expectations of end users in terms of performance and reliability, as well as ease of deployment and management.

We explore and develop adaptive network protocols and mechanisms for Wireless Mesh Networks that can overcome the major performance and reliability limitations of current systems. To support the development of these new protocols, the project also aims at new Formal Methods based techniques, which can provide powerful new tools for the design and evaluation of protocols and can provide critical assurance about protocol correctness and performance. Close collaboration with industry partners ensures the use-inspired nature of the project.

Novelty: Model checking is a technique for automatically verifying correctness properties of finite-state systems in general and WMNs in particular: given a model of a WMN routing protocol, a model checker like UPPAAL (http://www.uppaal.org/) can test automatically whether this model satisfies a given specification. In order to solve such a problem, both the model and the specification are formulated in some precise mathematical language. But even if a precise description of a protocol is given e.g., in process algebra, this description is usually not accepted by a model checker. This is due to incompatibility of different languages.

Outcome: Prior work involved the implementation of translation software from a process algebra language to a model description for UPPAAL. Although large parts of routing protocol can now be automatically translated, some difficult language constructs so far require human intervention. The goal of this project is to further automatise the translation effort, ultimately making it fully automatic. After this has been finished, the software should be tested on several case studies. Moreover, the software could be extended to produce input for other model checkers.

Expressiveness of Distributed Systems (+USyd)

Peter Höfner, Rob van Glabbeek

Abstract: We aim to discover which systems can be implemented in a distributed way---and how---using only asynchronous communication between components, while preserving desirable properties that may be specified in terms of synchronous communication. In connection with this, we try to establish an expressiveness hierarchy of specification formalisms with different communication paradigms.

We propose and inventory various definitions of what it means for processes to communicate with each other using only asynchronous communication, and subsequently investigate which processes can be implemented conform these definitions. In deciding whether a given process can be implemented using only asynchronous communication, one needs to choose a semantic equivalence that specifies which aspects of the specified behaviour need to be preserved under implementation. Depending on this choice, either a class of systems can be implemented distributedly---and we aim at giving a structural characterisation of this class---or all systems can be implemented distributedly---and we aim to investigate the strongest behavioural equivalence that makes this possible.

We also need to study adequate semantic equivalences to decide which aspects of a specified behaviour need to be preserved under implementation. Here the preservation of liveness properties under adequate progress or fairness assumptions warrants more investigations.

Novelty and Contribution: The project will look at some particular formal mechanisms (e.g. process algebras, Petri nets, or Turing machines) and try to analyse their expressivity. The goal involves the development of systems that can be or that cannot be implemented (incl. formal proofs of this) in the mechanism under consideration. Another goal may be the exploration of semantic equivalences that preserve required liveness properties. 

Expected Outcomes: Proven expressiveness results, results on distributability of classes of systems, and/or results on preservation of properties of semantic equivalences.

Reference Material Links:
NICTA's project on Concurrency and Protocol Verification: http://ssrg.nicta.com.au/projects/concurrency/.
SSRG: http://ssrg.nicta.com.au/.
Our research on expressiveness: http://ssrg.nicta.com.au/projects/concurrency/distributability.pml

Formal Specification of the carrier-Sense-Multiple-Access Protocol (+USyd)

Peter Höfner, Rob van Glabbeek

Abstract: Carrier sense multiple access (CSMA) is a probabilistic media access control (MAC) protocol in which a node verifies the absence of other traffic before transmitting on a shared transmission medium, such as an electrical bus, or a band of the electromagnetic spectrum. For example, on ethernet, any device can try to send a frame at any time. Each device senses whether the line is idle and therefore available to be used. If it is, the device begins to transmit its first frame. If another device has tried to send at the same time, a collision is said to occur and the frames are discarded. Each device then waits a random amount of time and retries until successful in getting its transmission sent. CSMA is specified in the IEEE 802.3.

Novelty: IEEE 802.3 specifies the protocol in English prose. By doing so, the specification might be easily understandable by programmers. 

Specifications written English prose, however, often contain ambiguities and, in some cases, even contradictions.
This can only be avoided my a formal specification. Such a specification in not only unambiguous, it also paves the way for
a formal analysis of the protocol, which is usually performed using techniques such as modelling checking or interactive theorem proving.

Outcome: Based on a existing process algebra, the CSMA protocol should be formally specified. To achieve this goal, CSMA needs to be understood in detail. 

Depending on the requirements of the protocol under consideration, the project might also consider the extension of the existing process algebra
by primitives required for the specification.

Reference Material Links:
NICTA's project on Concurrency and Protocol Verification: http://ssrg.nicta.com.au/projects/concurrency/.
SSRG: http://ssrg.nicta.com.au/.

Model Checking of Mesh Network Routing Protocols (+Usyd)

Peter Höfner, Rob van Glabbeek

Abstract: Wireless Mesh Networks (WMNs) are a promising technology that is currently being used in a wide range of application areas, including Public Safety, Transportation, Mining, etc. Typically, these networks do not have a central component (router), but each node in the network acts as an independent router, regardless of whether it is connected to another node or not. They allow reconfiguration around broken or blocked paths by "hopping" from node to node until the destination is reached. Unfortunately, the performance of current systems often does not live up to the expectations of end users in terms of performance and reliability, as well as ease of deployment and management.

We explore and develop adaptive network protocols and mechanisms for Wireless Mesh Networks that can overcome the major performance and reliability limitations of current systems. To support the development of these new protocols, the project also aims at new Formal Methods based techniques, which can provide powerful new tools for the design and evaluation of protocols and can provide critical assurance about protocol correctness and performance. Close collaboration with industry partners ensures the use-inspired nature of the project.

Novelty: Model checking is a technique for automatically verifying correctness properties of finite-state systems in general and WMNs in particular: given a model of a WMN routing protocol, a model checker like UPPAAL (http://www.uppaal.org/) can test automatically whether this model satisfies a given specification. In order to solve such a problem, both the model and the specification are formulated in some precise mathematical formalism, such as the UPPAAL input language.

Outcome: This project aims at setting up a model checking environment for UPPAAL, suitable for streamlining the model checking of routing protocols on certain network topologies. The environment should should be adaptable for the specification of classes of network topologies as well routing protocol formalisations.

Modelling Routing Protocols (+USyd)

Rob van Glabbeek, Peter Höfner

Abstract: Wireless Mesh Networks (WMNs) are a promising technology that is currently being used in a wide range of application areas, including Public Safety, Transportation, Mining, etc. Typically, these networks do not have a central component (router), but each node in the network acts as an independent router, regardless of whether it is connected to another node or not. They allow reconfiguration around broken or blocked paths by "hopping" from node to node until the destination is reached. Unfortunately, the performance of current systems often does not live up to the expectations of end users in terms of performance and reliability, as well as ease of deployment and management.

We explore and develop adaptive network protocols and mechanisms for Wireless Mesh Networks that can overcome the major performance and reliability limitations of current systems. To support the development of these new protocols, the project also aims at new Formal Methods based techniques, which can provide powerful new tools for the design and evaluation of protocols and can provide critical assurance about protocol correctness and performance. Close collaboration with industry partners ensures the use-inspired nature of the project.

The project's work should include the formalisation of a second standard protocol such as OSLR (http://en.wikipedia.org/wiki/Optimized_Link_State_Routing_Protocol) or HWMP (http://en.wikipedia.org/wiki/IEEE_802.11s). After a faithful specification has been given, the work could include the verification of basic properties of the routing protocol: packet delivery for example guarantees that a packet, which is injected into a network, is finally delivered at the destination (if the destination can be reached.

Novelty: Classical routing protocol specifications are usually written in plain English. Often this yields ambiguities, inaccuracies or even contradictions. The use of Formal Methods like process algebra avoids these problems and leads to a precise description of protocols. To compare and evaluate different protocols, we aim at a compendium of standard routing protocol specifications in a unified language.

Outcome: So far we have modelled one of the standard protocols using process algebra, namely AODV, as well as a draft successor protocol that is currently being discussed by the Internet Engineering Task Force (IETF).

 Verifying Communciation Protocols for Quadcopters (+Usyd)

Rob van Glabbeek, Peter Höfner

Abstract: In the past years NICTA's Software Systems Research Group (SSRG) has done much work developing and verifying seL4, a secure, formally verified microkernel. The next step is to use seL4 as a basis for developing truly secure software systems. This project will concentrate on communication protocols, which are part of nearly every system. The goal of the project is to verify the correctness of communication protocols for internal communication within a quadcopter. The protocols are defined by a formal specification. This specification will be the basis of the verification effort.

Novelty: The project will be one further step towards a real trustworthy system; so far no verified protocols had been combined with a verified kernel.

Outcome: Verification of the correctness of communication protocols running on a quadcopter.

Reference Material Links:
Trustworthy Systems project: http://www.ssrg.nicta.com.au/projects/TS/
SMACCM project: http://ssrg.nicta.com.au/projects/TS/SMACCM/
Communication protocols for quadcopters: http://ssrg.nicta.com.au/projects/concurrency/smaccm.pml

Systems

Kernels

  Interrupt-Related Covert Channels on seL4

Description of this topic is in the Security section.

ROS native on seL4

Gernot Heiser, Siwei Zhuang

Abstract: ROS (robotics operating system) is a communication middleware that is widely used for programming robots. It typically runs on a fully-fledged OS, such as Linux, using sockets for communication. This makes it readily accessible, but from the security and safety point of view is a nightmare. The purpose of this project is to produce a native ROS on the seL4 microkernel, depending on a minimal trusted computing base. It involved an assessment of the OS services required by ROS, and design, implementation and evaluation of ROS/seL4.

Novelty: A minimal ROS can enable a security and safety analysis of robotics software, dramatically increasing the trustworthiness of the robots, and opening the way for deployment in critical systems.

Outcome: An seL4-based ROS implementation that can support the high-assurance autonomous trucks developed under the DARPA HACMS program. Performance evaluation against a Linux-based implementation.

POSIX environment for seL4

Gernot Heiser, Ihor Kuz

Abstract: POSIX is a widely supported OS interface standard, provided by Linux and many other OSes. Much real-world software can be ported to a system that supports POSIX. The are POSIX profiles that require limited functionality, up to full Unix compliance. A good start to a POSIX environment for seL4 was made with the Robigalia project, which uses Rust as the implementation language. This project will use Robigalia as a starting point and design, implement and evaluate a complete POSIX environment for at least a minimal profile.

Novelty: A POSIX environment with a minimal trusted computing base, inhereting the strong formal isolation guarantees provided by seL4, that will provide a basis for porting a wealth of software useful in high-assurance systems. It will also serve as an evaluation of Rust as a systems programming language.

Outcome: A complete POSIX implementation suitable for high-assurance use. Performance evaluation against Linux.

Protected-Mode eChronos

Gernot Heiser, Alex Kroh

Abstract: eChronos is a formally-verified RTOS designed for deeply-embedded systems with no memory protection and single-mode execution. However there are interesting use cases for a verified kernel on mid-range processors that feature a simple memory-protection unit (MPU). A particularly interesting case is the ARM Coretex M4, which eChronos already supports, albeit without utilising the MPU. This project is to design a protected-mode version of eChronos, implement and evaluate it.

Novelty: NICTA has produced the first verified kernels for high-end microprocessors with full virtual memory (seL4) as well as for low-end single-mode microcontrollers (eChronos). The remaining middle ground are MPU-only processors. Success of this project will complete coverage.

Outcome: eChronos version that uses memory protection

eChronos Art Project

Peter Chubb,, Sebastian Holzapfel

Abstract: eChronos is a formally-verified RTOS designed for deeply-embedded systems with no memory protection and single-mode execution. It is fairly simple to drive sensors, actuators and relays from very cheap boards, and get interesting results. This project is to take simple M4-based development boards such as the Stellaris Launchpad, hook them up to ultrasonic sensors, motors and LEDs to produce an artistic installation that shows off the real-time and embedded capabilities of the platform, while being aesthetically interesting.

Novelty:

Outcome: eChronos-based art installation suitable for open days and demonstrations.

Sloth vs eChronos

Gernot Heiser, Anna Lyons

Abstract: eChronos is a formally-verified RTOS designed for deeply-embedded systems with no memory protection and single-mode execution. Sloth is a system for a similar application domain, which takes the unusual approach of leaving all scheduling to hardware, by running everything in an interrupt context. This limits the use of Sloth to processors where interrupts mode can be entered by software. This project is to evaluate and quantify the performance advantage of Sloth over eChronos.

Novelty: Sloth is presently the world's fastest RTOS. eChronos, which has the advantage of formal verification and less dependence on hardware features, is a more traditionally-designed RTOS. This project will determine whether the performance advantage of Sloth is significant enough to justify the different (and more limiting) design. The results are eminently publishable.

Outcome: A better understanding of RTOS design tradeoffs.

Standard C libraries - which one?

Kevin Elphinstone

Abstract: The project aims to survey existing C library implementations for use in seL4 microkernel. The standard C library is anything but standard, and differing implementations have differing properties. The goal of this project develop criteria for evaluating the goodness of a standard C library (such a performance, completeness, size, modularity), and use the criteria to understand the landscape of C libraries available for open source systems. The goal of the project is to port the most appropriate C library to seL4.

Novelty: An evaluation of existing C libraries in the context of microkernels.

Outcome: A C-library port and evaluation on seL4.

From RefOS to Phoenix.

Kevin Elphinstone

Abstract: RefOS is an immature multiserver OS on seL4. The OS is somewhat fragile and a little neglected. This project is aimed at resurrecting RefOS from the ashes into something usable for future development. The project provides the opportunity for a student to make their mark on the only multiserver OS environment running on seL4. While the project is quite open ended, it can also be tackled in a quite focused and manageable way.

Novelty: Novelty: Tackles issues in building multiserver systems on the worlds only formally verified microkernel.

Outcome: RefOS running in a simple form.

Rump kernels on Camkes

Kevin Elphinstone

Abstract: Rump kernels are a cut-down variant of the BSD operating system design to provide OS services in other contexts. We have a port of Rump kernels to native seL4. This project aims to build on existing work to run Rump kernels in the CAmkES environment on seL4. CAmkES is an embedded component framework for seL4 which would benefit from the increased functionality Rump kernels would provide.

Novelty: Be the first to examine the feasibility of using Rump kernel with a component framework on the world's only verified microkernel.

Outcome: A simple Rump component running in the CAmkES environment.

Using untrusted code in trusted environments.

Kevin Elphinstone

Abstract: Modern computer software systems are large and complex systems. The effort required to develop such a system can be reduced by using existing opensource code bases to avoid the cost of reimplementation. However, including large opensource code bases in high security environments provides a large attack surface that is difficult to both evaluate and ultimately assure is secure.

This topic's goal is to take some baby steps towards being able to utilise open source libraries while minimising exposure to bugs within the libraries using protection boundaries provided by seL4.

Novelty: The is a open research area the student can actively contribute to initial understanding of the area.

Outcome: An initial understanding of what might be achieved, and a simple proof of concept.

Middleware

Build the world's first secure network stack (+USyd)

Peter Chubb

Abstract: Build the world's first secure network stack by writing it in our special language. At NICTA, we developed a new language called Cogent for writing verified by construction software. The Cogent compiler generates C code, a formal specification describing what this code does, and a mathematical machine checked proof that the generated C code corresponds to the generated formal specification. We implemented verified by construction file systems by writing them in this language. The goal of this project is to test the feasibility of implementing a simplified network stack in Cogent. This may contribute to enriching Cogent and you would be encouraged to ask for feature requests to make implementing in this language easier.

Novelty: This will be the first use of the Cogent language in the domain of network stacks.

Outcome: The outcome of this work is testing whether the Cogent language has sufficient expressivity to be used to implement network stacks. This work will be used to extend the Cogent language.

Reference Material Links:

http://ssrg.nicta.com.au/projects/TS/filesystems.pml
http://plosworkshop.org/2013/preprint/keller.pdf

CAmkES on Linux

Ihor Kuz, Matthew Fernandez

Abstract: The Software Systems Research group at NICTA has developed a component platform (CAmkES) for developing microkernel-based systems on seL4 (our formally verified microkernel). While CAmkES helps to ease the difficulty of developing systems on seL4, developing significantly complex systems is still hard, due to the need to develop almost everything (e.g. device drivers, network stacks, display systems, etc.) from scratch. The goal of this project is to develop a version of CAmkES for Linux. This will provide a much richer environment on which to prototype and test CAmkES systems, before porting them to run on seL4.

Novelty: This work will aid in the development of secure systems running on seL4.

Outcome: A version of CAmkES targeted to Linux, and sample systems to test it.

Java Script on sel4

Peter Chubb, Kevin Elphinstone, Adrian Danis

Abstract: Currently there is no managed language that can run natively on seL4. The JavaScript core is sufficiently small and portable it could be a good target for a native seL4 language.

This project involves porting the v8 (or similar) node.JS code to run natively on seL4 on ARM, and porting enough of the nodebot libraries to control some simple things.

Outcome: - a javascript interpreter that runs on seL4

Stretch goals include porting Task.js, JavaScript's concurrency framework

Operating System Components

Ihor Kuz, Matthew Fernandez
Abstract: Towards developing a full OS on the seL4 microkernel.  At NICTA's Software Systems Research Group we've developed technology (CAmkES) for building componentised operating systems. Now we want to build up a repository of reusable operating systems components, so that we can easily build new, novel, and customised operating systems. The goal of this project is to develop new operating systems components, and develop some systems using these components as a means to test them.
Novelty: This work will contribute to a platform for developing secure and safe operating system software.
Outcome: A collection of reusable operating system components.

seL4-based Distributed Systems

Ihor Kuz, Gerwin Klein

Abstract: In NICTA's Software Systems research group we are developing and verifying seL4-based software systems. These systems are limited to run on a single computer, however, real-world systems are largely distributed systems, consisting of multiple networked computers. The time-triggered architecture (TTA) (developed by Hermann Kopetz) provides a computing infrastructure for the design and implementation of dependable distributed embedded systems. Most importantly key algorithms of TTA have been formally verified. The goal of this project is to investigate whether the combination of seL4 and TTA can be used to develop verified seL4-based distributed systems.

Novelty: This will be a first attempt at developing verified seL4-based distributed systems.

Outcome: A prototype seL4-based distributed system combining seL4 and TTA. The results of this project can form the basis of several other research projects further exploring this combination.

Visualisation of Componentised Operating Systems

Ihor Kuz, Siwei Zhuang

Abstract: NICTA's CAmkES (a component-based platform for developing microkernel-based systems on seL4) uses an Architecture Description Language (ADL) to describe the software architecture of an operating system. While the ADL helps to ease the difficulty of designing and building such a system, ADL documents quickly become too complicated to read and manipulate (in a text format) when the operating system becomes non-trivial. The goal of this project is to explore a way to visualise an operating system: to visually represent how components connect and interact with each other in a large system. This work could be also be expanded to become a full graphical editor for operating system design.

Novelty: This work will contribute to the CAmkES platform and our overall project for developing trustworthy software systems.

Outcome: A visualisation tool and a graphical editor for designing and developing component-based operating systems.

Security

Fuzz testing a new language and compiler (+USyd)

Ihor Kuz

Abstract: When developing software, the compiler that translates source code to machine instructions is generally assumed to be correct. Incorrect software is more likely to be a product of bugs in the source code than bugs in the translation. However, when high assurance techniques like formal verification are applied to the source code, this relationship is reversed. The compiler becomes the weaker link. Subtle compiler bugs may lurk undiscovered, and may only be triggered when compiling particular code.

Novelty:This will be the first use of the Cogent language outside the domain of file systems. There will also be the opportunity to explore new techniques for program generation as part of this project.

Outcome: The result of this work will be a reusable tool for generating valid Cogent programs. It is expected that this will in turn lead to a more robust Cogent compiler.

Reference Material Links:
Cogent: http://ssrg.nicta.com.au/projects/TS/filesystems.pml
Trustworthy Systems project: http://www.ssrg.nicta.com.au/projects/TS/
Software Systems Research Group (SSRG): http://www.ssrg.nicta.com.au/

Secure Systems: Build an Unhackable System!

Kevin Elphinstone, Ihor Kuz,

Abstract: Build a truly secure software system. In the past years NICTA's Software Systems Research Group (SSRG) has done much work developing and verifying seL4, a secure, formally verified microkernel. The next step is to use seL4 as the basis for developing truly secure software systems. This requires designing and implementing software systems that use and extend seL4 (for example web servers, web browsers, firewalls, virtual machines, etc.). But we want to be sure that these software systems provide the security we desire. We can gain assurance of security by analysing, and verifying the systems. The goal of this project is to design and build example systems and then show that they are secure.

Novelty: This will be one of the first implementations and analyses of secure software built on seL4.

Outcome: A seL4-based software system and analysis of its security.

Secure Systems: Can You Hack an Unhackable System?

Kevin Elphinstone, Ihor Kuz

Abstract: We claim that we can build truly secure software systems, but are we right? In the past years NICTA's Software Systems Research Group (SSRG) has done much work developing and verifying seL4, a secure, formally verified microkernel. Now we are using seL4 as the basis for developing truly secure software systems. But we want to be sure that these software systems provide the security we desire. We can gain assurance of security in many ways: by testing, attacking (hacking), analysing, and verifying the systems. The goal of this project is to take (or build) example systems and then show (by any of the above means) that they are secure (or not).

Novelty: This will be one of the first practical evaluations of the security of software built on seL4.

Outcome: Insight into how to make seL4-based systems that are secure in theory also really secure in practice.

 seL4-based Distributed Systems

Description of this topic is in the Middleware section.

 

Programming Languages

Linear type inference in Cogent language

Gabriele Keller, Zilin Chen

Abstract: Cogent is a language we designed and developed for writing provably correct file systems. From Cogent compiler, given a type-correct source program, it spits out an efficient C implementation, a high-level language specification in Isabelle/HOL, a series of intermediate language descriptions and proofs to show that the C code is correct with respect to the high-level spec. Cogent, a purely functional language, features linear type system, which is the key which enables this approach. On the downside, however, our linear type system requires a lot of user annotations in the source programs, which makes them quite verbose. The goal of this project is to research on how linear types, together with effectful computations like allocation and free of memory, can be inferred by the compiler, probably with the aids of model checking.

Novelty: Although there is some preliminary work in this area, it remains an open question. It will be of a good theoretical and practical contribution to the entire language community.

Outcome: The result of this work will be a formal type inference system (possibly with compromises) and its prototypical implementation in Cogent compiler.

http://ssrg.nicta.com.au/projects/TS/filesystems.pml