SSRG Summer Projects

These projects are available to holders of the NICTA Summer Research Scholarships. We may also provide some additional scholarships for good students who miss out in the official process. Talk to us if you are interested.

Background information


Projects marked NEW are not on the official list but are available nevertheless.

Componentisation Projects

These projects deal with the building of componentised operating systems on top of seL4, and CAmkES the component architecture that supports this. They are supervised by Ihor Kuz and various PhD students.

  • IK120: Desktop environment for seL4
    At SSRG we have developed seL4, a secure, formally verified microkernel. We have also developed many different OS components such as a file system, network stack, etc. Yet we all still use other operating systems to do our everyday work. The aim of this project is to develop the beginnings of a desktop environment based on seL4. It will involve using existing components, developing new ones, and combining all of these to create a usable system.
    Novelty and Contribution: This project will take the world's first formally verified operating system kernel, and make a usable system out of it, making it that much more available to the masses.
    Expected Outcomes: An seL4-based system that can be used to do basic desktop computing functions like create and edit files, and maybe even more advanced functions such as running slideshow presentations, compiling programs, or web surfing.
    Contact: Matthew Fernandez

  • IK121: Gaming on seL4
    At SSRG we have developed seL4, a secure, formally verified microkernel. That's cool, but what use is it if you can't play games on it? The aim of this project is to port or develop a game to run on an seL4-based system, and show that it really is a world-class operating system. The project will not only involve the porting or writing of the game code, but more significantly, it will involve the development of the supporting infrastructure that the game will require to run.
    Novelty and Contribution: While games are fun, getting a game to run requires many significant operating system services. Putting this together will therefore result in a significant boost in the OS services running and available for seL4, and will also provide a good platform to evaluate seL4 and its performance.
    Expected Outcomes: A playable game running on seL4, and an evaluation of that game's performance.
    Contact: Ihor Kuz

  • IK122: Extended file system functionality
    Implementing or extending a file system has generally been a high overhead task, requiring intimate knowledge and modification of kernel code. However, with the advent of user-level file systems (e.g. FUSE) the barrier to adding features to file systems has been significantly lowered. The aim of this project is to investigate the FUSE model and develop interesting file system extensions such as, tagged file system (replace the hierarchical file system structure with a tag-cloud based structure), typed file system (associate types with file systems and limit operations on files based on their type), variable granularity file system (treat directories as files, or treat archives (like zip files) as directories, hash-caching file system (maintain hash values of all files and allow fast access to them), etc.
    Novelty and Contribution: This project provides insight into various ideas regarding extensions of file system functionality and structure. There is more to it, however. We also wish to apply many of these ideas to our componentised file system design in seL4-based systems. Being able to implement and try them out in conventional operating systems will be a great benefit.
    Expected Outcomes: The outcome of this project will be design and implementations of various file system extensions, and evaluation of their usefulness and performance.
    Contact: Mark Staples

  • IK123: Secure Quadcopter (and Robot)
    Quadcopters are becoming popular as unmanned aerial vehicles (UAV) and toys. We have several small quadcopters that we want to use to demonstrate the capabilities of our seL4 secure microkernel. Your project, should you choose it, is to develop a scenario involving quadcopters, and possibly Lego robots, that are run by our microkernel and demonstrates its security properties. This project will involve creativity, coding, and playing.
    Novelty and Contribution: 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.
    Expected Outcomes: The result of this project will be a flashy demo that shows off the capabilities of the seL4 microkernel and systems based on it.
    Contact: Ihor Kuz

  • IK52: Web Server for L4-based Devices
    Any computer system worth its salt must be able to run a web server these days. At SSRG 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 web server will also be used to run parts of the SSRG 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.
    Contact: Ihor Kuz

  • IK80: Linux as a Component
    The SSRG 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 SSRG, making both more useful and available 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.
    Contact: Ihor Kuz

  • IK111: Hardware Devices as Operating System Components
    At SSRG 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.
    Contact: Ihor Kuz

  • 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.
    Contact: Ihor Kuz

Microkernel (seL4-based) 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
  • 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.
  • 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.
  • GH105: Flight computer for QB50 satellite NEW
    UNSW has made a successful bid for participation in the EU QB50 project, to build a QubeSat satellite for a launch in 2015.
    This project is to design and implement a ciruit board for a flight computer, and build an seL4-based faut-tolerant operating system on top, able to support critical attitude-control software running side-by-side with less critical DVB-S2 encoding of data for transmission to the ground.
    This is a project for two students, one designing and building the hardware, and the other designing and implementing the OS. The first student must have experience in PCB design, the second one solid knowledge in OS internals (having done COMP9242 is strongly recommended).
    Novelty and Contribution: This will be the first ARM-based flight computer, and (to our knowledge) the first multi-criticality system in space. It will also be the first Australian-designed and -built OS in space.
  • GH106: Port Google Go to seL4 NEW
    Google Go is a small but managed programming language. It is type- and memory-safe, has a syntax based on C but is aims to support concurrent programming and as such has constructs similar to Ada.
    These features make it suitable for programming high-assurance systems, particularly in combination with a high-assurance operating system and run-time environment.
    This opportunity exists with the formally-verified seL4 microkernel, which provides a rock-solid foundation for software, Porting Go, particularly its lightweight “native” run-time, to seL4 is the first step towards making this a reality. It may enable verification of the small run-time, and thus provide a programming environment of unprecedented dependability.
    Novelty and Contribution: This will be the first type- and memory-safe programming environment on a verified OS kernel, and provides the potential to verify the whole RTE at some later time.
  • GH107: Preventing cache-based covert channels without flushing NEW
    Caches, like other shared hardware, present a potentially high-bandwidth covert timing channel. The normal approach to preventing this channel is to flush all caches on every context switch. With the huge caches available in modern computer systems, this mitigation strategy has a disastrous performance impact.
    This project is to explore an alternative approach to flushing, namely preventing sharing of the cache. This is made possible by a unique aspect of the design of seL4, which separates kernel data similarly to user data, and has almost not shared kernel data structures (a covert channel analysis of those shared kernel data structures is subject to a different project).
    Specifically, page colouring can be used to partition the L2 cache between two security compartments so that they never use the same cache line. Cache pinning can be used to achieve the same for the L1 D-cache, both are straightforward. Sharing of I-cache lines can be prevented by replicating the kernel code, so that each partition executes its own copy of kernel instructions, and using cache pinning to keep them separate. This part requires careful design to get right (e.g. how do you boot?)
    Novelty and Contribution: A novel, low-overhead scheme to prevent cache-based covert channels.
  • GH108: Virtualized Windows on seL4 NEW
    seL4 is routinely used as a hypervisor to run Linux. Its use could be more widespread if it supported running unmodified Windows binaries. However, Windows shows its DOS heritage in its boot process, starting off in 16-bit mode. Most hypervisors supporting Windows therefore contain a big and ugly x86 emulator, which dramatically bloats the trusted computing base.
    The aim of this project is to virtualise Windows without emulation of legacy hardware modes. This can be achieved by booting a Windows system on hardware and taking a dump. On the seL4 system, the virtual-machine monitor then initialises the hardware to get it into the state expected by the a just-booted Windows system. At this stage it should be possible to undump the Windows system and get it running with minimal emulation code in the hypervisor.
    Novelty and Contribution: First full virtualization of an unmodified Windows binary without emulating legacy hardware modes. If done well, this should be easily publishable.

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, Toby Murray, and various PhD students and research engineers.

  • GK120: Case study of proving a million lines of code system.
    Providing strong security or safety guarantees for software systems in the order of million lines of code is one on the grand challenge of the Trustworthy Systems project. We are building a framework that will enable to minimise the amount of formal verification needed while still providing whole-system assurance. The approach taken is to architect the system as a set of components, with a minimum number of trusted components, that are kept isolated from the untrusted ones. We use the seL4 microkernel as a trustworthy foundation providing isolation between components. Our framework builds on the existing formal proof that seL4 is functionally correct and enforces integrity of user information. It will also rely on our ongoing proof of confidentiality enforcement.
    The goal of this project is to use this framework on a specific case study built of seL4. The framework aims at taking care of composing all the various proofs about the different parts of the system and only require verification of the parts specific to the case study. The project would involve identifying and formalising the targeted property for the case study and perform the verification of some of the proof obligations required by the framework. Some larger proof obligations, such as the correctness of some trusted components, might be assumed.
    Novelty and Contribution: Formal code-level proof of very large systems is largely considered infeasible. This work will contribute to demonstrate that, with the right foundation, approach and frameworks, this grand challenge can be achieved.
    Expected Outcomes: Formal verification of a seL4-base case study system, using the framework to provide whole-system assurance, possibly assuming some of the proof obligations.
    Contact: June Andronick
  • GK121: Automatically Refactoring Machine-checked Proofs.
    The seL4 microkernel verification is one of the very few large-scale proofs that exist in the world today. As such, our team is facing problems for which solutions and tools do not yet exist.
    In particular, the movement of proofs between files becomes both more important, for organising work and sharing results, and more difficult, because simply cutting-and-pasting may invoke time-consuming proof 'recompilation' and may well also break existing proofs.
    We had some success with a previous implementation in the Standard ML functional programming language, and this work has since been extended in Scala. Our work is informed by formal approaches to the problem, but our approach is manifestly pragmatic.
    This project involves adapting the best parts of both existing tools, and examining the feasibility of some new ideas for manipulating proofs to make the use of supporting lemmas more explicit---an important step for ensuring that moving one proof does not break another. It is not about directly verifying software, but rather about manipulating the proofs themselves.
    You would have the opportunity to learn the basic principles of automatic theorem proving, examine the source code of sophisticated symbol manipulation software (Isabelle), and develop a prototype tool. Your tool would be evaluated against the seL4 proof, giving you the insights necessary to propose innovative new mechanisms and techniques. You would work in a focused and large team just across the road from the UNSW campus at Kensington, benefit from the guidance and knowledge of experienced researchers and engineers, and enjoy the company of other interns and students over summer.
    Your work would have a direct impact on the daily activities of every member of the team, and also the potential to improve other verification projects internationally.
    Novelty and Contribution: It is only recently that proofs and the teams working on them have become so large that automatic refactoring is all but a necessity. NICTA researchers and their collaborators were among the first to develop such techniques and tools, but more work is needed before large proofs can be manipulated reliably and automatically on a daily basis. The seL4 proof presents a unique opportunity for evaluating and improving refactoring methods.
    Expected Outcomes: A prototype tool for automatically manipulating large proof texts and its evaluation against the seL4 proof text.
    Contact: Timothy Bourke
  • GK122: Rely-Guarantee formalisation usable for C programs.
    Formally reasoning about concurrent programs is a hard problem. Rely-Guarantee reasoning is well-known method for compositional verification of shared-variable concurrent programs. However, there is still a lack of formalisation of such framework for common programming languages. There exists an early formalisation, in the Isabelle/HOL theorem prover, of Rely-Guarantee reasoning, but no support for reasoning about the C programming language, still the most widely used language for developing software with high performance and precise memory requirements.
    The goal of this project is to implement the formalisation of Rely-Guarantee on SIMPL. SIMPL is a generic imperative language, embedded in Isabelle/HOL, and which was used as intermediate formal representation of the C implementation of the seL4 microkernel in the L4.verified project. L4.verified successfully produced a formal proof of functional correctness of seL4. It is now used as a trustworthy foundation to build larger systems composed of various components. Formal verification of these larger system thus involves reasoning about the interleaved execution of the components. This summer project entails formalising parallel composition of programs in the SIMPL language and extending the corresponding Hoare Logic.
    Novelty and Contribution: This project would produce the first formalisation of Rely-Guarantee to reason about C programs. This will contribute significantly to the formal verification of componentised systems.
    Expected Outcomes: Formalisation of Rely-Guarantee on the SIMPL language.
    Contact: Gerwin Klein
  • GK123: Mapping system architectures into a formal logic.
    Developing a system that can be formally verified to be secure is a long and expensive process. It begins by designing a system architecture, and ends by implementing that architecture and then verifying that implementation. It's important to get the architecture right at the start, otherwise the costs of implementing and verifying it only to find out that it's wrong can be very high. In order to avoid such costly mistakes we are developing a process and tools to analyse the security properties of software architectures before they are implemented. This analysis should be done in such a way that it can contribute to the formal verification of the system at a later stage. As a step towards this goal, the aim of this project is to develop a mapping of a system architecture description to the Isabelle/HOL theorem prover logic so that we can reason and prove properties about it.
    Novelty and Contribution: This project would bridge the gap between abstract description of systems architectures and expressive specification of the system, as well as the gap between automatic, high-level analysis and powerful logic to reason about function correctness down to the C code.
    Expected Outcomes: A mapping from architecture descriptions to Isabelle/HOL and investigation in reuse of analysis results for proofs in the theorem prover.
    Contact: Matthew Fernandez
  • GK124: Noninterference Security for Real-World Systems.
    This project involves extending traditional definitions of noninterference security to systems that contain trusted components, whose behaviour is relied upon in order to enforce security. Noninterference is a security property that is satisfied by a system when its low-classification components can learn nothing about its high-classification inputs, state and actions. Traditional models and noninterference definitions assume that all components within the system are potentially malicious and act arbitrarily, and so are ill-suited to real-world systems that contain trusted components that are relied on not to act improperly. These kinds of systems are becoming more common as high-security systems become more mainstream, and include systems that change their security configurations at runtime, in response to user actions. These systems rely on trusted components to accurately carry out the user's requests, and remain secure only when their trusted components behave as expected. Reasoning about noninterference in such systems requires a noninterference model that takes into account the actual behaviour of these trusted components.
    Novelty and Contribution: This work would produce the first framework for reasoning about noninterference security for systems with trusted components, and have direct contribution to the ongoing work to prove noninterference security for seL4-based systems.
    Expected Outcomes: A formal definition in Isabelle/HOL, and proof framework, for noninterference security for systems with trusted components, based on the existing noninterference framework for seL4.
    Contact: Toby Murray
  • GK125: Formal semantics for the Google GO language.
    The Go programming language is a new programming language from Google designed to be a better alternative for systems programming than C. Motivation include a fast compiler, a light-weight type-system, garbage collection and concurrency via "go-routines". The l4.verified project at NICTA achieved the world's first verification of a realistic micro-kernel (seL4). But there is still lots to do. In particular, we want to be able to build large systems on top of seL4, and to derive formal guarantees about those systems' behaviours. Though seL4 itself is written in C, there's no a priori reason why the systems above it should be. Indeed, maybe those systems could be written in Go. If this vision is to be achieved, there are a number of things that need to be done first. One of them is that, in order to do any sort of logical reasoning about programs, we need to understand what programs mean. This project will aim at defining a rigorous mathematical definition of (a subset of) Go's semantics. Writing a semantics is a bit like writing a compiler or interpreter in logic, and we would do this in a theorem-proving system (Isabelle or HOL4) to help us check that the details were right.
    Novelty and Contribution: This project would produce the first formal semantics of the Google Go language, with promising impact for efficient development and verification of large systems.
    Expected Outcomes: Formal definition of (a subset of) the semantics of each operation of the Go language.
    Contact: Gerwin Klein
  • GK126: 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.
    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.
    Contact: Toby Murray
  • GK127: 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.
    Contact: Gerwin Klein
  • GK128: 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.
    Contact: Gerwin Klein
  • GK129: 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. These 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.
    Contact: Toby Murray
  • GK1210: 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.
    Contact: Thomas Sewell
  • GK1211: SMT Solvers for C/C++ Analysis.
    SMT solvers are automated decision procedures for decidable theories. In the recent past the have become popular in many application areas including automated program verification. The goal of this summer project is to investigate their use in automated C/C++ code analysis to detect software bugs such as buffer overflows or divisions by zero.
    This project will require some programming experience as well as a strong interest in logic and program verification. It can later expanded into a thesis.
    This student project is in the context of the Goanna software analysis tool as developed by the NICTA Software Systems Research Group (SSRG). Goanna is an automated source code analyzer for C/C++ available both for academic and commercial use. You will be working directly with a team of international researchers and engineers and be given the chance to fuel a real software product with your contribution.
    Novelty and Contribution: This will be the first application of SMT solvers for verification purposes in the Goanna tool.
    Expected Outcomes: By the end of the internship it is expected that the candidate has a good understanding of SMT solvers, is able to generate models by himself and has successfully used an SMT solver to automatically show the correctness of example code.
    Contact: Ralf Huuck
  • GK1212: Security Checking of Chromium.
    Software security is a critical topic for many companies and research groups. Especially, with the rapid development of code bases and new multi-core features, security becomes a bottleneck in software development. Automated security analysis techniques are a must to reduce the burden on the software developer.
    This project is about developing new security checks for emerging problems in C/C++ source code. Part of the research is to extend the Goanna static analyzer with these checks and evaluated the quality on large open source projects such as Google's Chromium. Further test beds will be provide through the NIST SAMATE program and give the student a chance to compare his solutions to the best in the world.
    This student project is in the context of the Goanna software analysis tool as developed by the NICTA Software Systems Research Group (SSRG). Goanna is an automated source code analyzer for C/C++ available both for academic and commercial use. You will be working directly with a team of international researchers and engineers and be given the chance to fuel a real software product with your contribution.
    Novelty and Contribution: This project delivers new security checkers for the automated analysis of C/C++ programs. It also creates to opportunity to find previously unknown security bugs in well-known software.
    Expected Outcomes: By the end of the summer scholarship the student is expected to have developed their own new security checkers within the Goanna framework, has applied them to real large scale software and compared the results with the state of the art tools available. There also might be an opportunity to feedback the results to NIST.
    Contact: Ralf Huuck
  • GK1213: Advancing Software Engineering through Quality Metrics.
    Large scale software projects are difficult to manage. They can involve huge amounts of code and frequent changes, making it difficult to track their quality and to identify the most urgent "hot spots". Software metrics are one option to quickly identify those hot spots and give an overall quality estimation.
    This project is about designing and developing source code metrics for large scale C/C++ source code. There are two parts to it: Static metric of an existing snapshot of a project and dynamic metrics reflecting a project's evolution over time.
    Part of the research is to design and implement relevant metrics on top of out source code analyzer Goanna. Moreover, they software metrics should be evaluated against real life projects from their source code repository. The student will be required to investigate suitable metrics, do some implementation work and present an evaluation based on her/his findings.
    This student project is in the context of the Goanna software analysis tool as developed by the NICTA Software Systems Research Group (SSRG). Goanna is an automated source code analyzer for C/C++ available both for academic and commercial use. You will be working directly with a team of international researchers and engineers and be given the chance to fuel a real software product with your contribution.
    Novelty and Contribution: This project delivers advanced software metrics over the lifetime of a C/C++ project. It also creates to opportunity to establish some core insights for the software engineering community.
    Expected Outcomes: By the end of the summer scholarship the student is expected to have developed a number of software within the Goanna framework, has applied them to real large scale software and evaluated the results. Moreover, he will learn about valuable new research and technologies in the software development life cycle.
    Contact: Ralf Huuck

Served by Apache on Linux on seL4