Motivation
Fiducia is an orchestration language built on top of Microkit/seL4 that separates channel communication from low-level computation code, so that computation is orchestrated around communication events. It not only modularises embedded-system application design but also enables auto-formalisation: extracting formal models, checkable by model checkers, directly from Fiducia code. This realises the goal of unifying program and model under one roof, so that only a single source of truth needs to be maintained — the real power is that when the implementation evolves, the model can be automatically kept in sync with the code. This makes Fiducia a true enabler of embedding formal verification into the software development life cycle (SDLC).
We are actively developing the compiler behind Fiducia, and type checking is one of the pieces still missing. Nothing today verifies that expressions, assignments, and channel messages respect their declared types, and the compiler’s High/Low security labels on memory are checked only against each other — never against what a component’s own logic actually does with the data. In a language built for the low-level, security-relevant components of an operating system, that is exactly the safety net a compiler should provide, and Fiducia’s doesn’t have it yet.
The gap gets sharper at one specific point: Fiducia programs can call out to functions implemented externally, in a foreign language such as C. In addition to the normal type checker, we will need to check the types at the language boundary.
Goal
-
A basic type checker for the language. Implement checking for the core rules any statically typed language needs: arithmetic and comparison operators only combine compatible types, assignments match a variable’s declared type, structured record field access resolves to a real field of the right type, and a message sent over a channel matches the type the channel was declared to carry.
-
Extending that checking across the C function-call boundary. That includes extracting real function signatures from the actual C header files being imported, via a Clang/
bindgen-based pipeline. -
Explicit data-flow checking for information flow. Fiducia as a security-by-construction language extends its type system with security typing, e.g., labels shared memory with a security level (
High/Low). In this project, it is also expected to extend the type checking algorithm to explicit secure data flow, avoiding data read from a high secrecy memory written into a low memory region.
Bonus
- Make the C-signature-extraction step incremental, so it only reruns when a header file has actually changed rather than on every build.
- Implement type checking at the language boundary with code written in Pancake, an in-house driver programming language designed by the Trustworthy Systems team, built upon the CakeML verified compilation toolchain to provide strong correctness guarantees on the generated executable code.
Requirement
- Proficiency in Rust (the compiler’s implementation language).
- Familiarity with static type systems or basic compiler construction — an undergraduate programming-languages or compilers course is enough background.
What you will learn
Real engineering practice: implementing a type checker against first principles inside an existing, unfamiliar production compiler, working across a real language boundary between two different programming languages, and the standard collaborative software-engineering workflow (issues, pull requests, code review).