Figure 26 — Compiler-Security Separation
The compiler produces code words in the correctness domain, outside the Trusted Computing Base. The hardware validates Golden Tokens, enforces bounds, and hardcodes domain permissions in the security domain, inside the TCB. Compiler bugs affect correctness within the security perimeter but cannot breach it.
TRUST BOUNDARY
OUTSIDE TCB
INSIDE TCB
Correctness Domain
Compiler responsibility — bugs produce wrong answers, never security violations
CLOOMC++ Compiler
JavaScript front-end (imperative)
Haskell front-end (functional)
Resident Object Model (c-list → offsets)
Code Generator (32-bit instruction words)
Compiled Output
IADD DR4, DR0, #1 → 0x1E810001
MCMP DR0, #0 → 0x1C800000
BRANCH.EQ +3 → 0x22100003
RETURN → 0x06000000
Compiler Bugs (Correctness Failures)
• Wrong register allocation → wrong value computed
• Incorrect branch target → wrong method path taken
• Miscomputed c-list offset → wrong abstraction called
• Bad immediate encoding → arithmetic produces wrong result
All produce wrong answers — none escape the lump
✗
✗
✗
Why Compiler Bugs Cannot Breach Security
No instruction sequence can forge a Golden Token
No code can escape lump bounds (NS entry limit)
No code can access GTs not in its own c-list
Security Domain (Trusted Computing Base)
Hardware responsibility — enforces invariants regardless of compiled code
mLoad Gate (Read Path)
1. GT Type check (NULL → FAULT)
2. Version match (stale → FAULT)
3. Seal verify (tampered → FAULT)
4. Bounds check (overflow → FAULT)
5. Permission check (denied → FAULT)
6. F-bit check (remote → tunnel)
mSave Gate (Write Path)
1. GT Type check (NULL → FAULT)
2. Version match (stale → FAULT)
3. Seal verify (tampered → FAULT)
4. Bounds check (overflow → FAULT)
5. Write permission (W or S required)
6. B-bit check (bind propagation)
CALL Domain Enforcer
After mLoad validates E-GT:
Parse clistCount from word1
CR14 → X-only (HARDCODED)
CR6 → L-only (HARDCODED)
PC = 0 (execution starts at top)
B-bit cleared on preserved CRs
Hardware-Enforced Invariants
✓ Every memory access passes through mLoad or mSave
✓ Domain purity: Church (L,S,E) and Turing (R,W,X) never mix
✓ GTs cannot be forged — no instruction creates a GT from data
✓ Lump bounds enforced — code cannot read/write beyond limit
✓ Version revocation instant — all copies invalidated at once
TCB Size Comparison
Linux kernel: ~30,000,000 lines
seL4: ~10,000
Church Machine TCB: ~329 lines HDL
5 orders of magnitude smaller than Linux
Code words flow down
Every validation failure at any stage → single FAULT handler — no silent fallback, no default allow
Compiler bugs (correctness only)
mLoad Gate (read validation)
mSave Gate (write validation)