These projects are suggestions, and can be scaled up or down for the level and length of the project, and can also serve as inspiration. I also include some completed projects at the end that can serve as inspiration for new projects.
CHERI is a research project to develop practical capabilities machines, in which instead of using integers as indices into memory, memory accesses work with capabilities, which are unforgeable tokens of authority. Capabilities make it possible to mitigate many of the memory safety problems that plague mainstream computer systems. However, their use to ensure security requires high assurance. The Cerise project at AU has developed techniques to establish rich security properties for capability architectures. Many projects can be based around capability machines, either on the theory side, or on the practical side using the Morello development board, and I give a few examples below.
CHERI https://www.cl.cam.ac.uk/research/security/ctsrd/cheri/ CHERIoT https://cheriot.org/ Morello https://www.arm.com/architecture/cpu/morello
The Morello development board is an experimental capability machine based on the Arm architecture. The goal of this project is to develop test programs that demonstrate the expressiveness of capability machines.
Morello https://www.arm.com/architecture/cpu/morello
The capabilities of CHERI have authority over a contiguous range of memory addresses. This works well for buffer-manipulating programs, but not for programs that have richer access patterns, like those used in matrix manipulations, in particular for Machine Learning. The goal of this project is to extend CHERI capabilities to have authority over different slices of arrays: a row (contiguous arrays), a column (non-contiguous, which requires knowing the width of the matrix), of a sub-matrix (which also requires the width), and to use it to debug ML programs, and (more ambitious) to prove safety.
Sail is a domain-specific language for describing instruction set architectures precisely, making it possible to check conformance, generate tests, verify implementations, investigate ISA-level properties, etc.
Many projects can be based around Sail, and I give a few examples below.
The Motorola 68000 is a CISC computer architecture introduced in 1979 whose successful design has allowed to remain in use, more than 45 years after its inception. The goal of this project would be to write a definition of the 68k ISA in the Sail language, and to test it on programs.
Sail https://github.com/rems-project/sail
(co-advisor Aslan Askarov)
The definition of a modern instruction set architecture (ISA) like Arm or RISCV covers thousands of instructions, and the definition of one instruction can be hundreds of lines of code in a domain-specific language like Sail. The size of these definitions means that they are likely to contain errors. One particularly important property of an ISA definition is the integrity of exception levels (aka “protection rings” or “domains”): a userland program should not be able to affect operating systems private registers, and an operating system should not be able to affect hypervisor private registers. The goal of this project is to explore how to design a type system to identify violations of exception level integrity, and to explore how to implement a typechecker so that it scales to mainstream ISAs.
Sail https://github.com/rems-project/sail
Language-Based Information-Flow Security, Sabelfeld and Myers https://www.cs.cornell.edu/andru/papers/jsac/sm-jsac03.pdf
The definition of a single instruction in a modern instruction set architecture (ISA) can span hundred or event thousands of lines of domain-specific ISA description language. This makes those definitions difficult to access, even for experts. The goal of this project is to develop a practical source-to-source symbolic evaluator for Sail, that takes a Sail program and a set of constraints, and simplifies the Sail code based on the constraints. For example, a constraint can specify that the code is running at a given privilege level, and the symbolic evaluation will cut out the parts of the code that correspond to other privilege levels.
Sail https://github.com/rems-project/sail
(co-advisor Ben Simner)
Inter-process interrupts (IPIs) make it possible for one core to change the execution flow of another core, which is used by synchronisation mechanisms like Linux’s Read-Copy-Update (RCU). IPIs propagate separately from memory accesses, which raises the question of how IPIs and normal memory accesses interact. The goal of this project is to develop a test harness to exercise small programs using IPIs.
https://github.com/rems-project/system-litmus-harness
Axiomatic relaxed memory models provide succinct characterisations of the concurrent behaviour of (for example) hardware architectures. Different models can be used to characterise different feature sets, for example Arm-A with virtual memory enabled and Arm-A with virtual memory disabled. We expect that these models should have certain relationships: for example, if one does not use virtual memory, then it should not matter whether it’s turned on (under certain configurations) or off. The goal of his project would be to formally establish some of these relationships.
(co-advisor Ben Simner) Validation of relaxed memory model relies on a combination of confirming architectural intent via discussions with architects, and of hardware testing. Testing involves pointed litmus tests which capture important programming patterns, and systematic testing by generating programs that exercise combination of synchronisation edges of axiomatic model, as done using the DIY tool. Such systematic testing has proven invaluable in the past, but the tooling has fallen behind the development of new models (for example for instruction fetching, virtual memory, and exceptions) involving new types of edges. The goal of this project is to develop a systematic litmus test generator that supports modern memory models.
Computer security relies on systems code to correctly manage the underlying hardware, especially the virtual memory mechanisms used to enforce controlled isolation between processes and virtual machines. This requires delicate synchronisation around page table accesses, to handle the subtle relaxed concurrency phenomena of virtual memory. These were not supported by conventional testing, semantics, or verification methods, so systems programmers have had to rely almost entirely on code review by domain experts - until recent work. We now can, for disciplined code, give a relatively simple model of the safe manipulation of page tables. The goal of this project is to develop a program logic that captures this discipline of programming and uses it to expose simple abstractions to the user.
Knowledge of separation logic is required.
Very relaxed concurrency memory models, like those of the Arm-A, RISC-V, and IBM Power hardware architectures, underpin much of computing but break a fundamental intuition about programs, namely that syntactic program order and the reads-from relation always both induce order in the execution. Instead, out-of-order execution is allowed except where prevented by certain pairwise dependencies, barriers, or other synchronisation. This means that there is no notion of the ‘current’ state of the program, making it challenging to design (and prove sound) syntax-directed, modular reasoning methods like Hoare logics, as usable resources cannot implicitly flow from one program point to the next. AxSL is a separation logic for the relaxed memory model of Arm-A that captures the fine-grained reasoning underpinning the low-overhead synchronisation mechanisms used by high-performance systems code. In particular, AxSL allows transferring arbitrary resources using relaxed reads and writes when they induce inter-thread ordering.
The goal of this project would be to rebase AxSL on another memory model, for example TSO, RISC-V, or on a reformulation of the Arm memory models that makes stronger or different reasoning principles available, and expose these reasoning principles.
The behaviour of concurrent programs on modern hardware architecture is typically expressed using a predicate that indicates whether a given execution (induced by the instruction semantics) is allowed. This predicate is written using relatively straightforward relational algebra, so it should be relatively easy to test whether an execution satisfies the predicate. However, most tools combine the instruction semantics with the predicate checking. The goal of this project would be to develop a predicate testing tool that takes an execution and a relational model, and feeds it into an SMT solver to decide whether the execution is allowed.
aarch64.cat https://github.com/herd/herdtools7/blob/master/herd/libdir/aarch64.cat The offline mode of cppmem supports such a functionality http://svr-pes20-cppmem.cl.cam.ac.uk/cppmem/
(co-advisor Kayvan Memarian)
The state of the art in semantics of the C programming language, Cerberus, is defined by elaboration (faithful compilation) to an intermediate language, Core. Core makes syntactically explicit much of the complexity of C, and opens up the possibility to mechanise the metatheory of C. The goal of this project is to mechanise the definition of the semantics of Core, and then prove that Core has the expected properties, in particular determinacy for specific subset of the language. It would also make it possible to verify correctness of Core-to-Core optimisations that are used to execute Cerberus faster. Making the language definition an instance of the Iris language class would also make it possible to verify individual C programs. Knowledge of the Coq / Rocq proof assistant is required.
https://www.cl.cam.ac.uk/~km569/into_the_depths_of_C.pdf https://www.cl.cam.ac.uk/~pes20/cerberus/
PostScript is a page description language (like PDF, of which it is the ancestor), a language that describes the appearance of a printed page at a higher level of abstraction than a bitmap would. Structurally, postscript is a stack language whose semantics is, unusually, an image. The goal of this project is to mechanise the definition of (a significant subset of) the Postscript language and of its operational semantics, and (or: in the form of) an interpreter for PostScript that rasterises pages.
Postscript Blue Book: “PostScript Language Tutorial & Cookbook” https://archive.org/details/PSBlueBook Postscript Green Book: “PostScript Language Program Design” https://archive.org/details/PSGreenBook/page/n7/mode/2up
Lossless image formats range from the very simple (for example BMP) to the sophisticated (for example PNG and lossless JPEG). The goal of this project is to implement image formats (like BMP or PNG) in the form of their encoding and decoding functions, and of showing that these two functions are mutual inverses: decoding and re-encoding yields the same image.
Formally Verified Quite OK Image Format, Kunčar https://ieeexplore.ieee.org/document/10026566
Reactive Scratch is an educational programming environment designed to help children enjoy programming by using a synchronous programming language, Esterel, as its foundation, instead of the more common shared memory imperative programming. The goal of this project is to write an Esterel to WebAssembly compiler to replace the naïve, slow interpreter of Reactive Scratch.
https://www.cl.cam.ac.uk/~jp622/reactive-scratch/
(co-advisor Bas Spitters) WebAssembly is a language designed to be the compilation target to run programs in web browsers. WebAssembly is interesting, because it is at the same time a widely used web standard, supported by all major browser vendors, and a small and clean enough language to work with in a proof assistant. LLVM IR is a high-level assembly language that is used as the internal representation of the optimisation phases of the LLVM suite of compiler tools. Compilers for a variety of languages, including C (clang) and Rust (rustc), are composed of a front-end compiling the language to LLVM IR, and the LLVM optimisers and backends. A large subset of LLVM IR has also been formalised in a proof assistant. The goal of the project is to (1) explore compilation between mainstream languages, and (2) explore verified compilation.
Note: The main difference between the two languages is the type of control structure, see below; this project would assume that you are given a structured control overlay.
Two Mechanisations of WebAssembly 1.0, Watt et al. https://hal.archives-ouvertes.fr/hal-03353748/
Modular, Compositional, and Executable Formal Semantics for LLVM IR, Zakowski et al. https://www.seas.upenn.edu/~euisuny/paper/vir.pdf
Formal verification of a realistic compiler, Leroy https://xavierleroy.org/publi/compcert-CACM.pdf
WebAssembly is an unusual compilation target, because it only features structured control (“if”, “while”, etc.), and not unstructured control (“goto”). This means that to compile a (more typical) low-level language with unstructured control to WebAssembly, one needs to reconstruct an equivalent program with structured control. The goal of the project is to (1) explore how such a structured control reconstruction algorithm, like Relooper or Stackifier, works, and (2) explore how to use a proof assistant to prove correctness of algorithms.
Beyond Relooper: Recursive Translation of Unstructured Control Flow to Structured Control Flow (Functional Pearl), Normal Ramsay
(co-advisor Bas Spitters)
Interactive theorem provers like Coq make it possible to develop a program and prove its properties in the same environment. In many cases, the program is also of interest outside of the theorem prover; therefore, the theorem prover makes it possible to extract such an internal program to an external file, possibly written in another language. However, this raises the question of how the extracted program relates to the internal program, especially if extraction involves non-trivial compilation. Coq provides both unverified extraction and a recent certified extraction, CertiCoq. CertiCoq targets Clight and depends on CompCert to produce verified machine code. For applications such as the web and blockchains (‘web3’), WebAssembly (abbreviated Wasm) has emerged as the standard assembly language. The goal of this project is to develop a WebAssembly backend to CertiCoq and verify it.
Note: Extend to handle arrays, maybe floats
Computer security relies on systems code to correctly manage the underlying hardware, especially the virtual memory mechanisms used to enforce controlled isolation between processes and virtual machines. This requires delicate synchronisation around page table accesses, to handle the subtle relaxed concurrency phenomena of virtual memory. These are not supported by conventional testing, semantics, or verification methods, so systems programmers have had to rely almost entirely on code review by domain experts. The goal of this project is to a develop and verify a relaxed-memory checker, based on a general model of Arm-A virtual memory, but specialised to the programming discipline used by systems code. This would allow us to do runtime checking during conventional testing, catching sequences with insufficient synchronisation without needing to detect the relaxed outcomes directly.
x86-TSO is the memory model of concurrency on x86. It has a simple, well-understood characterisation in terms of an operational semantics where writes by a thread move through a FIFO buffer. x86-TSO also has a characterisation in terms of an “axiomatic” memory model, that is, an acyclicity check over sets of unconstrained executions. This axiomatic memory model sheds a different light on the memory model, and lends itself well to bounded model checking. Currently, we have pen-and-paper proofs of equivalence of the operational memory model and a version of the axiomatic memory model written in an old style. Project The core of the project would involve mechanising, in a proof assistant: * the definitions of the operational and the axiomatic x86 memory models; * a proof of equivalence between them. There are interesting opportunities to extend the models and proofs with extra features, like mixed-sized accesses, to generated executable code from the models that can be integrated into testing and exploration tools, to extract a bounded model-checker, connect it to other formalisations (dual TSO, …), etc. Requirements The student should have a good grasp or a strong willingness to learn the following topics: * Relaxed memory models (for example Multicore Semantics) * Proof assistants (for example Interactive Formal Verification - although this course uses the Isabelle proof assistant) The student should have a good grasp of the following topics: * Operational semantics (for example IB Semantics of programming languages)