Research
Software Systems

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

Applications

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

Projects

Projects marked        were added after the UNSW application deadline.

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/

A Verified C Library (+USyd)

Toby Murray, Callum Bannister

Abstract: With a verified kernel (seL4), and a verified compiler (compcert), the only missing link to support fully-verified low-level systems code is a verified language runtime. For C, still the most widespread systems-programming language, this mostly consists of the standard C library, which provides both commonly-used library routines (string manipulation, searching & sorting, ...), and a wrapper for the operating-system interface (memory allocation, IO, ...). This project provides the opportunity to contribute to the formative stages of the next big systems-verification project! The project is to tackle a particular subset of the library (e.g. strings), write a formal specification, code and debug a high-performance implementation, and formally verify it. To do so, you will use state-of-the-art formal verification tools currently under development at NICTA, and contribute at the cutting edge of this rapidly-expanding field. We anticipate that the final library will be open-sourced, allowing for widespread use in critical systems development.This project would suit a student with both strong low-level programming skills, and an interest in verification, formal methods,or mathematics.

Novelty: Validating new tools and approaches to low-level software verification; Contributing to the world's first verified C library.

Outcome: A verified high-performance implementation for a subset of the C library.

 A Verified Forth Interpreter (+USyd)

Gerwin Klein, Rafal Kolanski

Abstract: Java is taught to students everywhere. Did you know that the Java Virtual Machine (JVM) bytecode language is stack-based? Forth is the first stack-based language.

The Forth programming language is unique, efficient, fun to play with and suitable for deployment on even the simplest embedded systems. It is used in boot loaders, in space (e.g. NASA's ROSETTA mission), and its tiny runtime means it can often appear on new platforms before any other programming language. It even runs on AVR microcontrollers!

At NICTA, we are interested in high-assurance software systems, in particular those we can prove properties about. To prove these properties, we use the Isabelle/HOL interactive theorem prover.

Given that Forth is small enough to learn and work on over a summer, we think it would be fun to create a verified Forth interpreter.

Novelty: To our knowledge, there are no mechanised formalisations of Forth runtimes, nor verified interpreters. Given a verified interpreter as a starting point, this can then be coupled with a machine specification in order to port it to a specific device, even going as far as being able to reason about programs that run on it.


Outcome:An interpreter for Forth that runs, is proven not to crash or trample memory, and is fun to play with.

The participant will gain knowledge of using formal methods to verify properties of programs, learn the Isabelle/HOL theorem prover, and have some fun with a programming language that created the stack-based paradigm.

Reference Material Links:
Isabelle/HOL: http://mirror.cse.unsw.edu.au/pub/isabelle/index.html
Forth: http://en.wikipedia.org/wiki/Forth_(programming_language)
Trustworthy Systems project: http://www.ssrg.nicta.com.au/projects/TS/
Software Systems Research Group (SSRG): http://www.ssrg.nicta.com.au/

Designing a Standard Library for Automotive Applications

Ralf Huuck, Chunxiao Lin

Abstract: Automotive software development is typically subjected to much more rigour than average enterprise software. One of the approaches taken in industry is to design and implement software for compliance with the MISRA C/C++ standard.

However, much of the standard libraries used in automotive development are themselves not MISRA compliment, diminishing the value and trust put into automotive applications.

The goal if this summer project is to apply NICTA's Goanna code analyser to detect MISRA violations in the standard libc library and to work towards a MISRA compliment alternative whenever such violations are detected. A good understanding of C and some software development experience is required.

Novelty: The project would be the first of its kind delivering progress to an automotive compliant standard C library. It is expected that this can lead to future publications and industrial uptake.

Outcome: By the end of the summer project the student is to have developed a prototype library to demo the difference to the state of art.

 Formalising Berge's Lemma from Graph Theory (+USyd)

Christine Rizkallah, Toby Murray

Abstract: A matching in a graph is a subset of the edges of the graph such that no two edges share an endpoint. A maximum cardinality matching is a matching that contains the maximum possible number of edges. An augmenting path is a path that that starts and ends with edges not in the matching and alternates between edges in and not in the matching. Berge’s theorem states that a matching is a maximum cardinality matching if and only if there is no augmenting path. At the trustworthy system group at NICTA we use the theorem prover Isabelle/HOL to prove that programs are correct. The goal of this project is to learn about Isabelle/HOL and formalise the proof of Berge’s theorem in Isabelle/HOL. This proof can be later on used in verifying the maximum cardinality matching algorithm.

Novelty: This work will contribute with the formalisation of Berge’s theorem in Isabelle/HOL. 

Outcome:The result of this work can be used to verify a complex algorithm from the field of graph theory, namely the maximum cardinality matching algorithm.

Reference Material Links:
http://en.wikipedia.org/wiki/Berge's_lemma
https://www.cl.cam.ac.uk/research/hvg/Isabelle/
http://www.mi.fu-berlin.de/wiki/pub/ABI/AlgLecture5Materials/GraphLect3.pdf

 Formalising Theorems from Social Choice Theory (+USyd)

Christine Rizkallah, Gerwin Klein

Abstract: Social choice theory is the study of mechanisms for collective decision making where preferences of individuals are aggregated to produce a social welfare function. It is a subfield of game theory that receives much interest from computer scientists, mathematicians, and economists. There are many interesting classical results in the field of social choice theory including impossibility theorems such as Arrow's impossibility theorem and Sen's impossibility theorem. There are also axiomatic characterizations of voting methods such as May's characterization of the majority rule and Young's characterization of scoring rules. There are also classical voting paradoxes such as Condorcet's paradox, Anscombe's paradox, and the No-Show paradox. Some of those amusing results have been formally proven correct in the theorem prover Isabelle/HOL. The goal of this project would be to formalise a theorem of your choice in Isabelle/HOL.

Novelty:This work will formalise a classic theorem from the field of social choice theory. Judging from previously formalised results it will also probably reveal errors or incompleteness issues with the original proofs.

Outcome:This work will be added to an existing collection of formalised theorems from that domain.

Reference Material Links:
https://staff.fnwi.uva.nl/u.endriss/pubs/files/EndrissLPT2011.pdf
http://en.wikipedia.org/wiki/Social_choice_theory
https://www.cl.cam.ac.uk/research/hvg/Isabelle/

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/

Offline Proof Search for Isabelle/HOL (+USyd)

Gerwin Klein, Rafal Kolanski

 Abstract: 

The theorem prover Isabelle/HOL has a search facility that helps users to find existing proofs and definitions and use them in their own developments.

One current limitation of this search mechanism is that it can only find theorems that have already been processed in the current proof session, but it cannot find theorems from other sessions or from proof collections such as the archive of formal proofs.

The aim of this project is to develop an offline storage format for Isabelle/HOL theorems and adjust the search mechanism such that it accesses this offline storage format.

The project requires knowledge of a functional programming language, such as standard ML, OCaml, or Haskell. Knowledge of Scala is a plus.

Novelty: The new offline search will make a much larger database of formal facts available to Isabelle/HOL users than before and thereby increase productivity in formal proofs.

Outcome: An proof search implementation in standard ML and offline storage format. Optionally, also a user-interface component for the search in Scala.

Reference Material Links:

Isabelle: http://mirror.cse.unsw.edu.au/pub/isabelle/
Archive of Formal Proofs: http://afp.sf.net/

Open Theory Import for Isabelle/HOL (+USyd)

Gerwin Klein, Rafal 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/

 Proof Engineering -- Working with large-scale proofs (+USyd)

Gerwin Klein, Joel Beeren

Abstract:
seL4 is currently the world's only general-purpose microkernel whose functionality has been formally verified down to the code level. This machine-checked formal proof gives us very high assurance that the logic of the program is correct.

However, the seL4 microkernel is not a static object - new features are added regularly, and the proofs must be augmented to retain their trustworthiness. Furthermore, new additions to the proof itself -- for example, removing existing assumptions or establishing the absence of information flow -- require the original proof to change, often quite dramatically.

The aim of this project is to verify a small property of your choice on top of the seL4 functional correctness proof in the prover Isabelle/HOL and investigate the proof engineering aspects that are encountered in that proof.

Novelty: New data on proof engineering in establishing a previously unproven property on seL4 and increasing the level of assurance associated with the kernel.
Outcome: An Isabelle/HOL proof of a small property over the seL4 microkernel.

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/HOL: http://mirror.cse.unsw.edu.au/pub/isabelle/

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

Toby Murray, Yutaka Nagashima

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

CDSL is a purely functional domain-specific language with linear types. From a well-typed CDSL program, the CDSL 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 CDSL.

SSRG has implemented multiple file systems in CDSL. In the development of these file systems, the CDSL foreign function interface allowed us to call C functions from CDSL code where they can be best implemented in C. The goal of this project is to verify that these C functions fit into the CDSL 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

SMT Solvers

SMT Solvers for C/C++ Test Case Generation (+USyd)

Ralf Huuck, Chunxiao Lin

Abstract: SMT solvers are automated decision procedures for decidable theories.

In the recent past the have become popular in many application areas including automated program verification. The goal of this summer project is to investigate their use in automated C/C++ test case generation for code coverage and bug detection such as such as buffer overflows or divisions by zero.

Novelty: The summer project will develop new ideas to apply SMT solvers for test case generation and improved software analysis.

Outcome: By the end of the internship it is expected that the candidate has a good understanding of SMT solvers, is able to generate models by himself and has successfully used an SMT solver to generate test cases automatically.

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

eChronos Robot (+USyd)

Peter Chubb, Kevin Elphinstone, Alex Kroh

Abstract: NICTA and Breakaway Consulting have together developed a simple real-time operating system, that runs on ARM and PowerPC processors. This project aims to evaluate its suitability as a platform for robotics.

The work will involve porting the os to an existing robotics platform (the TI evalbot), and building software on top to get the robot to exhibit interesting behaviours.
If time permits, two extensions are available:
1. To build an iOS or Android app to control the robot
2. To design and build a simplebot as a cheap open-hardware platform using the software.

Novelty:  eChronos is a new OS framework. This work will help to mature it, and to show what (missing) features are really needed to make it truly useful.

Outcome:

  •  A port of eChronos to the TI Stellaris SoC
  •  Device drivers for timers, wheel motors, etc.,
  •  A simple robotics app running on top of eChronos
  •  (maybe) an app running on iOS or Android to control the robot

  Interrupt-Related Covert Channels on seL4

Description of this topic is in the Security section.

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

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.

Middleware

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

Christine Rizkallah, Toby Murray

Abstract: Build the world's first secure network stack by writing it in our special language. At NICTA, we developed a new language called CDSL for writing verified by construction software. The CDSL 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 CDSL. This may contribute to enriching CDSL 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 CDSL language in the domain of network stacks.

Outcome: The outcome of this work is testing whether the CDSL language has sufficient expressivity to be used to implement network stacks. This work will be used to extend the CDSL 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.

 Designing a Standard Library for Automotive Applications

Ralf Huuck, Chunxiao Lin

Abstract: Automotive software development is typically subjected to much more rigour than average enterprise software. One of the approaches taken in industry is to design and implement software for compliance with the MISRA C/C++ standard.

However, much of the standard libraries used in automotive development are themselves not MISRA compliment, diminishing the value and trust put into automotive applications.

The goal if this summer project is to apply NICTA's Goanna code analyser to detect MISRA violations in the standard libc library and to work towards a MISRA compliment alternative whenever such violations are detected. A good understanding of C and some software development experience is required.

Novelty: The project would be the first of its kind delivering progress to an automotive compliant standard C library. It is expected that this can lead to future publications and industrial uptake.

Outcome: By the end of the summer project the student is to have developed a prototype library to demo the difference to the state of art.

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.

 POSIX threads on the seL4 microkernel

Kevin Elphinstone, Peter Chubb

Abstract:The seL4 microkernel is a high performance operating system that is formally verified to be correct. POSIX has a standard API for managing and synchronising threads. This project aims to support the POSIX thread API efficiently on seL4, and in a way that is portable between various seL4 projects. The technical challenge here is mapping the various POSIX primitives to seL4 primitives, and implementing the sync primitive in a correct, efficient, and scalable way.

Novelty: Existing solutions are either incomplete, incompatible, or inefficient. A new implementation simultaneously avoiding all thread downsides would be novel in the seL4 com

Outcome: An efficient implementation of POSIX threads that could be adopted by the seL4 community. Open sourcing a successfull project is an option.

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

Clang/LLVM Extension for Code Analysis (+USyd)

Ralf Huuck, Chunxiao Lin

Abstract: The Apple supported Clang/LLVM compiler framework has become popular for applications both in industry and academia. While LLVM reached a high adoption rate it has still some shortcoming for supporting developers by automatic software error detection such as memory leaks, null pointer dereferences and security problems.

The goal of this project is to extend LLVM with the aforementioned capabilities by connected it tightly with NICTA's existing code analysis tool Goanna. A close internal integration could lead to a high adoption in LLVM user community and helping all C/C++/Objective C developers to write better code.

Some previous experience with LLVM is helpful.

Novelty: LLVM has its own software analysis tool for detecting basic flaws in C/C++ as well as Objective C code. This tool, however, is rather limited in capabilities. Extending LLVm to integrate with the Goanna blackend would open up new capabilities for LLVM users and make new technology available to the Objective C community

Outcome: By the end of the summer project the student is to have developed a prototype integration to demo the potential benefits. This prototype can be used as a base for a follow-up thesis.

Cloud-based Code Analysis (+USyd)

Ralf Huuck, Chunxiao Lin

Abstract:

With the ever increasing amount of software produced on shorter development cycles, it is paramount to use automated tools for security and quality checking. For instance, Apple uses automated tools to check for App Store compliance.

However, running software analysis tools such as static analysers or penetration testing tools can be computationally expensive. It might not only require substantial hardware resources, but also analysis time making it difficult to integrate those tools directly in software development processes. The goal of this project is to "outsource" some expensive computation to a cloud environment either locally on VMs or an Amazon AWS environment. The project includes development and experiments to see the benefits and explore its challenges.

Novelty: Running software analysis tools in the cloud is new. This project will be a good test bed for a feasibility study, for learning about combining formal analysis with cloud environments and for opening up the possibility of a subsequent thesis topic.

Outcome: By the end of the summer project it is expected to have gained good insight into accessing cloud environments remotely, how to run analysis tools in the cloud and how to push data to such tools. Moreover, we expect to obtain first performance results and effort estimations. It gives a good opportunity for students to learn about formal verification and distributed systems.

Enforcing Information-Flow Control with Static Code Analysis (+USyd)

Ralf Huuck, Chunxiao Lin

Abstract: Privacy has become a key issue in this cloud computing and Internet-of-Things era. Information-flow control is a proven technology to tackle this issue, by delivering secret data only to those with the correct privilege. Static information-flow analysis is one of the main research topics in this area.

The goal of this project is to utilise the current analysis engine of the static code analysis tool Goanna to implement a new detector for information-flow-related bugs in the program, which in turn helps to improves privacy protection of the software.

Novelty: No product-level static analysis tools currently support dedicated information-flow-related bug detection, and this new Goanna-based detector can take advantage of the efficiency of Goanna and bring information-flow control to software projects with large code bases.

Outcome: By the end of the summer project the student is to have developed a prototype integration to demo the potential benefits. This prototype can be used as a base for a follow-up thesis.

Exploiting the weakest link in high-assurance systems. (+USyd)

Toby Murray, Kevin Elphinstone

Abstract:

This project explores the interaction between usability and high-assurance systems, that protect critical information with the strength of mathematical proof. NICTA, in conjunction with the Defence Science and Technology Organisation, has developed a highly secure device that allows users to interact with highly classified data at the same time as performing ordinary (risky) work activity, like Internet browsing, on the same desktop. The device is built using NICTA's mathematically verified operating system kernel seL4, and its software design and implementation are currently being formally verified to prove that the device doesn't allow leakage of classified information to the public Internet even under the assumption that the user's operating systems are compromised.

However, this verification at present assumes a perfect user who never accidentally causes a classified information leak. In practice, user error is known to be a fairly common cause of sensitive information breaches. In this project, you will develop attacks that run on the user's operating system and try to exploit the user into unknowingly causing an information leak. This will require writing programs on the Windows operating system that try to fool the user by, for instance, impersonating classified applications, or trick the user into entering sensitive information when they shouldn't be. You will also informally evaluate the applications you write by having them tested by NICTA team members to see how often they fool ordinary users. If successful, this work could form the beginning of a undergraduate thesis that explores the interaction between usability and formally verified security.

Novelty: Explore the interaction between usability and formally verified security. 

Outcome: Develop attacks that run on the user's operating system and try to exploit the user into unknowingly causing an information leak

Reference Material Links:

http://ssrg.nicta.com.au/projects/TS/
http://ssrg.nicta.com.au/projects/seL4/

Fuzz testing a new language and compiler (+USyd)

Toby Murray, Matt Fernandez

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 CDSL 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 CDSL programs. It is expected that this will in turn lead to a more robust CDSL compiler.

Reference Material Links:
CDSL: 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/

 Javascript Security Vulnerability Detection (+USyd)

Ralf Huuck, Chunxiao Lin

Abstract: Javascript has become one of the most popular programming languages in the recent years. At the same time Javascript vulnerabilities have been one of the main reason for common exploits and hackers gaining access to systems. While other more traditional languages have a wide range of code analysis tool support to prevent some of the worst mistakes and vulnerabilities, the current situation for Javascript is still very unsatisfactory.

The goal of this project is to investigate common causes for Javascript vulnerabilities, examine which of those can be prevented by automated static analysis and to develop future recommendation or (if time permits) extend NICTA's exisiting code analysis tool Goanna to basic Javascript support.

Novelty: Javascript has still very little tool support for preventing quality and security problems. The summer project aims at making first contributions by understanding the problem space and working towards extending existing tools with Javascript support.

Outcome: By the end of the summer project the student is expected to have developed a javascript vulnerability mapping, a suggested set of checks that should be applied to Javascript programs and a potential prototype integration with an existing tool

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.

Sensing Security Issues through Software Monitoring

Ralf Huuck, Chunxiao Lin

Abstract: Software security is a critical topic for many companies and research groups. Especially, with the rapid development of code bases and new multi-core features, security becomes a bottleneck in software development. Automated security analysis techniques are a must to reduce the burden on the software developer.

This project is about using runtime monitors, i.e., sensor, that observe applications and automatically detect if unwanted sequences of events are happening. Part of the project is to compare the state of the art and to increase system security significantly by expanding the NICTA runtime monitoring approach for detecting malicious events.

This topic can be expanded to a thesis later on.

Novelty: Software security typically entails firewalls, policies and code analysis. The novelty is sensing the execution of code that has been instrumented beforehand by having low-overhead runtime monitors. This gives a different dimension to security and enables a higher degree of confidence.

Outcome: By the end of the summer project the student is expected to have developed a prototype runtime monitor that can sense security problems. This prototype can be used as a base for a follow-up thesis

 

Dependable Cloud

Big Data Provenance

Liming Zhu, Sherry Xu

Abstract: Data provenance is metadata which keeps track of where a piece of data comes from, and what operations have been done to it. This metadata provides a way to assess authenticity, enable trust in the data itself and the analysis results and allows reproducibility. This is particularly important when the data end-users, data analysts, data producers, and data wranglers are different groups of people across exploration and production stages. However, existing data provenance features are often embedded in vendor-specific tools or have strong assumptions of the types of analytics systems or operations and their tracking. There are also no good mechanisms of publishing/sharing data with "usable and verifiable" provenance attached. Big data is exacerbating the problem in terms of mechanism efficiency for provenance capturing and sharing. This project looks into how we can keep track of both data and programs by automatically associating version controlled programs to version controlled datasets, independent of systems used. The published provenance should be easily usable for a reproduction of the current dataset.

Novelty: platform independence and usable and verifiable to increase trust in results

Outcome: new mechanism design and implementation to track provenance independent of platforms.

Continuous Deployment for Big Data Analytics Applications

Liming Zhu, Len Bass

Abstract: Data scientists are increasingly moving from small-scale data analytics on a laptop to big data analytics in clusters (e.g. for genome analysis and financial data analysis). However, data scientists still need to perform explorative analytics development on their laptop or a small-scale environment and then deploy the data analytics application to clusters, often with extensive support from data product teams and engineering teams. If any issue arises during on the large-scale deployment or operation, data scientists need to revise their models back at their laptop and repeat the process again. Continuous Deployment/Delivery (CD) is a practice that copes with high frequency and automated deployment of applications. CD practices have been used in many types of applications but its use for data analytics applications and model development is still limited due to distinct model development cycle, data sampling and cluster deployment challenges. This project will expose you to data science and big data workflow. You will work within a team to develop new solutions to automate and simplify the workflow.

Novelty: Adaptation of continuous deployment practices to statistical and machine learning model development and deployment to clusters.

Outcome: survey of challenges in using continuous development in big data analytics proposed solution and prototypes for subset of issues

 Dependable Auditing on Operations of in-Cloud Applications

Liming Zhu, Len Bass

Abstract: Despite the tremendous potential of cloud computing, organisations that deploy their applications in the cloud may have concerns related to loss of control and dependability issues (e.g. security, privacy and availability). Operations of in-cloud applications are usually a mix of (semi-) automated tasks by both in-house administrators and cloud infrastructure providers reacting to rapidly changing environment. It is often difficult to establish assurance cases and track accountabilities of these operations in three cases 1) for compliance testing with respect to legal requirements such as Basel III 2) forensic operations when there has been a security breach, and 3) when the applications encounter problems and it is necessary to get compensation from the cloud vendor.This project will investigate the both the technical mechanisms and legal issues in auditing operations of in-cloud applications. Specifically, the student will examine the current logging facilities related to typical operations of in-cloud applications and cloud infrastructure vendors's compliance process and evidence requirements. The student will then propose improvements in logging and auditing so better assurances and accountability could be established.

Novelty: Linking low level logs and security mechanisms with high level auditing and compliance requirements

Outcome:proposed improvement in logging and traceability between logs and high level requirements. Implementation of a prototype that captures the traceability and the associated assurance case.

Modelling and Analysis of Asynchronous Rolling Upgrade (+USyd)

Daniel Sun, Liming Zhu
Abstract: Rolling upgrade is a practical technique that can upgrade distributed software systems with little availability loss during upgrading. To assure that robust rolling upgrade in clouds with the presence of failures is a topic within Dependable Cloud Operation in SSRG, NICTA. Synchronous rolling upgrade has been well studied, while asynchronous rolling upgrade hasn't been well analysed. This project aims at modelling and analysing Asgard, a software tool built by Netflix to support asynchronous rolling upgrade. A student will be assigned a mission to extend synchronous case to asynchronous case. The candidate techniques that will be adopted are continuous time Markov models, two dimensional Markov process, Hyper- or Hypo- exponential distribution, and phase distribution. This project also needs to program in either Amazon Web Service or NECTAR Cloud of Australia. A student following this project can acquire sufficient skills in modelling, analysis, programming for cloud computing.

Novelty: This work will extend a on-shelf cloud software tool and result in a concrete instance for popular DevOps.
Outcome: A software tool extending Asgard to provide predictable DevOps.

 Understanding and Improving Operational Processes in Large-scale Distributed Systems

Liming ZhuLen Bass

Abstract: Most failures of modern large-scale distributed systems happen during sporadic operational processes (such as upgrade, backup, recovery and configuration changes). The overall goal of the project is to understand the characteristics of these complex operational processes so that we can improve the overall dependability of the systems especially during sporadic operational activities. These operational processes are always a combination of automated processes and human-intensive processes which require different types of resources (software artifacts, computation power and humans) to carry out. These resources show a wide range of different characteristics in terms of their error-proneness, undoability, availability over time and dependency and etc. These put significant challenges in choosing and scheduling these resources appropriately and their impact on overall system dependability. The project will expose students to a set of real world operational processes for large-scale distributed systems. The project involves the modelling these processes in (semi-) formal process languages and investigation of analysis methods (and tools) to determine the impact of an operational processes on system dependability.

Novelty: applying process analysis and monitoring to operational processes for improving dependability

Outcome: new operational processes models, analysis methods and progress monitoring tools for typical operational processes