|
| 1 | +// SPDX-License-Identifier: CC-BY-SA-4.0 |
| 2 | +// SPDX-FileCopyrightText: 2025-2026 Jonathan D.A. Jewell <j.d.a.jewell@open.ac.uk> |
| 3 | + |
| 4 | += Munition (Chimichanga) |
| 5 | + |
| 6 | +image:https://img.shields.io/badge/OpenSSF-Best_Practices-green?logo=opensourcesecurity[OpenSSF Best Practices,link="https://www.bestpractices.dev/en/projects/new?repo_url=https://github.com/hyperpolymath/chimichanga"] |
| 7 | +image:https://img.shields.io/badge/License-MPL--2.0-blue.svg[License: PMPL-1.0,link="https://github.com/hyperpolymath/palimpsest-license"] |
| 8 | +image:https://api.thegreenwebfoundation.org/greencheckimage/github.com[Green Web,link="https://www.thegreenwebfoundation.org/green-web-check/?url=github.com"] |
| 9 | +:toc: macro |
| 10 | +:toclevels: 3 |
| 11 | +:icons: font |
| 12 | +:source-highlighter: rouge |
| 13 | +:sectanchors: |
| 14 | +:sectlinks: |
| 15 | + |
| 16 | +A capability attenuation framework for sandboxed WASM execution in Elixir. |
| 17 | + |
| 18 | +image:https://img.shields.io/badge/RSR-Gold-gold[RSR Gold] |
| 19 | +image:https://img.shields.io/badge/License-MPL--2.0-blue.svg[License: PMPL-1.0,link="https://github.com/hyperpolymath/palimpsest-license"] |
| 20 | +image:https://img.shields.io/badge/Elixir-1.14+-purple[Elixir] |
| 21 | + |
| 22 | +toc::[] |
| 23 | + |
| 24 | +== Overview |
| 25 | + |
| 26 | +Munition provides secure execution of untrusted WebAssembly code with three core guarantees: |
| 27 | + |
| 28 | +[cols="1,3"] |
| 29 | +|=== |
| 30 | +|Guarantee |Description |
| 31 | + |
| 32 | +|**Bounded Execution** |
| 33 | +|Fuel-metered computation that guarantees termination. Every WASM instruction consumes fuel; exhaustion halts execution deterministically. |
| 34 | + |
| 35 | +|**Memory Isolation** |
| 36 | +|Each execution gets fresh, isolated linear memory. No state leaks between executions. |
| 37 | + |
| 38 | +|**Forensic Capture** |
| 39 | +|Failure state is automatically captured for post-mortem analysis. Memory snapshots, fuel state, and execution context preserved atomically. |
| 40 | +|=== |
| 41 | + |
| 42 | +== The Capability Attenuation Model |
| 43 | + |
| 44 | +Munition implements a formal model for capability attenuation across language boundaries: |
| 45 | + |
| 46 | +[source] |
| 47 | +---- |
| 48 | +┌─────────────────┐ ┌─────────────────┐ ┌─────────────────┐ |
| 49 | +│ Source Code │ │ Attenuator │ │ Runtime │ |
| 50 | +│ (rich caps) │ ──▶ │ (compiler) │ ──▶ │ (restricted) │ |
| 51 | +│ │ │ │ │ │ |
| 52 | +│ PHP: can do │ │ Removes/maps │ │ WASM: can only │ |
| 53 | +│ anything │ │ capabilities │ │ do what host │ |
| 54 | +│ │ │ │ │ permits │ |
| 55 | +│ Pony: typed │ │ Preserves │ │ │ |
| 56 | +│ capabilities │ │ proofs │ │ Elixir: super- │ |
| 57 | +│ │ │ │ │ vises, captures│ |
| 58 | +└─────────────────┘ └─────────────────┘ └─────────────────┘ |
| 59 | +---- |
| 60 | + |
| 61 | +=== Attenuation Strategies |
| 62 | + |
| 63 | +[cols="1,2,2"] |
| 64 | +|=== |
| 65 | +|Strategy |Source Languages |Description |
| 66 | + |
| 67 | +|**Restrictive** |
| 68 | +|PHP, JavaScript |
| 69 | +|Source has implicit universal capabilities. Attenuator removes/intercepts all capability exercise. |
| 70 | + |
| 71 | +|**Preserving** |
| 72 | +|Pony |
| 73 | +|Source has typed capabilities. Attenuator maps source capabilities to target capabilities. |
| 74 | + |
| 75 | +|**Additive** |
| 76 | +|Rust |
| 77 | +|Source already has ownership guarantees. Runtime adds additional isolation (fuel, memory bounds). |
| 78 | +|=== |
| 79 | + |
| 80 | +== Architecture |
| 81 | + |
| 82 | +=== Component Overview |
| 83 | + |
| 84 | +[source] |
| 85 | +---- |
| 86 | +┌────────────────────────────────────────────────────────────────────┐ |
| 87 | +│ Public API │ |
| 88 | +│ Munition.fire/4 │ |
| 89 | +└─────────────────────────────────┬──────────────────────────────────┘ |
| 90 | + │ |
| 91 | +┌─────────────────────────────────▼──────────────────────────────────┐ |
| 92 | +│ Instance Manager │ |
| 93 | +│ Munition.Instance.Manager │ |
| 94 | +│ │ |
| 95 | +│ ┌──────────────┐ ┌──────────────┐ ┌──────────────────────────┐ │ |
| 96 | +│ │ Compile │→ │ Instantiate │→ │ Execute │ │ |
| 97 | +│ └──────────────┘ └──────────────┘ └──────────────────────────┘ │ |
| 98 | +│ │ │ │ │ |
| 99 | +│ ▼ ▼ ▼ │ |
| 100 | +│ ┌──────────────────────────────────────────────────────────────┐ │ |
| 101 | +│ │ Forensic Capture │ │ |
| 102 | +│ │ (on any failure path) │ │ |
| 103 | +│ └──────────────────────────────────────────────────────────────┘ │ |
| 104 | +└─────────────────────────────────┬──────────────────────────────────┘ |
| 105 | + │ |
| 106 | +┌─────────────────────────────────▼──────────────────────────────────┐ |
| 107 | +│ Runtime Behaviour │ |
| 108 | +│ Munition.Runtime │ |
| 109 | +│ │ |
| 110 | +│ ┌────────────────────┐ ┌────────────────────┐ │ |
| 111 | +│ │ Wasmex (default) │ │ (future runtimes) │ │ |
| 112 | +│ │ via Wasmtime │ │ │ │ |
| 113 | +│ └────────────────────┘ └────────────────────┘ │ |
| 114 | +└────────────────────────────────────────────────────────────────────┘ |
| 115 | +---- |
| 116 | + |
| 117 | +=== Module Structure |
| 118 | + |
| 119 | +[cols="2,3"] |
| 120 | +|=== |
| 121 | +|Module |Responsibility |
| 122 | + |
| 123 | +|`lib/munition.ex` |
| 124 | +|Public API: `fire/4`, `fire_pooled/4`, `validate/2` |
| 125 | + |
| 126 | +|`lib/munition/instance/manager.ex` |
| 127 | +|Lifecycle orchestration: compile → instantiate → execute → capture → cleanup |
| 128 | + |
| 129 | +|`lib/munition/instance/state.ex` |
| 130 | +|Instance lifecycle state tracking |
| 131 | + |
| 132 | +|`lib/munition/runtime/behaviour.ex` |
| 133 | +|Pluggable WASM engine interface |
| 134 | + |
| 135 | +|`lib/munition/runtime/wasmex.ex` |
| 136 | +|Wasmtime implementation via Wasmex |
| 137 | + |
| 138 | +|`lib/munition/forensics/dump.ex` |
| 139 | +|Structured crash dump format with MNTN serialization |
| 140 | + |
| 141 | +|`lib/munition/forensics/capture.ex` |
| 142 | +|Atomic state capture on failure |
| 143 | + |
| 144 | +|`lib/munition/forensics/analyser.ex` |
| 145 | +|Memory introspection and pattern searching |
| 146 | + |
| 147 | +|`lib/munition/fuel/policy.ex` |
| 148 | +|Default fuel allocations and complexity calculation |
| 149 | + |
| 150 | +|`lib/munition/fuel/meter.ex` |
| 151 | +|Consumption tracking and statistics |
| 152 | + |
| 153 | +|`lib/munition/host/functions.ex` |
| 154 | +|Host function registry with capability gating |
| 155 | + |
| 156 | +|`lib/munition/host/capabilities.ex` |
| 157 | +|Capability definitions and validation |
| 158 | +|=== |
| 159 | + |
| 160 | +== Quick Start |
| 161 | + |
| 162 | +=== Installation |
| 163 | + |
| 164 | +[source,elixir] |
| 165 | +---- |
| 166 | +# Add to mix.exs |
| 167 | +{:munition, "~> 0.1.0"} |
| 168 | +---- |
| 169 | + |
| 170 | +=== Basic Usage |
| 171 | + |
| 172 | +[source,elixir] |
| 173 | +---- |
| 174 | +wasm = File.read!("plugin.wasm") |
| 175 | +
|
| 176 | +case Munition.fire(wasm, "process", [input], fuel: 100_000) do |
| 177 | + {:ok, result, metadata} -> |
| 178 | + IO.puts("Result: #{inspect(result)}") |
| 179 | + IO.puts("Fuel remaining: #{metadata.fuel_remaining}") |
| 180 | +
|
| 181 | + {:crash, :fuel_exhausted, forensics} -> |
| 182 | + IO.puts("Execution exceeded fuel limit") |
| 183 | + IO.puts(Munition.Forensics.Dump.summary(forensics)) |
| 184 | +
|
| 185 | + {:crash, :trap, forensics} -> |
| 186 | + IO.puts("WASM trap occurred") |
| 187 | + analyser = Munition.Forensics.Analyser.new(forensics) |
| 188 | + IO.puts(Munition.Forensics.Analyser.hex_dump(analyser, 0, 256)) |
| 189 | +end |
| 190 | +---- |
| 191 | + |
| 192 | +=== Features in Action |
| 193 | + |
| 194 | +==== Fuel Metering (Guaranteed Termination) |
| 195 | + |
| 196 | +[source,elixir] |
| 197 | +---- |
| 198 | +# This will ALWAYS terminate - no infinite loops possible |
| 199 | +{:crash, :fuel_exhausted, _} = |
| 200 | + Munition.fire(wasm, "infinite_loop", [], fuel: 1_000) |
| 201 | +---- |
| 202 | + |
| 203 | +==== Memory Isolation |
| 204 | + |
| 205 | +[source,elixir] |
| 206 | +---- |
| 207 | +# Execution A writes to memory |
| 208 | +Munition.fire(wasm, "write_data", [pattern]) |
| 209 | +
|
| 210 | +# Execution B cannot see it - fresh memory every time |
| 211 | +{:ok, [0], _} = Munition.fire(wasm, "read_data", [0]) |
| 212 | +---- |
| 213 | + |
| 214 | +==== Forensic Capture |
| 215 | + |
| 216 | +[source,elixir] |
| 217 | +---- |
| 218 | +{:crash, reason, forensics} = Munition.fire(wasm, "buggy_function", []) |
| 219 | +
|
| 220 | +# Serialize for offline analysis |
| 221 | +binary = Munition.Forensics.Dump.serialize(forensics) |
| 222 | +File.write!("crash_dump.mntn", binary) |
| 223 | +
|
| 224 | +# Extract insights |
| 225 | +analyser = Munition.Forensics.Analyser.new(forensics) |
| 226 | +strings = Munition.Forensics.Analyser.extract_strings(analyser) |
| 227 | +---- |
| 228 | + |
| 229 | +== Formal Specification |
| 230 | + |
| 231 | +Munition includes a formal TLA+ specification proving capability safety, termination, and forensic capture guarantees. See link:docs/capability_model.md[Capability Model] for: |
| 232 | + |
| 233 | +* Formal definitions (Source Language, Target Runtime, Attenuator) |
| 234 | +* Soundness and Completeness properties |
| 235 | +* Forensic Capture specification |
| 236 | +* Full TLA+ model |
| 237 | +* Soundness proof sketch |
| 238 | + |
| 239 | +=== Security Guarantees |
| 240 | + |
| 241 | +[cols="1,3"] |
| 242 | +|=== |
| 243 | +|Property |Guarantee |
| 244 | + |
| 245 | +|**Termination** |
| 246 | +|Fuel exhaustion guarantees all executions terminate |
| 247 | + |
| 248 | +|**Memory Safety** |
| 249 | +|WASM linear memory is bounds-checked |
| 250 | + |
| 251 | +|**Isolation** |
| 252 | +|No shared state between executions |
| 253 | + |
| 254 | +|**Capability Restriction** |
| 255 | +|Only explicitly granted capabilities are accessible |
| 256 | + |
| 257 | +|**Forensic Preservation** |
| 258 | +|All failures are captured atomically for audit |
| 259 | +|=== |
| 260 | + |
| 261 | +=== Non-Guarantees |
| 262 | + |
| 263 | +* Execution time is bounded but not constant (timing side-channels possible) |
| 264 | +* CPU cache timing attacks remain possible |
| 265 | +* Memory allocation before instantiation may exhaust host resources |
| 266 | +* Custom host functions must be implemented securely |
| 267 | + |
| 268 | +== Development |
| 269 | + |
| 270 | +=== Prerequisites |
| 271 | + |
| 272 | +* Elixir 1.14+ |
| 273 | +* Rust (for building test WASM modules) |
| 274 | +* https://github.com/casey/just[just] (task runner) |
| 275 | + |
| 276 | +=== Setup |
| 277 | + |
| 278 | +[source,bash] |
| 279 | +---- |
| 280 | +git clone https://github.com/hyperpolymath/chimichanga |
| 281 | +cd chimichanga |
| 282 | +
|
| 283 | +# Full setup (deps + WASM) |
| 284 | +just setup |
| 285 | +
|
| 286 | +# Or manually: |
| 287 | +mix deps.get |
| 288 | +cd test_wasm && cargo build --target wasm32-unknown-unknown --release |
| 289 | +mkdir -p test/fixtures |
| 290 | +cp test_wasm/target/wasm32-unknown-unknown/release/munition_test_wasm.wasm test/fixtures/test.wasm |
| 291 | +---- |
| 292 | + |
| 293 | +=== Testing |
| 294 | + |
| 295 | +[source,bash] |
| 296 | +---- |
| 297 | +just test # All tests |
| 298 | +just test-unit # Unit tests only (no WASM required) |
| 299 | +just test-integration # Integration tests only |
| 300 | +just test-coverage # With coverage report |
| 301 | +---- |
| 302 | + |
| 303 | +=== Code Quality |
| 304 | + |
| 305 | +[source,bash] |
| 306 | +---- |
| 307 | +just check # Run all checks (fmt, lint, dialyzer) |
| 308 | +just lint # Credo analysis |
| 309 | +just dialyzer # Type checking |
| 310 | +just validate # Full RSR Gold validation |
| 311 | +---- |
| 312 | + |
| 313 | +== Project Statistics |
| 314 | + |
| 315 | +[cols="1,1"] |
| 316 | +|=== |
| 317 | +|Metric |Value |
| 318 | + |
| 319 | +|Elixir Source |
| 320 | +|~1,955 lines (14 modules) |
| 321 | + |
| 322 | +|Test Suite |
| 323 | +|~380 lines (unit + integration) |
| 324 | + |
| 325 | +|Test WASM (Rust) |
| 326 | +|~286 lines |
| 327 | + |
| 328 | +|Documentation |
| 329 | +|40+ KB across 14 files |
| 330 | + |
| 331 | +|Version |
| 332 | +|0.1.0 (pre-release) |
| 333 | + |
| 334 | +|RSR Compliance |
| 335 | +|Gold |
| 336 | +|=== |
| 337 | + |
| 338 | +== Documentation |
| 339 | + |
| 340 | +* link:ARCHITECTURE.md[Architecture] - System design and execution flows |
| 341 | +* link:docs/capability_model.md[Capability Model] - Formal specification and proofs |
| 342 | +* link:CONTRIBUTING.adoc[Contributing] - Tri-Perimeter Contribution Framework |
| 343 | +* link:GOVERNANCE.adoc[Governance] - Decision-making model |
| 344 | +* link:SECURITY.md[Security] - Vulnerability reporting policy |
| 345 | +* link:REVERSIBILITY.md[Reversibility] - Safe operations commitment |
| 346 | +* link:ROADMAP.adoc[Roadmap] - Future development plans |
| 347 | + |
| 348 | +== License |
| 349 | + |
| 350 | +Dual-licensed under MIT OR MPL-2.0. |
| 351 | + |
| 352 | +See link:LICENSE.txt[LICENSE.txt] for details. |
| 353 | + |
| 354 | +== Maintainers |
| 355 | + |
| 356 | +See link:MAINTAINERS.md[MAINTAINERS.md] for the current maintainer list. |
| 357 | + |
| 358 | +--- |
| 359 | + |
| 360 | +_Maintained by https://github.com/hyperpolymath[Hyperpolymath]_ |
0 commit comments