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

Applications

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

Projects

Projects marked  NEW were added after the UNSW application deadline.

Formal Methods

Theorem Proving

Automating Invariant Proof Re-Use

Daniel Matichuk and Gerwin Klein

Abstract: In interactive theorem provers, such as Isabelle, users state hypotheses and collaboratively interact with the system to prove them as facts. The proof calculus developed in the L4.verified project uses a monadic variant of Hoare logic to reason about program invariants. A proof developer must state the pre and post condition of each function. He then reasons about each step of the function, ultimately demonstrating the precondition is strong enough to imply the postcondition.

The reasoning about these “intermediate” function states, however, is lost once the proof is finished, only the initial hypothesis is retained for use in further proofs. If the function needs to be reasoned about again, to prove other invariants or more complex properties, logic from the original proof will be needed. Often this involves copy-pasting proof scripts, resulting in significant maintenance overhead when the proof needs to be updated.

A prototype proof calculus exists to to address this shortcoming, allowing intermediate results about program states to be saved and re-used, but suffers from a lack of automated tools to support it. This project aims to implement automated procedures for supporting this new calculus, and ideally integrating it into existing L4.verified proofs.

Novelty: It is only recently that proofs of this size have existed, and thus the cost of duplicated reasoning has not been apparent until now. The development and automation of a new calculus to avoid this is a novel extension to the established state-of-the-art for formal verification in interactive theorem provers. This work could impact the development of all proofs using the current framework, both in seL4 and other ongoing verification projects at NICTA.

Outcome: A collection of proof methods (and other tools, as necessary) to support the automatic re-use of invariant proofs inside of the monadic Hoare logic used in L4.verified.

References

A Verified C Library

Gerwin Klein and June Andronick

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.

Formal Verification of Concurrent Programs Flying Quadcopters

June Andronick and 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.

Formally Verified Multi-Level Terminal

Toby Murray and June Andronick

Abstract: A verified multi-level terminal, which allows computer users to access information of different national security classifications simultaneously, on the same machine without unwanted information leakage, has been a dream for more than 30 years. This dream has remained unrealised because, until now, we have lacked sufficiently secure operating systems on which to build such a system, and sufficiently advanced formal verification infrastructure with which to verify it. In the last 10 years, NICTA has built and brought together both of these missing ingredients in its Trustworthy Systems project and the seL4 microkernel.

As part of the Trustworthy Systems project, we are building a multi-level terminal system on sel4. The goal of this summer project is to apply and extend the existing security theorems for the seL4 kernel in order to prove the main security property of the multi-level terminal: that it never leaks high-classification information. This proof will be performed in the Isabelle/HOL theorem prover and build on the existing confidentiality proof for seL4.

You will be working closely with a senior researcher, as part of a team comprising graduates, PhD students, and senior researchers who are building and verifying the multi-level terminal. Your work will form a critical part of its verification, and the overall assurance case for its deployment in high-security environments like Defence

Novelty You will produce the world's first security proof for a Multi Level Secure system built on a formally secure security kernel. We are planning to open-source the multi-level terminal system and its security proofs. As such, it will be the first high-security system that is both open source and open proofs.

Outcome: A formal noninterference security theorem for a multi-level terminal system built on sel4.

References

Robustness for Binary Verification Using CSmith

Thomas Sewell and Gerwin Klein

Abstract: We have recently introduced a prototype mechanism for proving that the machine code produced by standard compilers such as GCC is a correct implementation of the input program [1]. This mechanism links the NICTA understanding of the C language [2] to the Cambridge definition of the semantics of the ARM architecture [3]. The prototype has been used to prove that the compiled binary of the seL4 microkernel adheres to the same specification as its source code [4].

This prototype is now being used for more substantial projects, and efforts are being made to mature it into a robust and reliable tool. In addition to the pragmatic interest in reliability, there is a question of research interest to be answered also: what are the real limitations of this otherwise promising approach?

To examine this question in more detail, this project will adapt the CSmith tool [5] and a variety of C compilers to produce test inputs to stress-test the proof mechanism. The project will also look into understanding and addressing the limitations that will be found in the prototype, though it is not clear yet what this will involve.

Novelty: This project will create evidence of interest in answering a long-running research question about the effectiveness of translation validation. It will also contribute directly in additional robustness in the NICTA binary-verification tool.

Outcome: A framework for generating test cases for binary verification, and a statistical analysis of the effectiveness of the verification and the extent of limitations.

References:

Verified Software Components

June Andronick, Matthew Fernandez

Abstract: The next step towards formally verified (secure) software systems. The Software Systems Research Group at NICTA has developed a component platform (CAmkES) for building high assurance microkernel-based systems. The correctness of a component system is predicated on the correctness of key components, for which strong evidence is required. The goal of this project is to verify the functionality of specific user-level software components, with an eye to using the resulting properties in a compositional proof of the correctness of an entire system.

Novelty: This work will contribute to research efforts of providing provably correct component software systems.

Outcome: A software component (or multiple components) with formally verified functional properties.

SMT Solvers

Adding New Theories to SMT Solvers

Franck Cassez, Ralf Huuck

Abstract: Automated software analysis for C/C++ programs can be performed via trace refinement and the method makes use of SMT solvers that are automated decision procedures for decidable theories (e.g. linear integer arithmetic, arrays, bit vectors). Modern programming languages like Scala can be paired up with solvers to add new theories e.g. predicate on strings (length, etc).

The proposal should be implemented in Scala in the tool Perentie and a set of benchmarks should demonstrate the benefits of the new technique. The project aims at extending our software analysis tool, Perentie (academic version of Goanna) with some new decidable logics of interests primarily C/C++ strings. The project requires strong interest in logic and program verification as well as programming in Scala.

Novelty: Adding support for ad-hoc theories is a primary concern in software analysis. The project aims at developing a framework that ca be re-used to add new theories later on. It improves the core analysis engine.

Outcome: It is expected that the candidate will acquire a good understanding of SMT solvers, Scala programming and develop new theories combining functional programming and SMT solving.

Combining SMT Solving and Abstract Interpretation for C/C++ Program Analysis

Franck Cassez, Ralf Huuck

Abstract: Automated software analysis for C/C++ programs can be performed via trace refinement. This approach while very powerful has not been fully exploited so far. The method makes use of SMT solvers that are automated decision procedures for decidable theories (e.g. linear integer arithmetic, arrays, bit vectors). Combining abstract interpretation techniques with SMT solving in trace refinement can be speed up the analysis and make it more accurate.

The project aims at integrating these two techniques in our software analysis tool, Perentie (academic version of Goanna).

The proposal should be implemented in Scala in the tool Perentie and a set of benchmarks should demonstrate the benefits of the new technique. The project requires strong interest in logic and program verification as well as programming in Scala.

Novelty: This will be the first time abstract interpretation and SMT solving are combined in the trace refinement approach.

Outcome: It is expected that the candidate will acquire a good understanding of SMT solvers, standard abstract interpretation techniques and propose a sensible (theory-wise) combination of them.

Protocols

Automatic Translation of Routing Protocol Specifications

Peter Höfner and 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.

Implementing Secure Protocols for Quadcopters

Peter Höfner, Gerwin Klein

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 the basis for developing truly secure software systems. The project will concentrate on communication protocols, which are part of nearly every system. These protocols are either used for communication between components of a microkernel or to communicate with other systems. The goal of the project is to implement communication protocols for quadcopters communicating to a ground station (including authentication and encryption).

The protocols will be defined by a formal specification, which is verified by members of the team.

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

Outcome: Communication protocols running on a quadcopter; the software of the quadcopter is based on seL4.

Model Checking of Mesh Network Routing Protocols

Peter Höfner and 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

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

Systems

Kernels

ARM Hypervisors: seL4 vs KVM NEW

Gernot Heiser and Alex Kroh

Abstract: KVM for ARM uses an approach called "split virtualization" (aka microkernels reinvented), with a small "Lowvisor" in Hyp mode and a complete Linux/KVM VMM in kernel mode. An implication of this design is that on each hypercall or virtualisation trap it requires a full world switch, including saving and restoring the complete virtual machine (VM) state in software. The result is a high basline cost of VM exits. seL4, in contrast, runs a minimal VMM in user mode, and does not require a world switch to invoke it, resulting in a much lower baseline cost.

The aim of this project is to evaluate the performance of virtualised ARM Linux on seL4 and KVM, and, where appropriate, tune the seL4 VMM performance.

Novelty: KVM is presently the best supported open-source ARM hypervisor, and considered the benchmark. A paper in ASPLOS'14 describes the design and analsyses the performance, this is presently the standard reference for hardware-supported virtualisation on ARM. The point of this work is to demonstrate that we can do better, and thus establish a new performance baseline. We should also be able to analyse the implications of ARM's design, especially the design decision to leave saving and restoring of VM state to software.

Outcome: Critical analyis of seL4 virtualization performance and of harwdare and software design tradeoffs. Great opportunity for an ASPLOS paper.

Effective Cross-Kernel Communication

Gernot Heiser and Kevin Elphinstone

Abstract: For reasons of scalability and verifiability, seL4 uses a multikernel approach where cores do not share an L2 cache. This implies that kernels on different cores do not share state, and communicate asynchronously via mailboxes.

This project is to design, implement and evaluate a user-level communication package for threads running on different cores on top of the kernel's minimal mechanisms, and compare to other approaches, e.g., Linux IPC. This will, no doubt, require work on the seL4 mechanisms too. In fact, the project could be split between two students, one working inside the kernel and one at user level.

NICTA's Trustworthy Systems team are world leaders in research for providing unprecedented security, safety, reliability and efficiency for software systems. Successes include deployment of the OKL4 microkernel in billions of devices, and the first formally verified OS kernel, seL4. Present activities include covert channel mitigation, mixed-criticality real-time systems, and automatic code-proof co-generation. We are building a complete seL4-based high-assurance system for autonomous helicopters, like Boeing's Unmanned Little Bird, in a project funded by US DoD. You will work with a unique combination of OS and formal methods experts, producing high-impact work with real-world applicability, driven by ambition and team spirit.

Novelty: Multikernels are new, and other than the Barrelfish paper there is little evaluation, and what there is is on x86, with vastly different tradeoffs to our ARM platforms. Furthermore, seL4's idiosyncrasies mean that previous resuts are not necessarily transferrable. Given the significance of seL4, this work can lead to publishable results.

Outcome: Understanding of how to do user-level communication in an seL4 multikernel; report describing design, implementation and evaluation.

References

Fast Cross-Core Communication

Gernot Heiser and Kevin Elphinstone

Abstract: For performance and verifiability reasons, seL4 uses a big kernel lock (BKL) when running on multicore platforms with shared caches. This works without impacting performance as long as contention on the lock is high. Synchronous communication between cores has the potential to increase lock contention, so asynchronous communication is preferred. However, the present kernel implementation is not optimised for this.This project is to design and implement a testbench for cross-core communication that is representative of real-world workloads. It will then use this testbench to evaluate and improve the performance of cross-core asynchronous IPC.

Novelty: L4 kernels are generally the fastest microkernel designs, and seL4 (despite being the most highly assured OS kernel ever) is presently the fastest L4 kernel, in terms of synchronous IPC. No-one has, to date, seriously evaluated and optimised asynchronous IPC, despite this being the obvious mechanism for multicores. The project has the potential of publishable results.

Outcome: High-performance cross-core communication in a BKL seL4 kernel.

Interrupt-Related Covert Channels on seL4

Description of this topic is in the Security section.

Protected-Mode eChronos

Gernot Heiser and 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

seL4 on MPU-only Microprocessor

Gernot Heiser and Kevin Elphinstone

Abstract: seL4 is designed for microprocessors with full virtual-memory support. However there are interesting use cases for a verified kernel on lower-end processors that only have a simple memory-protection unit (MPU). A particularly interesting case is the ARM Coretex M4, which has the same instruction-set architecture as the A9/A15 processors whcih seL4 presently supports, so a port to the M4 would be trivial except for memory management.

seL4's approach to memory management should be easier to adapt to MPUs than earlier L4 kernels. This project is to investigate the design and implementation changes required for an MPU-based seL4, do the port 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, such as the M4. Success of this project will complete coverage.

Outcome: seL4 version that runs and performs on M4 processors.

Sloth vs eChronos

Gernot Heiser and 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

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.

Generated Verified File System

Gernot Heiser and Peter Chubb

Abstract: NICTA's project to co­generate file­system implementations and their correctness proofs aims to dramatically reduce the cost of verified software. It uses embedded domain­specific languages (EDSLs) to specify the logic of a file system, and generates code and proofs from that specification.Important for the credibility of the approach is to demonstrate its generality: that the same EDSL and underlying machinery can be used to generate a wide class of file systems, and that the resulting systems perform competitively. This project is to apply the framework to a different kind of file system than what it has been used for before, eg a log­structured file system such as XFS. It is to test and improve the suitability of the tool chain, and thoroughly evaluate the resulting file­ system against manually­written high­performance Linux implementations.

Novelty: Being able to generate verified and performant file systems from DSLs is big

Outcome: Working journal­based file system and understanding of the strengths and limitations of the co­generation approach.

High-Assurance POSIX Implementation

Ihor Kuz, Toby Murray

Abstract: The Open Group is currently working on a standard that defines a POSIX-subset for high-assurance systems, called the Mils™ API. This project would investigate implementing the Mils API on top of the seL4 microkernel, whose functional correctness and security has been formally verified.

Novelty: This project would produce the world's first implementation of the Mils API for a microkernel implementation whose security and functional correctness has been formally verified.

Outcome: A design and (probably partial) implementation of the Mils API on top of the seL4 kernel.

High-Performance User-Level Device Drivers

Kevin Elphinstone, Ihor Kuz,

Abstract: The microkernel approach to operating system construction implies that most OS components, including device drivers, execute outside the kernel as user-level processes. This raises an important research question: Can user-level drivers perform as well as in-kernel drivers? This question has been the subject of a long-lasting debate in the OS community. The goal of this project is to answer this question in the context of the seL4 microkernel-based OS. Working with a small team of NICTA undergraduate and postgraduate students and researchers, you will design and implement a user-level driver framework for seL4 along with one or several high-perfomance drivers.

Novelty: This work will produce important experimental data on the performance of user-level device drivers in a modern microkernel-based systems, which will guide further research in this area.

Outcome: A high-performance user-level device driver framework for seL4.

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.

Trustworthy File-System Compilation using Binary Tools

Thomas Sewell and Liam O'Connor-Davis

Abstract: This project will examine an alternative approach to validating the compilation of a domain specific language (DSL) used for file-system implementation. File systems are currently too important to fail but too large to prove correct by hand. The NICTA Trustworthy File Systems project [1] aims to address this by introducing reusable DSLs which allow file-system implementations to be expressed in their most natural core. These languages require a trustworthy compilation path. The current approach is to build a validating DSL to C compiler. The alternative approach which will be considered in this project is to compile the DSL down to machine code, and apply new methods for comparing machine code to source code [2].

Novelty: This project would introduce a novel approach to compiling DSL software in a correct-by-construction environment. It is a key building block in building a useful DSL-based software development environment with a proof of correctness.

Outcome: During the summer project the effectiveness of this approach will be tested, and steps will be taken towards verifying all aspects of the calcuation. Full validation will probably require a subsequent project.

Verified Software Components

Description of this topic is in the Theorem Proving section.

Virtualisation for Security

Description of this topic is in the Security section.

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

High-Assurance POSIX Implementation

Description of this topic is in the Middleware section.

Interrupt-Related Covert Channels on seL4

Gernot Heiser and Toby Murray

Abstract: seL4 is the world's only general-purpose kernel with a proof of confidentiality that applies to its binary implementation. This proof provides very strong guarantees that the kernel enforces data confidentiality --- i.e. prevents information leakage that would violate the system's access control policy --- with some side conditions. The side conditions include interrupts being disabled and that the proof does not cover covert timing channels.

One such timing channel arises when interrupts are enabled: the arrival of interrupts causes the time-slice of the current thread to be extended, because interrupt-servicing pre-empts the currently running thread, allowing it to indirectly observe interrupts that should otherwise remain secret. The goal of this project is to investigate mechanisms to mitigate and close such channels, while ensuring adequate interrupt response latencies.

We expect a natural trade-off between channel bandwidth and interrupt-response latency, so further work in this project would investigate this trade-off by applying existing tools to measure the effectiveness of various mitigation strategies against benchmarked latencies. This project therefore involves a combination of kernel implementation, benchmarking and analysis.

Novelty: If successful, the results of this project could be incorporated into future versions of seL4, and be applied to relax the assumptions of the seL4 confidentiality proof, increasing seL4's applicably for applications that demand both high-performance and high-assurance. seL4 would become the world's only kernel with a code-level confidentiality proof that holds when interrupts are enabled.

Outcome: The design, implementation and empirical evaluation of kernel mechanisms to mitigate interrupt-related covert channels for seL4.R

References

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.

Secure Quadcopter

Ihor Kuz, Alexander Kroh

Abstract: Develop a secure quadcopter based on seL4
Quadcopters are becoming popular as unmanned aerial vehicles (UAV) and toys. We wish to demonstrate the capabilities of our seL4 secure microkernel in providing a secure platform to the end-user. This project involves the construction and software design of a secure UAV. The platform shall run our trusted microkernel and demonstrate its security properties. This project will involve creativity, coding, playing and the occasional crash landing.

Novelty: We have a microkernel with formally verified security properties, however, very few systems that actually take advantage of it. The result of this project will be a unique secure system running on a formally verified microkernel.

Outcome: The result of this project will be a flashy demo that shows off the capabilities of the seL4 microkernel and systems based on it.

seL4-based Distributed Systems

Description of this topic is in the Middleware section.

Virtualisation for Security

Ihor Kuz, Adrian Danis

Abstract: Security through virtualisation is a hot topic, but does it really buy you anything if you can't trust the hypervisor? At NICTA's Software Systems Research group we are developing a trustworthy seL4-based virtual machine monitor. This provides the ideal platform to implement a virtualisation-based security environment (i.e., one based on isolation where each application is run in a separate virtual machine so that applications cannot maliciously interfere with each other, an example of this is Qubes: http://qubes-os.org/). The goal of this project is to design and implement a prototype virtualisation-based security solution on seL4 and show that it is, in fact, secure.

Novelty: This work will raise the bar for people wanting to provide security through virtualisation.

Outcome: A prototype implementation of an seL4-based system that provides application isolation through virtualisation.

Dynamic Security Architecture Description Language

Ihor Kuz, Matthew Fernandez

Abstract: Model and analyse security properties of dynamic software systems. In NICTA's software Systems group we have previously shown that we can model, verify security properties, and generate code from the software architecture description of static systems (that is, systems whose structure (processes, threads, and inter-process communication channels) never changes). We wish to make it possible to do the same for dynamic systems, that is systems whose software architecture can change at run time. The goal of this research is to propose a new model for dynamic software architectures that takes into account authority and authority change in the modelled systems.

Novelty: This will be the first dynamic architecture description language that takes into account the authority to make changes to the system architecture.

Outcome: An architecture description language for dynamic software architectures and tools for analysing security properties of such architectures.

Served by Apache on Linux on seL4