ERTOS Summer Projects 12/2010 – 2/2011
These project are available to holders of the UNSW/NICTA Summer Research Scholarships. We may also provide some additional scholarships for good students with the a strong OS background who miss out in the official process. Talk to us if you are interested.
- Linux Projects
- Device Driver Projects
- Componentisation Projects
- L4 and Embedded Systems Projects
- Verification Projects
Projects marked are not on the official list but are available nevertheless.
Project title: Universal boot loader for embedded systems
Supervisor: Gernot Heiser
Collaborating supervisor: Peter Chubb
Research Area: Software systems / operating systems
Abstract of reseach project:
Embedded systems development is different from application development in many ways. It tends to be more low-level and tightly integrated with the operating system. Also, development and compilation is typically performed on a separate system (desktop or build farm). This then requires loading the new system image onto the embedded hardware platform using a boot loader, typically once per edit-compile-run cycle. The boot loader is like a small operating system, containing drivers for the device(s) used to loading the code.
There are a variety of possible boot devices, with different characteristics, ranging from serial port (slow) via JTAG (faster), DFU (even faster) to TFTP via network (fastest). Faster devices are more complex, which means that writing the drivers is much more work. For this reason, many embedded platforms only support the slowest boot devices in their boot loader, making system development extremely tedious.
However, many of these platforms support Linux as an OS, or a port of Linux is relatively straightforward. Linux, of course, comes with drivers for just about any device. The purpose of this project is to scrap the boot loader and replace it by Linux, thus leveraging the available driver base. You will investigate what is required to use Linux as a boot loader, and demonstrate the approach on the Panda board, a state-of-the-art multi-core embedded development platform based on an ARM Cortex A9 processor.
Requirements: Excellent C programming skills, desire to get your hands dirty, interest in playing with cool hardware, desire to learn about operating systems and embedded systems
These projects are related to research on device-driver reliability. They will be supervised by Leonid Ryzhyk.
- LR01: Reliable Device Driver Framework for Linux
As part of an effort to put an end to the numerous software failures caused by buggy device drivers, our research group is developing a new device driver architecture for Linux. This architecture will eliminate certain types of bugs by design and will make writing a correct driver easier. In this project, you will develop Linux kernel components as part of our driver development framework and will implement one or more drivers using this framework. In the course of the project, you will learn to write safe and efficient kernel code and will gain experience in device driver development. The outcome of this work will be published in one of the top OS conferences and will be proposed for inclusion in the mainstream Linux kernel.
- LR02: Modelling of I/O devices for automatic device-driver synthesis
Device-driver development is a notoriously difficult and error-prone task. Device-driver synthesis is a novel technology developed at NICTA that aims to replace the conventional manual driver development process by an automated process where a device driver is generated automatically by a tool based on a formal specification of the I/O device. In this project you will develop specifications of one or more I/O devices for use in driver synthesis. Such a specification constitutes a high-level model of device operation written in the SystemVerilog hardware description language (HDL). You will validate the model by running it side-by-side with the low-level register-transfer-level specification of the device in a simulated environment and comparing the outputs. In the course of the project you will learn the SystemVerilog HDL and acquire skills in hardware modelling and verificaion. Being part of the larger effort to develop practical device-driver synthesis tools, this project can be naturally extended into an honours thesis project on driver synthesis.
These projects deal with the building of componentised operating systems on top of L4 (OKL4 or seL4), and CAmkES the component architecture that supports this. They are supervised by Ihor Kuz and various PhD students.
- IK52: Web Server for L4-based Devices
Any computer system worth its salt must be able to run a web server these days. At ERTOS we are building a research OS based on a component architecture (CAmkES) and a microkernel (seL4). We already have a (simple) network stack, but we still don't have a web-server! What this project will accomplish is to design and build a componentised web server and OS. But, it doesn't end there. The system must be fast. Therefore a significant amount of effort will also be spent analysing and optimising the resulting system.
Novelty and Contribution: Besides contributing to the further development of an embedded OS, this project will provide insights into the design issues and performance tradeoffs involved with componentising application and system services. The completed webserver will also be used to run parts of the ERTOS website.
Expected Outcomes A working web server integrated into our componentised OS. The insight into the design decisions and tradeoffs involved in designing such a subsystem will influence and further drive research into structuring modular, microkernel-based operating systems.
- IK80: Linux as a Component
The ERTOS group has done (and commercialised) much work in virtualising Linux to run on the L4 microkernel. We have also done work developing a componentised microkernel-based OS. However the two essentially live in separate worlds. The goal of this project is to integrate virtualised Linux (and its applications) into the componentised OS. One way to do this is to treat Linux as a large component and develop appropriate interfaces and an appropriate framework for this. The project will investigate the best way to do this and implement a prototype system.
Novelty and Contribution: This project will combine two aspects of the novel research that we do at ERTOS, making both more useful and avalaible to a broader audience of developers. It will lead to a system that can be used in a variety of existing and future embedded devices, including mobile phones and media players.
Expected Outcomes A demonstration system consisting of a componentised OS, a virtualised Linux instance, and applications all coexisting and communicating in harmony.
- IK110: More Efficient Componentised Operating Systems
CAmkES is a component-based software framework for building seL4-based operating systems. This framework allows operating systems to be built out of pre-existing software building blocks, making OS development easier and more flexible, as well as facilitating verification. However, CAmkES currently only allows components to be placed in separate address spaces: while this is good for security and safety, it is bad for performance and optimisation. The goal of this project is to extend the model to allow OS components to share address spaces. This new model must be implemented and evaluated to quantify the benefits of having components share an address space.
Novelty and Contribution: This work will enable the construction of efficient operating systems out of pre-existing software components. The component-based approach to OS development is a key part of the ERTOS strategy to producing highly dependable embedded computing systems, and it is crucial that the resulting systems be efficient and show good performance.
Expected Outcomes An extension of the CAmkES framework to support same-address space components and an evaluation of the performance gain that this brings.
- IK111: Hardware Devices as Operating System Components
At ERTOS we've developed technology for building componentised operating systems. One of the things missing, however, is a clean model for accessing hardware. This project will involve designing and implementing a device access model for CAmkES, our component model, which runs on the seL4 microkernel.
Novelty and Contribution: This work will extend the component-based model down to the hardware interaction level, paving the way to developing componentised device drivers and, ultimately, a fully componentised operating system.
Expected Outcomes An initial model of devices as software components, as well as an implementation prototype for several devices.
- IK112: Secure Software-Based Rootkit Detection
The seL4 microkernel is the only formally verified hypervisor. This verification implies that it cannot be bypassed, except by hardware or BIOS compromise. As such, it provides an ideal platform for implementing rootkit detection for commodity operating systems, such as Linux or Windows, since it combines the flexibility of software-based detection systems with the trustworthiness of hardware-based ones. This project involves extending the seL4-based hypervisor "Wombat" to enable tracing and inspection of guest operating systems, in order to produce a pluggable framework for implementing rootkit detection. This framework could also serve as a useful debugging harness for seL4-based systems, by implementing plugins tailored to common debugging tasks.
Novelty and Contribution: This work would produce the first rootkit detection framework backed by a formally-verified non-bypassable microkernel.
Expected Outcomes A pluggable framework for tracing and inspecting running guest operating systems on top of the seL4 microkernel; a proof-of-concept plugin for this framework that detects a known rootkit infection in Linux.
These projects cover a wide range of operating systems and embedded systems research, mostly dealing with L4 and seL4. They are supervised by Kevin Elphinstone, Gernot Heiser, and various PhD students and research engineers.
- KE90: Lottery Scheduling for Embedded Systems
A flexible CPU scheduling mechanism should be able to accommodate many application domains with only configuration of the scheduler being required. One such scheduler that might fufil the role is a lottery scheduler. A lottery scheduler randomly draws a winner to determine which task runs next. The distribution of tickets to tasks is used to affect the scheduling behaviour.
This project aims to develop an efficient lottery scheduler and an API for managing the ticket distribution.
- KE94: Device discovery in a microkernel-based system.
Secure embedded L4 (seL4) is a microkernel-based operating system that is formally verified to be correct, i.e bug free, under some simple assumptions. Microkernel-based systems can run device drivers as user-level applications, which removes potentially buggy device drivers from the kernel where failure of a driver always results to catastrophic failure of the whole system. Removal of drivers was also a key enabler of the formal verification.
However, drivers are needed by applications to interact with peripherals, and thus a systematic device driver framework is required for the seL4 kernel. Support for device discovery in PCI-based computers is a part of any driver framework. This project aims to look at what is involved in support device discovery in seL4, including looking at whether the code should be in the microkernel, or running as a service at user-level. This project will impart a deep understanding of how modern PC interact with peripherals.
This research project will contribute to our understanding of the best way to support peripherals in a formally verified, microkernel-based, operating system.
The outcome expected is an understanding of what is required of a software framework to enable dynamic device discovery in a microkernel environment. An initial software prototype of such a framework.
- KE95: A 64-bit seL4 microkernel
Secure embedded L4 (seL4) is a microkernel-based operating system that is formally verified to be correct, i.e bug free, under some simple assumptions. Currently, seL4 runs on 32-bit Intel and ARM processors. This project's goal is to extend seL4 to support 64-bit Intel processors. SeL4 is a small kernel of approximately 8,000 lines of C code. Its size makes this project quite achievable in the time frame of a summer project.
seL4 is a world first formally verified microkernel. Knowledge gained from porting to 64-bit processors will be used as input to producing a 64-bit formally verified kernel.
Expected outcome would be a software prototype of seL4 that runs of 64-bit Intel x86 platforms.
- KE96: A small multiserver OS for seL4
Secure embedded L4 (seL4) is a microkernel-based operating system that is formally verified to be correct, i.e bug free, under some simple assumptions. One class of operating systems that can be build on a microkernel is a multiserver operating system, where components of a tradition operating system are separated and run as normal applications, isolated from the failure of other operating system components. This project aims to implement a very simple multiserver operating system on the seL4 microkernel. The exact functionality is up to you, but the expectation would be a simple name service, process service, and maybe file service. The expectation is that this project would build on knowledge gained in COMP9242 advanced operating systems.
The support for multiserver operating systems is a goal of the seL4 microkernel, and this project would be the beginning of evaluating the existing support for such systems.
The expected outcome would be a software prototype of a simple system on the seL4 microkernel.
- GHs100: Secure Browser OS
A secure web browser with a minimum trusted computing base has been propagated as a way to protect against browser exploits, for example IBOS. Such an approach is a big improvement over present practice, but is still at the mercy of an underlying OS which isn't trustworthy.
This is changed with the availability of the formally-verified a seL4 microkernel, which can present a truly trustworthy basis for a secure browser. This project is to design and implement such a secure browser OS on seL4.
Novelty and Contribution: First truly trustworthy web browser.
- GHs101: Evolvable Trustworthy System
The trusted platform module (TPM) specified by the Trusted Computing Group (TCG) and implemented on many PC platforms supports a secure boot and remote attestation (where an external agent can ascertain that the system is in a particular software configuration). However, the TCG approach has been a considered a failure for end-user devices, as it does nothing to ensure that the “trusted” software is trustworthy and does not support upgrading it when it has found to be vulnerable.
The formally-verified seL4 microkernel presents an opportunity to make TPMs useful: seL4 is truly trustworthy, so attesting that it is running provides real assurance of trustworthiness. seL4 itself can then be used to instantiate a trusted software stack, and protect it from untrusted components, and it can be used to upgrade the trusted software securely.
This project is to build a demonstrator of an seL4-based, evolvable trustworthy system. This will require implementing TPM-facilitated secure boot of seL4 and some trusted base which can be remotely attested. If time allows, demonstrate secure software evolution.
Novelty and Contribution: Such an approach to a practical TPM-based trusted system has not been demonstrated, and will constitute publishable research.
- GHs102: Preempt or not preempt, that is the question
A widespread belief holds that an OS kernel for real-time use must be fully preemptible (whatever that means). While preemptability is a reasonably obvious requirement for monolithic kernels, it is also used for microkernels, such as the commercial Green Hills Integrity, QNX Neutrino and research systems such as Fiasco, a member of the L4 microkernel families. In contrast, most L4 microkernels, such as Pistachio, OKL4 and seL4 are non-preemptible. The claim is that if all kernel paths are kept short enough, then preemption adds performance overheads without significantly improving real-time behaviour.
This project is to quantify the performance/real-time tradeoff, and establish the criteria under which a non-preemptible kernel is a winner. This will require evaluating the hardware-dictated system-call, interrupt-handling and preemption overheads on several architectures, and establish limits on preemption-free system-call latencies and on that basis answer the question.
Novelty and Contribution: A comprehensive treatment of this issue will provide a significant, and publishable, contribution to the theory of OS design and implementation.
- GHs103: Design and build a gadget to win an iAward
The AIIA's iAwards have a category for tertiary student projects. They tend to be dominated by simple web and phone apps. Think of a cool embedded device, build it and win!
- GHs104: Design tradeoffs for real-time Java runtime on seL4
The Fiji real-time Java virtual machine (JVM) has recently been ported to seL4. However, that port, while fairly functional, is essentially a proof-of-concept. In particular, its implementation of threads is mostly a workaround for limitations in the then seL4 implementation rather than a principled approach.
With the seL4 scheduling issues fixed, threading for Fiji on seL4 should be reassessed. Specifically the question of whether Java threads should be mapped 1-1 on seL4 threads, or a user-level threads package is to be used. This project will implement both versions (which requires design and implementation of a native user-level threads package for seL4) and analyse their pros and cons with respect to functionality and performance. This may lead to publishable results.
The following summer projects are strongly related to the verification of seL4 and systems built on top of it. Details can be found on the L4.verified page. They are supervised by Gerwin Klein, June Andronick, Toby Murray, Matthias Daum, and various PhD students and research engineers.
- GK90: Automatic Information Flow Analyses for seL4-based Systems.
The seL4 microkernel provides a formally verified foundation for the construction of secure systems, and is designed to be deployed to enforce system-wide security policies. Information flow security policies describe the allowed information flows that may occur between a system's various components. The goal of this project is to produce a tool that automatically analyses an seL4-based system (described in capability distribution language capDL) to determine whether it satisfies a user-supplied information flow policy. This tool would automate the application of an information flow security theorem, which is currently being proved for seL4, and allow system designers and implementers to quickly check whether their systems adhere to desired information flow policies. A further extension would involve integrating this tool with the "Peek" seL4 visualisation tool, developed during a prior TOR summer studentship, to allow users to visually specify and examine information flow policies in the context of the systems to which they apply.
Novelty and Contribution: This work would produce the first automatic information flow checker for seL4-based systems, backed by a formal proof of information flow security that is currently underway.
Expected Outcomes: A prototype tool that takes as input a capDL system description, an information flow policy and a mapping of seL4 threads to information flow domains, and determines whether the system satisfies the policy.
- GK91: Testing vs Formal Verification, a Comparison.
seL4 is currently the world's only microkernel whose functionality has been formally verified down to the code level. Producing this high-assurance proof took an average of seven people four years. The purpose of this project is to compare the level of effort and level of assurance of this project with full coverage testing. The idea is to take a small part of the seL4 microkernel and write a testing framework with coverage analysis that achieves full coverage after selected criteria (e.g. branch coverage, code coverage, etc) either by generating test cases or by manually writing them. The question to be answered is: how many defects does this process discover for an early unverified version of the kernel? How much time needs to be spent to cover a small piece of code with tests. Apart from an empirical comparative result, the outcome of this project will also be useful for testing currently unverified architecture versions of seL4.
Novelty and Contribution: seL4 is one of the very few pieces of software in existence where the number of defects is known for different versions. The result of the project would be the first comparative study with real background data.
Expected Outcomes: A testing framework with coverage analysis for low-level C code and an application of it to the seL4 kernel. The project is well suited to be extended into a thesis project for automatic test case generation and further coverage criteria.
- GK92: A verified kernel with immune system.
seL4 is currently the world's only 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, it does not protect us against hardware faults. The goal of this topic is to extend the seL4 kernel and its specification to include self-health tests, potentially with error correction. The idea is to generate a list of expected hardware faults, to devise ways to detect these faults in the kernel and if possible to correct some of them. Examples are spurious hardware interrupts, memory bit flips, faulty memory regions, corrupt kernel boot image etc. Potential techniques are redundancy (duplication of important memory content), invariant and consistency checks, protection state checks, and checksums. These techniques will only work with a certain probability and often the only action that can be taken is to shut down the system safely. For safety- and security-critical systems this usually is vastly preferable to continuing running with corrupt data or code. The formal verification of seL4 has produced a substantial list of invariants that are known to be true about the system. Many of these can potentially be transformed into sophisticated consistency checks.
Novelty and Contribution: The relationship between formally verified software and fault-tolerance has not seen much research so far. This project is a first step to integrate both aspects.
Expected Outcomes: A set of self-health tests with formal specification for the seL4 microkernel.
- GK93: Covert timing channel analysis of seL4.
seL4 is currently the world's only microkernel whose functionality has been formally verified down to the code level. One remaining challenge is to understand the potential for covert channels in seL4, i.e. indirect paths by which unauthorized access can be gained to resources. This include both covert timing channels, such as those by which information is leaked by modulating the time required to complete given operations, and covert storage channels, which can arise when a publicly available output depends on confidential information. The aim of this project is to perform an initial analysis of potential covert timing channels in seL4, including an initial estimate of their throughput capacity. The results of this project are crucial for a security certification of seL4 at the highest levels of assurance.
Novelty and Contribution: This would be the first covert-channel analysis conducted of the seL4 microkernel.
Expected Outcomes: An initial list of potential covert timing channels in the seL4 microkernel. The project is well suited to be extended into a thesis project.
- GK94: Information Flow Security Proof for a Domain Scheduler.
The seL4 microkernel can be deployed as a separation kernel to enforce information flow security policies. In such a configuration, the kernel's usual scheduler is replaced by a so-called "domain scheduler" that ensures that scheduling decisions cannot leak information between system components, by always making such decisions independently of the state of all system components. This project would involve completing a formal proof of information flow security for such a scheduler. This proof will form an integral part of a larger first-of-its-kind proof of information flow security for seL4, which is currently underway.
Novelty and Contribution: This work would produce the first proof of information flow security for an seL4 domain scheduler.
Expected Outcomes: An information flow security proof for a domain scheduler for seL4, integrated into a larger proof of information flow security for the entire kernel.
- GK95: Beyond functional correctness: high-level test cases by proof.
seL4 is currently the world's only microkernel with a formal proof of functional correctness. This proof gives us very high assurance that seL4's code behaves as its specification says. Some bad-mouths would say that this only shows that the code has no more errors than the specification. This is true but (1) the specification is formal, precise and concise, which makes it easier to analyse and understand; and (2) the verification effort can now concentrate on showing desired properties about the specification: the correctness proof guarantees that the same properties hold for the kernel source code (for some kind of properties). Proof at the specification level are orders of magnitude easier than direct proofs on the implementation. The goal of this topic is to increase the level of confidence in seL4's specification by proving targeted properties, such as IPC (Inter Process Communication) properties. An example would be to show that each message sent by one component to another component using seL4's IPC mechanism eventually reaches the receiver. More generally, such proofs correspond to traditional high-level test cases, but uses a formal verification technique rather than testing.
Novelty and Contribution: seL4's functional correctness proof was a breakthrough and world's first, both in operating system and formal methods research. This work goes beyond this level of assurance, increasing the level of trustworthiness of seL4's specification.
Expected Outcomes: Proof for a set of properties about seL4's formal specification, starting with IPC properties.
- GK96: Automatic fact generalisation for Isabelle/HOL.
Interactive theorem provers, such as Isabelle/HOL, are systems in which user state hypotheses manually and then collaborate with the system to prove their validity, yielding new facts. Frequently the proof supplied is more general or more useful than the fact exported.
Theorem provers have recently been used on some very large projects, such as CompCert at INRIA and the L4.verified project at NICTA and UNSW. These projects typically build up very large libraries of known facts. Avoiding lost time by optimising these libraries for reuse is highly desirable. Facts may fail to be reusable in various ways. Some have unnecessary assumptions. Some have unnecessary restrictions on the form of certain variables, such as a proof of "f (a + b, 0) = g (, a + b)" when "a + b" could be replaced by any x. Some proofs of specific facts contain within them proofs of more general ones. Finally, the locale mechanism of Isabelle/HOL makes it easy to limit reusability of facts by proving them within a context which makes assumptions they do not require.
The aim of this project is to develop an automatic mechanism for locating and generalising facts within a proof library which are not as reusable as they ought to be.
Novelty and Contribution: An automatic tool for generalising facts within proof libraries would be of immediate benefit to a number of large scale projects using Isabelle/HOL, and insights into the approach could be of broader value in the field of automated reasoning.
Expected Outcomes: An automatic tool for generalising facts within proof libraries.
- GK97: Data Mining on the l4.verified Proofs.
The l4.verified project produced a formal, machine-checked proof showing that the C implementation of the seL4 microkernel complies with an abstract, formal specification. This proof of functional correctness comprises over 150.000 lines checked by the Isabelle theorem prover. Current research in NICTA's ERTOS group includes further kernel development as well as continued proof efforts, e.g. showing integrity and information flow properties about the kernel.
The aim of this TOR project is to extract data from the existing proof scripts that can aid further proof development as well as proof maintenance. Interesting data include usage counts for lemmas as well as a graph of lemma dependencies. The usage count could, for instance, be combined with the existing lemma-finder tool to show frequently used lemmas first. The dependency graph is mainly useful for proof maintenance.
Novelty and Contribution: The l4.verified project is one of very few large-scale verification projects. Data mining on such large proof scripts is a novelty. The still ongoing software development exposes unique challenges for proof maintenance, which can effectively be addressed with the help of data mining.
Expected Outcomes: The primary goal of this project is the extraction of lemma dependencies and lemma usage counts from the Isabelle theorem prover. The project could be extended to include visualization of the gained data in graphical form.