Capability Attenuation Framework

A formal model for capability-restricted sandboxed execution.

Definitions

Source Language

A source language S is defined by:

Syntax: Grammar of valid programs
Semantics: Meaning of programs (operational or denotational)
Capabilities C_S: Set of operations programs may perform

Target Runtime

A target runtime T is defined by:

Execution model: How programs execute
Capabilities C_T: Set of operations the runtime permits
Isolation boundary: Separation between instances

Attenuator

An attenuator A: S → T is a transformation (compiler, transpiler, interpreter) that converts source programs to target programs.

Formal Properties

Soundness

An attenuator A is SOUND if and only if:

∀p ∈ S, ∀c ∈ C_S:
  (c ∉ C_T) ⟹ (A(p) cannot exercise c at runtime)

Informally: capabilities not granted by the runtime cannot be exercised, regardless of what the source program attempts.

Example: If the target runtime doesn't provide filesystem access, a sound attenuator ensures the compiled program cannot access the filesystem, even if the source program contains filesystem operations.

Completeness

An attenuator A is COMPLETE if and only if:

∀p ∈ S:
  (p uses only c ∈ C_S ∩ C_T) ⟹ (⟦A(p)⟧_T = ⟦p⟧_S)

Informally: if a program only uses capabilities available in both source and target, its meaning is preserved.

Example: A program that only performs arithmetic should produce the same results after compilation as it would in the source language.

Forensic Capture

A runtime T supports FORENSIC CAPTURE if and only if:

∀ execution e of program p that terminates abnormally:
  T produces state snapshot σ such that:
  - σ contains sufficient information to determine failure cause
  - σ is captured atomically at moment of failure
  - σ is isolated from subsequent executions

Example: When a WASM trap occurs, the runtime captures the complete linear memory state before any cleanup, allowing post-mortem analysis.

The Munition Framework

Capability Classes

Capability	Description	Default	Risk	Validated
`compute`	Execute instructions	Granted	N/A	implicit
`memory_read`	Read linear memory	Granted	Low	implicit
`memory_write`	Write linear memory	Granted	Low	implicit
`host_call`	Call host functions	Per-function	Medium	as `{:host_function, name}`
`log`	Write to log output	Configurable	Low	atom
`time`	Access system time	Configurable	Low	atom
`random`	Access entropy	Configurable	Low	atom
`filesystem_read`	Read files	Denied	Medium	atom
`filesystem_write`	Write files	Denied	High	atom
`network`	Network access	Denied	High	atom

The Validated column tells you what kind of value Munition.Host.Capabilities.valid?/1 recognises for each capability:

implicit — always-granted baseline; the runtime cannot turn these off, so they don't appear in the explicit grant list and valid?(:compute) is intentionally false.
{:host_function, name} — host calls are validated as a tagged tuple rather than a flat atom because they are parameterised by the host function being invoked.
atom — listed in @standard_capabilities and recognised by valid?/1. These are the atoms a caller actually passes via opts[:capabilities] on Munition.fire/4.

The atoms in the Validated = atom rows above are exactly the elements of @standard_capabilities in lib/munition/host/capabilities.ex — keep the two in sync.

Attenuation Strategies

Different source languages require different attenuation approaches:

Restrictive Attenuation (PHP, JavaScript)

Source language has implicit universal capabilities. The attenuator must impose restrictions that the source language doesn't express.

C_S = {compute, memory, filesystem, network, time, random, ...}
C_T = {compute, memory}  (default)

Transformation:
- Every filesystem call → host function call (interceptable)
- Every network call → host function call (interceptable)
- Host denies by default, grants explicitly

Properties:

Sound: Yes, by construction (all capability exercise goes through host)
Complete: Only for pure computation

Preserving Attenuation (Pony)

Source language has explicit typed capabilities. The attenuator maps source capabilities to target capabilities.

Pony iso → Rust Box<T> / owned value
Pony val → Rust Arc<T> / shared immutable
Pony ref → Rust (complicated - requires actor model)
Pony box → Rust &T
Pony tag → Rust *const () (identity only)

Properties:

Sound: If mapping is correct
Complete: For the mappable subset

Challenge: Pony's ref (multiple mutable references within actor) doesn't map to Rust without unsafe or actor runtime.

Additive Attenuation (Rust)

Source language already has ownership/safety guarantees. Compiling to WASM adds additional isolation.

C_S = {compute, memory (with ownership), ...}
C_T = {compute, memory, fuel_bound, memory_isolation}

Rust ownership guarantees preserved
WASM adds:
- Linear memory isolation
- Fuel bounding (not in Rust)
- Instance isolation (not in Rust)

Properties:

Sound: Inherited from Rust + WASM
Complete: Yes (Rust → WASM is well-defined)

Soundness Proof Sketch

Theorem: Munition's execution model is sound with respect to the declared capability set.

Proof:

WASM provides a capability-secure execution environment:
- No ambient authority (all capabilities via imports)
- Memory isolation (linear memory per instance)
- Control flow integrity (structured control flow)
Munition's import construction is capability-gated:
- build_imports/1 only includes functions for granted capabilities
- Non-granted capabilities result in missing imports
- Missing imports cause instantiation failure (not runtime failure)
Fuel bounding ensures termination:
- Every instruction consumes fuel
- Fuel is checked before execution
- Exhaustion halts execution deterministically
Forensic capture is atomic:
- Capture occurs immediately on failure
- Memory is read-only after capture point
- No modification possible between failure and capture

Therefore, the system is sound: no capability outside the granted set can be exercised, and all executions terminate. □

Formal Specification (TLA+)

---------------------------- MODULE Munition ----------------------------
EXTENDS Naturals, Sequences, TLC

CONSTANTS
    MaxFuel,        \* Maximum fuel allocation
    Capabilities    \* Set of all capabilities

VARIABLES
    fuel,           \* Current fuel remaining
    memory,         \* Linear memory state
    status,         \* running | completed | trapped | exhausted
    granted,        \* Set of granted capabilities
    dump            \* Forensic dump (if failed)

vars == <<fuel, memory, status, granted, dump>>

TypeInvariant ==
    /\ fuel \in 0..MaxFuel
    /\ status \in {"running", "completed", "trapped", "exhausted"}
    /\ granted \subseteq Capabilities
    /\ dump \in SUBSET (Capabilities \X Seq(0..255))

Init ==
    /\ fuel = MaxFuel
    /\ memory = <<>>
    /\ status = "running"
    /\ granted \in SUBSET Capabilities
    /\ dump = {}

ExecuteInstruction ==
    /\ status = "running"
    /\ fuel > 0
    /\ fuel' = fuel - 1
    /\ UNCHANGED <<memory, status, granted, dump>>

CallHostFunction(cap) ==
    /\ status = "running"
    /\ cap \in granted
    /\ fuel > 0
    /\ fuel' = fuel - 1
    /\ UNCHANGED <<memory, status, granted, dump>>

DenyHostFunction(cap) ==
    /\ status = "running"
    /\ cap \notin granted
    /\ status' = "trapped"
    /\ dump' = {<<cap, memory>>}
    /\ UNCHANGED <<fuel, memory, granted>>

ExhaustFuel ==
    /\ status = "running"
    /\ fuel = 0
    /\ status' = "exhausted"
    /\ dump' = {<<"fuel", memory>>}
    /\ UNCHANGED <<fuel, memory, granted>>

Trap ==
    /\ status = "running"
    /\ status' = "trapped"
    /\ dump' = {<<"trap", memory>>}
    /\ UNCHANGED <<fuel, memory, granted>>

Complete ==
    /\ status = "running"
    /\ fuel > 0
    /\ status' = "completed"
    /\ UNCHANGED <<fuel, memory, granted, dump>>

Next ==
    \/ ExecuteInstruction
    \/ \E cap \in Capabilities: CallHostFunction(cap)
    \/ \E cap \in Capabilities: DenyHostFunction(cap)
    \/ ExhaustFuel
    \/ Trap
    \/ Complete

\* Safety: No ungrated capability can be exercised
CapabilitySafety ==
    \A cap \in Capabilities:
        (cap \notin granted) =>
            ~(\E s \in dump: s[1] = cap /\ s[1] # "trap" /\ s[1] # "fuel")

\* Liveness: All executions terminate
Termination ==
    <>(status # "running")

\* Forensics: Failed executions have dumps
ForensicCapture ==
    (status \in {"trapped", "exhausted"}) => (dump # {})

==========================================================================

Research Directions

1. Capability Inference

Given a source program, automatically infer minimum required capabilities:

infer: Program → Set<Capability>

Such that:
  ∀p: fire(compile(p), granted=infer(p)) succeeds iff p is valid

2. Graduated Trust

Dynamic capability expansion based on execution history:

trust_level(plugin, history) → Set<Capability>

Where:
  - New plugins get minimal capabilities
  - Successfully behaving plugins gain capabilities
  - Misbehaving plugins lose capabilities

3. Capability Composition

Safe composition of multiple sandboxed modules:

compose: (Module, Capabilities) × (Module, Capabilities) → (Module, Capabilities)

Such that:
  C_composed ⊆ C_1 ∪ C_2

4. Forensic Analysis Automation

Automated analysis of crash dumps to identify:

Root cause classification
Exploitation attempt detection
Capability escalation attempts

References

Miller, M. S. (2006). Robust Composition: Towards a Unified Approach to Access Control and Concurrency Control. PhD thesis.
Clebsch, S., et al. (2015). Deny Capabilities for Safe, Fast Actors. AGERE.
Haas, A., et al. (2017). Bringing the Web up to Speed with WebAssembly. PLDI.
Watson, R. N. M., et al. (2015). CHERI: A Hybrid Capability-System Architecture for Scalable Software Compartmentalization. IEEE S&P.

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

Uh oh!

Capability Attenuation Framework

Definitions

Source Language

Target Runtime

Attenuator

Formal Properties

Soundness

Completeness

Forensic Capture

The Munition Framework

Capability Classes

Attenuation Strategies

Restrictive Attenuation (PHP, JavaScript)

Preserving Attenuation (Pony)

Additive Attenuation (Rust)

Soundness Proof Sketch

Formal Specification (TLA+)

Research Directions

1. Capability Inference

2. Graduated Trust

3. Capability Composition

4. Forensic Analysis Automation

References

Uh oh!

FilesExpand file tree

capability_model.md

Latest commit

History

capability_model.md

File metadata and controls

Capability Attenuation Framework

Definitions

Source Language

Target Runtime

Attenuator

Formal Properties

Soundness

Completeness

Forensic Capture

The Munition Framework

Capability Classes

Attenuation Strategies

Restrictive Attenuation (PHP, JavaScript)

Preserving Attenuation (Pony)

Additive Attenuation (Rust)

Soundness Proof Sketch

Formal Specification (TLA+)

Research Directions

1. Capability Inference

2. Graduated Trust

3. Capability Composition

4. Forensic Analysis Automation

References