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.
Contents
- 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.
Linux Projects
These projects involve work on the Linux kernel or userspace. They will be supervised by Peter Chubb.
- PC91: Linux as a Boot Loader
Linux has a feature called `KEXEC' that allows a linux kernel to replace itself with another kernel. Therefore, it should be possible to use a small Linux instance as a boot loader, to boot over NFS or TFTP, without some of the problems that other boot loaders (e.g., U-boot) have. In fact this is done in a small way for the Sharp Zaurus Angstrom distribution. However, it would be really nice to be able to boot systems other than Linux. This project is to develop a root filesystem that in the first case can be used to boot another Linux instance on the BeagleBoard, and when successful, to be able to boot SeL4 plus other components as required.
more info
Device Driver Projects
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.
more info - 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.
more info
Componentisation Projects
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.
- IK70: Audio Framework for Embedded OS
Multimedia and audio devices are a popular class of embedded systems. As part of our research into modularised, microkernel-based operating systems for embedded devices, we wish to look at the design and implementation of an audio framework. This involves designing and developing a reusable software framework for audio applications and devices. The framework must be built using the component architecture we have developed for microkernel-based operating systems. Building a demonstrator showing the framework in use will also be part of the work.
more info - 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.
more info - IK81: Video phone
A great way to demonstrate the flaws of a componentised operating system is to run a multimedia application on it (which may explain why there are so few of them). Two-way video conferencing is a particularly good demonstration because it uses a large number of operating system components (such as an IP stack and video, camera, and network drivers) and requires careful co-ordination between the scheduler and all threads in the system to manage the large amount of data flow. This project aims to produce a video conferencing application on a componentised operating system. It will involve some implementation work and design and testing of a complete system.
more info
L4 and Embedded Systems Projects
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.
more info - KE92: Covert Channels - building infrastructure to steal secrets
Many operating systems are explicitly designed to keep secrets exactly that - secret. They actively seek to prevent data from leaking from one data clasification (e.g. top secret) to another lower clasification - even if the user actively attempts to violate system security. Your mission, should you choose to accept it, is to develop software to bypass system security to leak secrets using covert channels. The project would be fairly open for the student to survey communications techniques includling signal processing and error correction to develop tools capable of sending secret messages to a collaborator.
more info - KE93: Microkernel-based virtualisation.
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 application domain that is interesting for seL4 is secure virtualisation. SeL4 supports virtualisation via hardware features of Intel's VT-x enabled processors. Initial support for VT-x has been completed for seL4, which enables a simple Linux to run inside a simple virtual machine on seL4. The aim of this summer project is to investigate supporting a more featured virtual machine platform by using QEMU (a Linux-based virtual machine monitor) on seL4. By using QEMU, the intention is to re-use QEMU's existing emulation of a typical PC platform to provide a more complete virtualisation of a PC platform, and thus enable operating systems like windows to run unchanged on our virtual machine monitor.
Secure virtualisation is a serious issue for cloud computing. SeL4 might serve as a basis for secure cloud computing. This project will contribute to our understanding of how a formally correct microkernel like seL4 can support feature-rich virtualisation using hardware extensions, without adding significant complexity to microkernel itself.
Ideally, the outcome would be support for QEMU on seL4, which would then provides a reasonably complete virtual machine environment. A more modest goal is to develop an understanding how QEMU might be supported on seL4 via developing facets of an initial prototype.
- 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.
- KE97: Simple OS server on 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. SeL4 has some interesting features in its design that affect the structure of software built on top of it. This project is a challenge to build a very simple operating system server on seL4. The motivation for doing so it to understand the structure and simplicity of a minimal system built on seL4. We expect the simple system to have the basic functionality of processes, virtual memory, a network stack and file system. The project might use COMP9242 Advanced Operating Systems project as a base to start with.
SeL4 is formally verified to be correct, however such guarantees don't apply to systems build on the kernel - only the kernel itself is correct. To take a step towards formal verification of a complete software stack, this project aims to providing an practical understanding of a minimal system, which can then be used to plan further verification activities.
The expected outcome is a software prototype of a simple operating system server running on seL4.
- GHs91: OKL4/OK:Linux on Marvell SheevaPlug
Port OKL4 to the Marvell SheevaPlug. Get OK:Linux going, benchmark. Bonus points for comparing the performance of the v6 and v7 ISAs. - GHs95: Efficient concurrency control for high-performance microkernels
Concurrency control in OS kernels for multicore (CMP) or multithreaded (SMT) processors requires locking, which introduces complexity and overheads. Both can be minimised by either of two extreme approaches: a big kernel lock (single-threading the whole kernel) and multikernel (avoiding shared kernel data alltogether and using a message-passing approach).
This project evaluates both schemes in the context of a high-performance microkernel (featuring very short system calls) for present and near-future high-performance embedded hardware. The approach will use simulation, measurements and analytical models as appropriate to determine which approach presents the best tradeoff for a particular hardware platform.
Novelty and Contribution: Most OS kernels use more-or-less fine-grained locking, as a big lock is thought not to scale. However, unlike most kernels, L4 microkernels are designed for very short system calls, which make a big lock competitive for small to moderate numbers of processor. The multikernel approach is mostly attractive for high numbers of cores and high communication latencies, none apply to embedded processors.
No systematic evaluation of the tradeoffs has been made to date. Given that CMPs are becoming widespread in the embedded space, and the commercial success of the L4 microkernel, this study is topical and relevant. - GHs96: Global scheduling in virtualized systems via semantic patches
Virtual machines inherently introduce a hierarchical scheduling approach, where the hypervisor schedules VMs and guest OSes schedule processes. This approach does not meet the requirements of embedded systems, where a global view of priorities is required.
This project is to use semantic patches, as supported by the Coccinelle tool, to remove the scheduling decisions from a para-virtualized Linux guest and integrate them into a global scheduling policy. The virtualization platform used will be the OKL4 Microvisor.
Novelty and Contribution: Virtualization is getting increasing traction in embedded systems, but the hierarchical scheduling model limits applicability and leads to ugly hacks and workarounds. Semantic patches present a potentially clean approach to collapsing the scheduling hierarchy, without increasing engineering effort. This will open new application areas for virtualization in embedded systems.
more info - GHs97: Native Real-time Java on L4
Ovm is a real-time capable JVM for use in embedded systems. This project is to port Ovm to an L4 platform (seL4 or OKL4) to enable the use of Java components in safety- or security-critical environments. The performance and real-time properties of the port are to be evaluated.
Novelty and Contribution: Java, owing to its type safety, is an attractive language for programming critical systems. This usually requires real-time capability, which, in usable form, has only recently become available in JVMs, Ovm being one of them. To date, none has been ported to a secure microkernel that provides a small trusted computing base. The combination of real-time Java and L4 microkernel will provide new opportunities for trustworthy computing.
more info - GHs98: OKL4 microvisor as a systems platform
The OKL4 Microvisor is a new platform which combines the properties of a hypervisor and a microkernel. This project is to evaluate to which degree the Microvisor fulfills the functions of a classical microkernel, in that it should be able to support the construction of general systems with a minimal trusted computing base. Specifically evaluate its ability to support a microkernel-oriented component system, such as CAmkES, at overhead comparable to L4 microkernels.
Novelty and Contribution: The OKL4 Microvisor has already demonstrated its suitability as a hypervisor, with measured overheads for para-virtualized Linux far lower than for any other hypervisor where performance data is available. Demonstrating competitive performance in classical microkernel-based systems would prove that the Microvisor is truly the convergence point of hypervisors and microkernels, and settle the old hypervisor vs microkernels debate for good.
more info - GHs99: OS for a Dataflow Computer
NICTA is involved in a project to build a peta-scale computer based on the concept of a dataflow machine. This roject is to re-examine traditional OS functionality in the context of a totally different computing paradigm, and identify the core functions an OS for such a machine should have. It is furthermore to evaluate the existing hardware design for its ability to meet the requirements of the OS. A basic OS prototype is to be developed on a simulator for the architecture.
Novelty and Contribution: Peta-scale (million GFLOPS) computing is a strategic initiative of the US government, with significant funding attached. Present computing architectures will not scale to PFLOPS, hence the renewed interest in dataflow architectures. This ToR is part of a large project to build a peta-scale computer (details are under NDA). - 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 and a microkernel. 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.
more info
Static Analysis and Verification Projects
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, and various PhD students and research engineers.
- GK90: Automatic security analysis of complex systems
The L4.verified project has produced seL4, the world's first formally proven correct general-purpose microkernel. The next big step in this challenge of building truly trustworthy systems is to provide a framework to allowing secure systems to be constructed on top of seL4.
The goal of this project is to develop such a framework that takes a user's description of a system and generates a formal model of the resources required by each component of the system. The project will then look at automatically determining from the model how these components can interact, and automatically determining if the final system will always obey certain security properties, such as how information can flow between components (even under the assumption that each component's code is malicious).
An extension to this project would be to automatically generate formal proofs that these computations are correct, i.e. linking the formal model to the actual implementation. Together with the proof of seL4's correctness, this project will pave the way for proven secure systems that can be used in critical environments.
Novelty and Contribution: The project is the first important step in building fully trustworthy systems on top of seL4. A known, secure initial state of the system is the prerequisite for any security analysis of the overall system. The novelty of this project is to provide automate software-engineering support for a well-founded, formal security analysis of a large software system.
Expected Outcomes: The expected result is a program that takes a textual description of a system's security architecture, generates a formal security specification of the system and computes a new, simplier specification with fewer components. The program should then be able to perform a security analysis on this new specification to determine the access rights each component has to other components. - GK91: Formal Verification of Linux
The fully formal verification of Linux is slightly beyond the scope of a 3 month summer scholarship, but there is no reason why selected parts of the Linux kernel should not be amenable to formal verification in that time frame. The aim of this project is to apply C-level formal verification techniques to a small Linux function of your choice and to evaluate how well the method is applicable to a larger code base. You will be using a state-of-the-art C verification tool developed by the L4.verified project. The project will involve developing formal specifications and proofs of correctness in the interactive theorem prover Isabelle/HOL.
Novelty and Contribution: This work addresses the often neglected problem of verifying software written in system languages such as C. A successful outcome will provide useful experience in applied formal methods and increase the reliability of the Linux kernel.
Expected Outcomes: The expected result is a specification and if possible formal proof of a small component within Linux or of a set of important library functions. - GK92: Proving the absence of residual information in seL4
The purpose of this project is to extend the current formal proof of correctness of the seL4 microkernel to one crucial security property: the absence of residual information. In other words, the aim of this project is to formally prove, in the Isabelle/HOL theorem prover and using the formalisation of seL4 already developed, that no information remains in a resource when this resource is reallocated to another component. The results of this project are crucial for a security certification of seL4 at the highest level of assurance.
Novelty and Contribution: seL4 currently is the world's only microkernel whose functionality is formally verified down to the code level. This project is one of the first steps to extend this proof towards security properties.
Expected Outcomes: A formalisation of the property in Isabelle/HOL and substantial progress towards a formal proof of this property in seL4. The project is well suited to be extended into a thesis project. - 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 channel, 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: The Top 100 Theorems
Of the top 100 most famous and interesting mathematical theorems in the world, 83 have now been verified using various automated proof assistants, but only 75 using a single theorem prover. Will we be able to get the full 100? This summer project consists of picking a small number of the easier and smaller ones of these famous theorems and prove them in the interactive, industrial grade theorem prover Isabelle.
Although this is a fun project, it has the more serious background of driving interactive theorem proving technology and to make this technology more accessible to not-yet-experts. You will learn state of the art theorem proving technology that is also applied to program verification.
Skill Prerequisites: A good background in mathematics is required for this project.
Novelty and Contribution: The main contribution will be the formalisation in higher-order logic of a know mathematical theorem and its proof. Strict formalisation such as this requires creativity and ingenuity. Frequently the formalisation finds omissions or even small mistakes in published mathematical proofs.
Expected Outcomes: If successful, your work has an excellent chance of being published in either the Archive of Formal Proofs or the Isabelle theorem prover distribution directly. Only initial results are expected from the ToR project, with further work suitable for a thesis, and expected to lead to publishable results. - GK95: A Visualisation Environment for the seL4 microkernel
Capability-based operating systems, such as seL4, allow the construction of software and applications whose security and reliability are vastly superior to current commodity software. In such systems, the interactions between components are tightly controlled by the capabilities that each component possesses: one component can interact directly with another only if the first possesses a capability that refers to the second. Thus, writing secure software for capability-based systems requires the programmer to be constantly aware of which components have capabilities to each other, in order to reason about the security of a system (such as the permitted information flows between components). This project involves creating a visualisation environment for the seL4 microkernel that provides a 3D representation of the objects in a system and the connections and allowed accesses and information flows between those objects, via the capabilities that each object possesses, in order to aid the development of secure systems on top of seL4. The input to the tool would be a formal description of the objects and capabilities in a system, as well as for instance the possible information flows between them. If time permits, possible extensions to this initial functionality might involve visualising how a system changes over time, as its components interact and as new components are created; or implementing and experimenting with various filters to aid the visualisation of large systems, by which irrelevant details can be abstracted away from the user or multiple related objects aggregated together.
Novelty and Contribution: Writing capability-based software is a relatively unexplored frontier in software engineering. This project will enable this new frontier to be better navigated by experienced programmers, and to appear inviting to new programmers, by creating a necessary and powerful tool to aid in the development of secure capability-based software. To our knowledge, such a tool has never been created before for a publicly released capability system like seL4.
Expected Outcomes: A prototype visualisation environment that can be used by programmers when writing software for seL4, and that can be included in future releases of seL4 to aid its adoption as a foundation for secure systems development. - GK96: Port the Cambridge ARMv7 model to the L4.verified framework
Verification of systems code (such as the seL4 microkernel) relies on the accuracy and completeness of the underlying hardware model. To date, proofs on seL4 have been completed with respect to an abstract "C machine". The next step in the chain is to take the proofs right down to machine-code level. Promising work has been done both within our group and externally toward developing accurate, usable machine models, in particular a very complete ARMv7 model developed at Cambridge. The goal of the project is to integrate this model with our framework to improve our low-level reasoning capabilities.
Novelty and Contribution: This integrated model will provide the basis for the second stage of the L4.verified project.
Expected Outcomes: Either a port of the ARMv7 model to Isabelle/HOL or (preferably) a tool to automate its integration. - GK97: Formal stack depth analysis of C code
One of the most useful features of a high-level language (e.g. C) is that it provides a runtime stack for local variables and function call evaluation. Hidden (mostly) from the programmer is the fact that the stack lives in memory and has a finite size. For the most part this is a good abstraction and makes life much more pleasant. However, if we want to be certain that a program behaves as we expect, we need to show that the "stack invariants" are maintained: That the stack never aliases with heap-addressable memory and that it never overruns its allocation. This project is concerned with the second of these. To ensure these properties for the seL4 kernel (as part of the L4.verified project), we developed a tool to give a safe upper bound on stack usage of the kernel by analysing its machine code (and counting stack pushes and pops). This approach is sufficient to give a casual argument that the stack invariants are maintained but, in the spirit of the project, we want a rigorous proof of that fact, no shortcuts allowed! The goal of this project is to generate a formal proof of (an upper bound on) the stack usage of a C program in our verification environment, preferably generated automatically by a tool.
Novelty and Contribution: This tool would be a significant addition to our verification environment and would be important in the second phase of the L4.verified project.
Expected Outcomes: A tool to automatically generate a formal proof (in Isabelle/HOL) of an upper bound on the stack usage of a given C program.