Keyboard shortcuts

Press ← or → to navigate between chapters

Press S or / to search in the book

Press ? to show this help

Press Esc to hide this help

Introduction

Fiducia is a language for building embedded applications on seL4 Microkit systems. A Fiducia project describes a system of protection domains (PDs) connected by channels, each PD implemented by external C / Rust code and modelled by a CSP-style process algebra. From this single description the toolchain produces both a bootable Microkit image and a formal model that can be checked for deadlock-freedom.

This manual is the task-oriented guide to the toolchain. For the syntax and semantics of the language itself, see the Fiducia Language Reference — it stays focused on .fis / .fi syntax, while this manual covers installing, configuring, running, and verifying projects day-to-day.

🚧 Fiducia is under active development. The language and tools are not yet complete; interfaces described here may change between releases.

The toolchain at a glance

ToolRole
ficThe compiler: parses, validates, and type-checks a project; emits ASTs, SDF XML, topology graphs, UPPAAL models, or a bootable Microkit image.
fireThe project runner: reads fire.toml and drives fic — fire build produces the image, fire run builds and launches it on QEMU or hardware, fire verify model-checks the UPPAAL model with verifyta.

A Fiducia project

A project is a directory containing:

  • one .fis file — the system description: memory regions, protection domains, channels, and the system composition;
  • one .fi file per protection domain — the PD implementation: imports of C sources, memory mappings, event declarations, and process definitions (the file eth_outer.fi implements the PD named eth_outer);
  • the imported .c implementation files (.rs imports parse but aren’t runnable yet — the C backend rejects them; see --emit=c);
  • a fire.toml manifest telling fire how to build and run it (see The Project Manifest).

The compiler pipeline is:

discover → parse → resolve → validate → typecheck → WF2 → emit

where typecheck enforces information-flow security (no High→Low leaks via channels) and WF2 checks the channel dependency graph for cycles (a structural deadlock-freedom condition).

Where to go next

  1. Install the tools.
  2. Write or copy a fire.toml.
  3. Build and run on QEMU — the demo/datadiode/ project in the repository is a complete worked example.
  4. Verify deadlock-freedom.
  5. Consult the fic reference for the individual compiler emit modes.