Computer Laboratory

CTSRD

Part II, Part III, and ACS student project ideas


This page documents dissertation and research project ideas based on CTSRD-derived research for University of Cambridge Computer Laboratory students. There are, of course, many other interesting projects that might be done in related areas, and you should feel to talk to us about these as well. Please contact the listed potential supervisor, or Dr Robert Watson, for further information.

Capsicum: practical capabilities for UNIX

Capsicum is a hybrid capability-system model that merges historic ideas about capability-based security with contemporary UNIX operating systems. The Capsicum API is designed to support application compartmentalization, allowing user processes to execute in capability mode, unable to access global namespaces, with added APIs for capability-like features such as capabilities based on file descriptors, process descriptors, and a service model based on the Casper daemon. Developed in collaboration between the University of Cambridge and Google, ongoing Capsicum work is being funded by Google, DARPA, and the FreeBSD Foundation; Capsicum is available out-of-the-box in FreeBSD, and Google has developed patches for the Linux kernel.

Extending Capsicum and exploring how applications can use its features remains an active area of work, with many potential Part-II development or Part-III/ACS research projects.

  • Capsicum Software TPM and Crypto Service Module

    Compartmentalized application components frequently require access to cryptographic services such as key management and TLS. However, this components often should not be granted direct network access, or even use of keying material to build TLS connections. Simultaneously, cryptographic code itself proves highly vulnerable, and should be sandboxed away from other sensitive application components. This project would develop a "software TPM"-like cryptographic module for Capsicum, intended to offer cryptographic services to sandboxed components while itself executing in one (or perhaps many) sandboxes. Services would include key storage, indirect use of keys (e.g., the ability to encrypt with a key while not having access to the key), and higher-level protocols such as TLS (e.g., the ability to communicate over TLS without having either socket access, or access to keying material used to authenticate the connection). Potential evaluation criteria would include security improvements and performance impact, with key questions including how to maximise security improvement while minimising overhead and code change.

    Prerequisites: Strong C programming experience, UNIX programming; Part-II security or Part-III/ACS R209 recommended.

    Potential supervisors: Robert Watson, Khilan Gudka

  • Capsicum Support in GNUstep

    GNUstep is an implementation of the APIs from the OpenStep specification and later from Apple's Cocoa. This project will involve modifying the framework to make use of Capsicum, a simple set of capability APIs for FreeBSD. There are several steps:

    • Modify NSWorkspace to read a plist describing required services from an application or tool's property list and ensure that they have access to them, then call cap_enter before spawning. This part requires rtld to support sandboxed-on-launch code. If this support is not finished, then a first approximation can be achieved by calling cap_enter() from NSApplicationMain().
    • Implement a file chooser service that will pass file and directory descriptors to applications that try to use the standard open / save dialogs.
    • Ensure that the distributed notification centre and pasteboard server connections are open before entering the sandbox.

    At this stage, applications should be useable with capsicum with some small modifications. There are several additional small changes that could make the porting easier:

    • Modify NSFileWrapper to use openat() and friends.
    • Create an NSString subclass that carries a file descriptor for a base path as an instance variable and allows all of the standard path modification operations to work relative to this.
    • Maintain a dictionary mapping paths to directory descriptors, so that attempts to open a file with NSFileHandle or NSFileWrapper will use openat() via this mechanism.

    Evaluation should include some example applications running in sandboxes, a comparison with the MAC-based sandboxing on OS X, and ideally an example of using Distributed Objects to implement privilege separation in an existing application.

    Prerequisites: Knowledge of Objective-C, UNIX programming.

    Potential supervisor: David Chisnall

TESLA: Temporally Enhanced System Logic Assertions

  • TESLA realtime and probability distributions

    Temporally Enhanced Security Logic Assertions (TESLA) introduce C-language extensions for inline temporal assertions and automata validation, which in turn drive compiler-generated runtime instrumentation and validation of temporal effects. However, strict sequence-based properties are not the only type of temporal properties that may be of interest: we are also interested in realtime effects, such as validating assertions of realtime behaviour in protocols, and distribution effects over time, in which sampled values take on desired properties (e.g., randomness and monotonicity). This project would extend the TESLA framework to allow these properties to be declared and continuously validated during program execution.

    This project will investigate possible extensions to TESLA improving its performance and functionality:

    • Adopting new static-analysis techniques that allow: (a) optimising out local checks where it can be determined that they would always pass; (b) improving run-time instrumentation performance by lifting checks out of loops (etc); and (c) providing compile-time failures for locally validatable properties, rather than requiring runtime testing.
    • Investigating 'distribution assertions' in which tracked data-structure fields are checked temporal properties other than explicit automata -- e.g., probability distributions, mean/media/stddev, monotonic increase/ decrease, likely/unlikely, etc.
    • More complex instremented invariant structures, such as providing side-effect-free (functional?) code snippets that, at various events, validate those properties without requiring manual instrumentation; for example, the correctness of cached values that would otherwise require walking large data structures such as trees or linked lists.
    • Other interesting applications of TESLA's instrumentation and analysis approaches.

    Potential evaluation criteria might involve usefulness (by qualitative metrics), false positives/negatives, and compile-time and run-time performance impact.

    Prerequisites: strong working knowledge of the C programming language, and an interest in both compilers and low-level system software, such as operating system kernels and network daemons.

    Potential supervisor: Robert Watson

BERI: Bluespec Extensible RISC Implementation

BERI is the Bluespec Extensible RISC Implementation, a prototype hardware-software research platform consisting of a RISC processor and peripherals synthesisable to FPGA, the FreeBSD operating system, Clang/LLVM compiler suite, and a large number of open-source applications. We have not drawn out specific project ideas for BERI, but there are many interesting things to do here, including support for additional devices, characterisation of the realism of the FPGA-based implementation as compared to fabricated processor designs, etc. Please contact Robert Watson if you are interested in a potential project in this area.

CHERI: Capability Hardware Enhanced RISC Instructions

CHERI (Capability Hardware Enhanced RISC Instructions) is a novel CPU architecture implementing a hybrid capability model: in-address-space memory protection and fine-grained compartmentalization. The CTSRD project has prototyped the CPU on FGPA, and adapted the FreeBSD operating system and Clang/LLVM to run on the platform, as well as a broad array of open-source applications. The platform is now suitable for a variety of Part-II, Part-III, and ACS operating-system, compiler, and software research and development projectsinvestigating software security, language security, program analysis and transformation, processor sucurity, and the hardware-software interface. Potential supervisors exist in all of these areas; please contact us to be pointed in the direction of a suitable supervisor for your interests.

  • Operating-System Support for Tagged Architectures

    CHERI is a "tagged architecture" meaning that each word or line of memory has additional, unaddressable, metadata associated with it. The CHERI model relies on a 1-bit tag indicating whether a 32-byte line is a capability or ordinary data. Other tagged models associate information-flow labels, pointer metadata, taint tracking, or other properties with words or lines. These novel techniques are being written about heavily in the hardware-software research community, but their implications for operating-system design are as-yet unclear: contemporary OSes depend on simpler models of memory, in which all words are addressable and interchangeable (e.g., allowing virtual memory to be paged to a swap partition or file in the filesystem, which may not have obvious places to store tags). This project will explore how contemporary OS designs respond to the introduction of tags. Development tasks might include extending the process model, debugging interfaces, virtual-memory subsystem, filesystems, etc, to better support tags in a generalisable way, although with a focus on CHERI as a useful case study. Evaluation criteria might include the functional implications, complexity of changes, and performance impact.

    Prerequisites: Strong experience programming in C, the UNIX environment; Part-II security or Part-III/ACS R209 recommended.

    Potential supervisor: Robert Watson

SOAAP: Security-Oriented Analysis of Application Programs

SOAAP is the Security-Oriented Analysis of Application Programs. Sandboxing technologies such as Capsicum and CHERI support the fine-grained compartmentalisation of large-scale applications such as web browsers and office suites, as well as multiple-component software such as the UNIX userspace. When deployed correctly, application compartmentalisation offers significant benefits by allowing policies to be imposed within applications, and in mitigating exploited vulnerabilities. However, application compartmentalisation remains an art rather than a science: identifying, implementing, and debugging partitioning strategies requires detailed expertise in both the application and security. SOAAP is exploring semi-automated techniques, grounded in static analysis, dynamic analysis, and automated program transformation, to improve the developer experience. We have an LLVM-based prototype that models Capsicum security, now being applied to applications such as the Chromium web browser.

We have not drawn out specific project ideas for SOAAP, but there are many interesting things to do here, including developing new analysis techniques, automated program techniques, evaluating effectiveness, etc. Please contact Robert Watson if you are interested in a potential project in this area.