Repository Structure

The repository follows a layered structure where each directory has a single, clear ownership.

• Directoryhaven/

  • …
• Directory.github/

  • …
• Directoryworkflows/ CI pipeline definitions (ci.yml, nightly.yml, benchmark.yml, …)

  • …
• Directoryagents/ Specialized Copilot agent definitions

  • …
• CODEOWNERS Isolation-critical path ownership
• copilot-instructions.md AI assistant context
• Directorysrc/

  • …
• Directorycore/

  • …
• Directorymm/ Stage-2 page table management (stage2.c)

  • …
• Directoryirq/ Interrupt ownership and routing (ownership.c)

  • …
• Directorysched/ Budget-based temporal scheduler (budget.c)

  • …
• Directorydma/ SMMU / IOMMU policy (smmu.c)

  • …
• Directoryexc/ EL2 exception handler (el2_exceptions.c)

  • …
• Directoryarch/ Architecture-specific EL2 helpers (arm64)

  • …
• Directorytime/ Timer and budget accounting

  • …
• Directoryiommu/ IOMMU abstraction layer

  • …
• Directoryguest/

  • …
• Directorydrivers/ Guest UART driver stub (uart.c)

  • …
• Directoryrtos/ FreeRTOS integration layer (freertos_integration.c)

  • …
• Directorycommon/ Shared utilities

  • …
• Directoryplatform/ Board-specific initialisation hooks

  • …
• Directoryinclude/

  • …
• Directoryhaven/

  • …
• types.h Primitive typedefs (hv_u32, hv_u64, hv_status_t)
• stage2.h Stage-2 MMU API
• irq_ownership.h IRQ ownership API
• budget_sched.h Budget scheduler API
• smmu.h SMMU API
• el2_exceptions.h EL2 exception API
• guest_uart.h Guest UART API
• freertos_integration.h FreeRTOS API
• Directoryarch/ Architecture-specific headers

  • …
• Directoryconfigs/

  • …
• Directoryarm64/

  • …
• imx95-devkit.yaml Primary thesis platform config
• imx8qm-mek.yaml Secondary heterogeneous board config
• qemu-virt.yaml CI and developer QEMU config
• Directoryriscv/ (planned)

  • …
• Directoryx86/ (planned)

  • …
• Directorytests/

  • …
• Directoryunit/ Stub contracts, EL2 exc, SMMU, FreeRTOS, UART

  • …
• Directoryintegration/ Isolation flow, negative isolation tests

  • …
• Directoryisolation/ Planned cross-partition violation tests

  • …
• Directoryselftests/ Planned kernel selftests

  • …
• Directorydemos/ Planned demo scenarios

  • …
• Directoryscripts/

  • …
• build.sh Core C build
• test.sh Test runner
• style-check.sh Shell syntax + C syntax-only check
• check-configs.py YAML partition config validator
• ci-preflight.sh Full local CI gate
• ci-metadata.sh Build metadata capture
• benchmark-baseline.py Command timing baseline
• package-evidence.sh Evidence archive packager
• qemu-smoke.sh QEMU availability check
• setup-hooks.sh Git hook installer
• release.sh Release workflow
• Directorydocs/

  • …
• Directoryarchitecture/ OVERVIEW, ISOLATION_MODEL, THESIS_DEEP_DIVE

  • …
• Directorymethodology/ CI strategy, benchmarks, chapter traceability

  • …
• Directoryporting/ i.MX95 setup, validation runbooks, porting guide

  • …
• Directoryroadmap/ Milestones, release specs (R1–R4)

  • …
• Directorysafety/ Threat model, assumptions

  • …
• Directoryapi/ API placeholder

  • …
• Directorywebsite/ This Astro Starlight documentation site

  • …
• Directorybuild/ Generated artefacts (gitignored)

  • …
• Directoryverification/ Coq and Isabelle formal proofs (planned)

  • …
• Directorytools/

  • …
• Directoryconfig-gen/ Config compiler tooling (planned)

  • …
• Directoryanalysis/ Static analysis scripts

  • …
• Directorydrivers/

  • …
• Directorylinux/ Linux guest driver modules (planned)

  • …
• Directoryguest-tools/ Guest userspace tools (planned)

  • …

Key Design Boundaries

src/core/ is the Trusted Computing Base

All code under src/core/ runs at EL2 and is the TCB. Changes here require an Isolation Guardian review. Every function must have a corresponding unit or integration test.

include/haven/ is the Stable Interface

Headers under include/haven/ define the only API surface that tests and platform code use. Changes here are breaking changes and require a version bump.

configs/ drives partition topology

YAML configs are the single source of truth for partition boundaries. The check-configs.py validator enforces required fields at every CI run.

website/ is decoupled from the build

The Astro documentation site under website/ is deployed independently to Vercel. It does not affect the C build or test pipeline.