# seL4 HAMR: Model-Based High-Assurance Engineering HAMR (High Assurance Modeling and Rapid engineering) is an open-source model-driven development framework for safety-critical embedded systems, developed by the SAnToS Lab at Kansas State University (lead: Prof. John Hatcliff) in collaboration with Collins Aerospace, Dornerworks, and Aarhus University. It was applied on the DARPA CASE (Cyber Assured Systems Engineering) program to generate seL4/C-based applications for UAV mission computing on the Boeing CH-47 Chinook platform. Primary sources: Sireum HAMR (hamr.sireum.org); Belt et al., "Model-Driven Development for the seL4 Microkernel Using the HAMR Framework" (J. Systems Architecture, 2022); Hatcliff et al., "HAMR: An AADL Multi-Platform Code Generation Toolset" (ICSA 2021); Hatcliff et al., seL4 Summit 2025 keynote ("Model-based Development for seL4 Microkit/Rust with Integrated Formal Methods using HAMR"); GUMBO contract language (Galois / SAnToS Lab); seL4 Foundation CAmkES documentation. --- ## 1. What HAMR Is HAMR operates across three development layers: 1. **Architecture modeling** -- The system is specified in AADL (SAE AS5506) or SysMLv2. The model captures component topology, port-based communication, timing/scheduling properties (periodic, sporadic, aperiodic threads), and GUMBO behavioral contract annotations. 2. **Code generation** -- HAMR generates deployment infrastructure (inter-component communication glue, tasking, platform configuration) and typed component skeletons developers fill with application logic. Output languages: Slang, C, and (as of 2025) Rust. 3. **Verification infrastructure** -- GUMBO model contracts are translated to source-level contracts for Logika (Slang), Verus (Rust), and executable property-based test oracles. Platform backends: JVM, Linux, seL4/CAmkES (C), and seL4 Microkit (Rust, 2025 work). --- ## 2. The AADL Model AADL is an SAE international standard (AS5506) for architecture description of embedded, real-time, safety-critical systems. Key concepts relevant to the HAMR/seL4 mapping: - **Components**: hierarchically typed -- `system`, `process`, `thread`, `device`, `data`, `subprogram`, `bus`. `thread` is the unit of concurrent execution; `process` is the protected address space containing one or more threads. - **Ports**: typed communication endpoints attached to components. - *Data port*: most-recent-value semantics; sender writes, receiver reads at next dispatch. - *Event port*: queued notification with no data payload. - *Event data port*: queued notification with a typed data payload. - **Connections**: directed edges between compatible ports that define the data-flow and event-flow topology of the system. Connections are typed and directional; the model enforces that only compatible port kinds connect. - **Properties**: attach timing, scheduling, size, and other non-functional attributes to components and connections (e.g. `Dispatch_Protocol => Periodic`, `Period => 10 ms`, `Queue_Size => 8`). - **Behavior Annex (SAE AS5506/3)**: an optional state-machine sub-language for attaching internal behavioral specifications to components, formalizing the implicit execution semantics of threads. - **GUMBO**: a contract language (developed by Galois and KSU) that extends AADL with `requires` / `guarantees` / `compute` clauses attached to component implementations, serving as the model-level precondition/postcondition and data-invariant language. GUMBO integrates with the AADL Behavior Annex and is translated by HAMR into Slang/Logika contracts or Verus proof obligations. --- ## 3. The seL4/CAmkES Pipeline HAMR starts from the AADL instance model (as produced by OSATE, the open-source AADL editor) and generates: ### 3.1 CAmkES Topology Specification HAMR generates the complete CAmkES `.camkes` file describing the deployment topology. The mapping is: | AADL concept | CAmkES / seL4 concept | |---|---| | `process` component | CAmkES component (seL4 protection domain / "partition") | | `thread` component | CAmkES component with seL4 domain assignment (1-to-1) | | `thread` scheduling domain | seL4 domain scheduler domain ID | | Data port (sender → receiver) | CAmkES dataport (shared memory), write-only cap on sender, read-only cap on receiver | | Event/event-data port | CAmkES notification or queue construct | | Connection (A.out → B.in) | CAmkES connection with read/write permission split | The key isolation invariant: CAmkES read/write permission specifications are used to configure the seL4 kernel to enforce the directionality of AADL ports. The sender component holds a write-only capability to the shared dataport; the receiver holds a read-only capability. The kernel enforces this at the capability level -- no bypass is possible without a new capability grant. ### 3.2 Scheduling AADL's timing model (periodic/sporadic threads with bounded periods and deadlines) maps to the seL4 domain scheduler. Each AADL thread gets a static domain assignment. On the DARPA CASE work, time partitioning was enforced via the domain scheduler: each thread's time slice is determined at build time from the AADL timing properties and the domain schedule is generated as part of the HAMR output. ### 3.3 Generated Component Skeletons For each AADL thread, HAMR generates: - A component skeleton with `initialize`, `compute` (or `timeTriggered`/ `eventTriggered`), and `finalize` entry points. - Port API stubs: `get_()`, `put_()` functions that hide CAmkES shared-memory / notification mechanics behind a typed, uniform interface. This API is identical in shape across JVM, Linux, and seL4 backends -- developer code calls the same interface regardless of platform. ### 3.4 Slang Reference Implementation HAMR's C skeleton APIs are derived from the Slang reference implementation. Slang is Sireum's safety-critical subset of Scala: immutable-by-default, bounded loops, no reflection, and a restricted type system suited to Logika verification. The Slang implementation serves as a verified reference that the C and Rust backends are expected to match semantically. ### 3.5 The 2025 seL4 Microkit / Rust Extension As of the 2025 seL4 Summit work (DARPA PROVERS INSPECTA project), HAMR generates Rust component skeletons deployable in seL4 Microkit protection domains. HAMR auto-generates the Microkit system description file, developer- facing channel/notification APIs for Rust threads, and Verus contract stubs from GUMBO model annotations. This is an active development track; the C/CAmkES backend is the more mature path. --- ## 4. Verification Model HAMR's verification approach is layered: 1. **GUMBO model contracts**: `requires`/`guarantees` clauses on AADL components capture the intended behavioral contract at the architecture level. These are part of the model, not the code. 2. **Translated code contracts**: HAMR translates GUMBO into Slang/Logika proof obligations or Verus specifications. The translation preserves the model-level contract's semantic intent in the target language's contract system. 3. **Logika / Verus verification**: Tools verify that the developer's component implementation satisfies the translated contracts. Logika operates on Slang; Verus operates on Rust. 4. **Property-based test oracles**: HAMR also generates executable test harnesses that check GUMBO contract conformance at runtime, complementing formal verification with systematic testing. 5. **seL4 kernel verification**: The underlying seL4 kernel is formally verified (machine-checked proof of functional correctness in Isabelle/HOL covering integrity and confidentiality). HAMR sits above this: its generated CAmkES specification maps to a seL4 capability topology that the verified kernel enforces. The combination targets the argument that the system's isolation structure (as modeled in AADL) is correctly realized by the verified kernel. The assurance case HAMR targets is roughly: AADL model (structural) + GUMBO (behavioral) + Logika/Verus (code-level conformance) + seL4 (kernel-level isolation proof) → high-assurance system suitable for DO-178C / DO-331 objectives. This layered argument is the distinguishing feature versus a conventional RTOS-based development process. --- ## 5. Applicability to capOS ### 5.1 Where the Approaches Align Both HAMR and capOS treat the formal interface definition as the authoritative contract layer. HAMR uses the AADL model + GUMBO contract annotations; capOS uses the Cap'n Proto schema. Both insist that the interface *is* the permission: in HAMR, an AADL connection determines which component can write to which port, and the generated CAmkES capability configuration enforces that topology; in capOS, holding a capability to a CapObject determines what methods a caller can invoke, and narrower capabilities enforce tighter access. Both generate typed, platform-adapted communication glue from the interface definition. HAMR generates port API stubs and CAmkES/Microkit configuration; capOS generates (via capnpc + capos-rt) the typed method dispatch layer that clients call. ### 5.2 Static vs. Dynamic Capability Topology The sharpest structural difference: HAMR produces a **closed, static topology**. All components, connections, and capability distributions are fixed at build time. CAmkES explicitly does not allow runtime changes -- the set of components and their communication channels is defined at system configuration time and instantiated at boot. This is intentional: the full topology can be statically analyzed, and the seL4 capability distribution can be checked against a capDL (capability distribution language) model as part of the assurance case. capOS is designed around **dynamic capability routing**. The kernel acts as a capnp-rpc router; new capabilities can be forged by authorized processes, transferred via Move/Copy grants, and held in per-process CapTables that grow and change at runtime. The `ProcessSpawner`, `AuthorityBroker`, and `SessionManager` capabilities enable runtime-created service graphs. This is not a weakness -- it is the whole point of a capability-rpc OS -- but it means the topology at any moment is not checkable against a static model. For capOS's current research target, the dynamic model is the right fit. For a flight-critical avionics partition, the static model is the right fit. These are different points on the assurance-vs-flexibility tradeoff. ### 5.3 Generated Glue vs. Manual CapObject Dispatch In HAMR, the developer writes *only* application logic in `initialize`/ `compute`/`finalize` entry points; all communication infrastructure is generated. The developer-visible API is uniform across backends -- the same `get_altimeter()` call works on JVM, Linux, and seL4. In capOS, capability dispatch is currently manual: each `CapObject` implementation handles capnp message bytes directly via match-on-method-ID. The typed client wrappers in `capos-rt` abstract this for callers, but the server-side skeleton is hand-written per capability type. HAMR's approach suggests an achievable improvement: if capOS had a `capnpc` plugin or a build tool that generated `CapObject` dispatch stubs and server-side skeletons from `.capnp` schemas, the authoring burden per capability type would shrink significantly. The schema already carries everything needed to generate the match arm, parameter decode, and return encode. ### 5.4 Model-Driven Partition Generation HAMR demonstrates the utility of driving the entire partition topology -- not just per-component skeletons -- from the model. The CAmkES `.camkes` file, the domain schedule, the capability permission split, and the component binaries all originate from a single AADL instance model. This is "the model is the system" in the most literal sense. capOS has no equivalent today. Service-graph topology is described in CUE/AADL manifests and executed dynamically by `init`. For future high-assurance work (e.g., flight-critical or safety-certified deployments), a model-driven generation step that produces both the `system.cue` manifest and the capability grant topology from a formal model would be directly applicable. The capnp schema would serve as the interface contract (as it already does), while a system-level architecture model would specify the instantiation and wiring. ### 5.5 Contract Verification Gap HAMR demonstrates a full contract pipeline: model annotation (GUMBO) → generated code contracts (Logika / Verus) → formal verification. capOS has no equivalent for CapObject implementations. The `.capnp` schema defines the method signatures and types, but there is no Logika/Verus-style annotation layer for pre/postconditions on individual capability method handlers. For a research OS this is acceptable -- capOS's assurance comes from seL4-style kernel isolation, not from verified component behavior. But the HAMR model shows what the path to component-level behavioral verification looks like when starting from a schema-as-contract baseline. ### 5.6 AADL vs. Cap'n Proto as the Schema Layer AADL carries significantly more non-functional information than Cap'n Proto schemas: scheduling properties (period, deadline, dispatch protocol), port queue depths, memory footprint bounds, required hardware (device associations), and safety annex annotations. Cap'n Proto schemas carry method signatures, field types, and (via annotations) some semantic metadata, but scheduling and resource-budget properties are out of scope for the format. For capOS's current use -- typed RPC dispatch, schema-stable ABI, and code-generation for typed clients and server stubs -- Cap'n Proto is the right tool. AADL is not a replacement: it is a higher-level architecture modeling language that sits above the RPC schema layer and consumes it. A future model-driven capOS toolchain would use AADL or SysMLv2 at the system level and capnp schemas at the interface level, not choose one over the other. --- ## 6. Open Questions for Future Evaluation - **capnpc → CapObject stub generation**: Given that the capnp schema fully describes method signatures, types, and return shapes, how much of the server-side `CapObject` dispatch boilerplate could a code-gen plugin eliminate? HAMR's generated skeletons suggest this is tractable. - **System-manifest generation from a topology model**: Could a lightweight AADL-or-SysMLv2 instance model (or a CUE-native equivalent) generate the `system.cue` manifest, the initial CapTable grants, and a capDL-style verification model for the static portion of the system graph? - **GUMBO-inspired contract annotations in capnp schemas**: Could capnp annotation syntax be used to attach precondition/postcondition stubs (analogous to GUMBO's `requires`/`guarantees`) to interface methods, enabling future Verus or Creusot verification of CapObject implementations? - **seL4 Microkit vs. CAmkES**: The 2025 HAMR work migrates from CAmkES to the newer seL4 Microkit, which uses Rust and a simpler protection-domain model. If capOS ever targets seL4 as an optional verified kernel backend, Microkit + HAMR would be the current recommended entry point. --- ## Sources - [Sireum HAMR](https://hamr.sireum.org/) -- framework home page, pipeline overview, platform backends, GUMBO contract language reference. - [Belt et al., "Model-Driven Development for the seL4 Microkernel Using the HAMR Framework" (J. Systems Architecture, 2022)](https://www.sciencedirect.com/science/article/abs/pii/S1383762122002740) -- primary journal paper on the AADL→seL4/CAmkES mapping. - [Belt et al., preprint (Loonwerks)](https://loonwerks.com/publications/pdf/belt2022aeic.pdf) -- open-access preprint of the above. - [Hatcliff et al., "HAMR: An AADL Multi-Platform Code Generation Toolset" (ICSA 2021, Springer)](https://link.springer.com/chapter/10.1007/978-3-030-89159-6_18) -- multi-platform overview paper. - [Hatcliff et al., "Model-based Development for seL4 Microkit/Rust with Integrated Formal Methods using HAMR", seL4 Summit 2025 keynote](https://www.youtube.com/watch?v=gP1klZJi04U) -- Rust/Microkit extension, Verus integration, Collins/Dornerworks INSPECTA application. - [seL4 Summit 2025 Abstracts](https://sel4.systems/Summit/2025/abstracts2025.html) -- abstract for the HAMR keynote above. - [ResearchGate: HAMR to seL4 Code Generation Concepts diagram](https://www.researchgate.net/figure/HAMR-to-seL4-Code-Generation-Concepts_fig7_365647878) -- visual of the AADL→CAmkES generation pipeline. - [GUMBO contract language (Galois)](https://www.galois.com/project/gumbo) -- GUMBO overview: model-level contract annotation and auto-insertion into Slang code. - [ACM SIGAda 2023: "An AADL Contract Language Supporting Integrated Model- and Code-Level Verification"](https://dl.acm.org/doi/abs/10.1145/3591335.3591339) -- GUMBO design and integration paper. - [SAnToS Lab HAMR system-testing case studies (GitHub)](https://github.com/santoslab/hamr-system-testing-case-studies) -- open-source example systems with GUMBO contracts and generated Logika/Slang verification targets. - [CAmkES GitHub manifest](https://github.com/seL4/camkes-manifest) -- CAmkES static-architecture model, component/connection model, capDL. - [DARPA CASE program](https://www.darpa.mil/program/cyber-assured-systems-engineering) -- program context for HAMR's real-world application. - [Ongoing seL4 Research | seL4 Foundation](https://sel4.systems/Research/ongoing.html) -- includes HAMR as an active seL4 research track. - [SAE AS5506/3: AADL Behavior Model Annex](https://saemobilus.sae.org/standards/as55063-architecture-analysis-design-language-aadl-annex-d-behavior-model-annex) -- the AADL Behavior Annex standard that GUMBO extends.