From fc7c327e30beac7211a9cc53032214983a44c66e Mon Sep 17 00:00:00 2001 From: Ralf Anton Beier Date: Tue, 10 Mar 2026 17:55:45 +0100 Subject: [PATCH] safety: initial STPA analysis (losses, hazards) Adds system-theoretic process analysis for Synth as a WebAssembly-to-ARM AOT compiler. Covers 6 losses and 10 hazards (with 3 sub-hazards). Key areas: instruction selection correctness, bounds check generation, ARM encoding validity, control flow translation, register allocation, ELF generation, Meld dispatch ABI compatibility, and verification gap between proofs and implementation. Follows the same STPA schema as Meld (pulseengine/meld/safety/schema/stpa.schema.json). Co-Authored-By: Claude Opus 4.6 --- safety/stpa/hazards.yaml | 122 +++++++++++++++++++++++++++++++++++++++ safety/stpa/losses.yaml | 78 +++++++++++++++++++++++++ 2 files changed, 200 insertions(+) create mode 100644 safety/stpa/hazards.yaml create mode 100644 safety/stpa/losses.yaml diff --git a/safety/stpa/hazards.yaml b/safety/stpa/hazards.yaml new file mode 100644 index 0000000..516721f --- /dev/null +++ b/safety/stpa/hazards.yaml @@ -0,0 +1,122 @@ +# STPA Step 1b: System-Level Hazards +# +# System: Synth — WebAssembly-to-ARM Cortex-M AOT compiler + +hazards: + - id: H-1 + title: Instruction selection maps WASM op to semantically wrong ARM sequence + description: > + The pattern-matching instruction selector maps a WasmOp to an + ArmInstruction sequence that does not preserve the operation's + semantics. This includes wrong arithmetic (e.g., signed vs unsigned + shift), wrong comparison (e.g., condition code confusion), wrong + conversion (e.g., float-to-int truncation vs saturation), or + missing side effects (e.g., trap on division by zero). + losses: [L-1] + + - id: H-2 + title: Peephole optimization changes program semantics + description: > + The peephole optimizer transforms an instruction sequence in a way + that changes observable behavior. Constant propagation uses wrong + value, dead code elimination removes a side-effecting instruction, + instruction fusion changes evaluation order, or strength reduction + produces a different result for edge-case inputs. + losses: [L-1] + + - id: H-3 + title: Bounds check generation is incorrect or missing + description: > + Memory access instructions are compiled without bounds checks + (when --bounds-check is enabled), or the generated CMP/BHS + sequence uses the wrong memory size, wrong offset calculation, + or wrong branch target. Out-of-bounds access silently succeeds. + losses: [L-1, L-2] + + - id: H-4 + title: ARM encoding produces invalid machine code for target + description: > + The ARM encoder generates an instruction encoding that is invalid + for the target ISA variant. Thumb-2 encoding on Thumb-1-only core, + VFP instruction without FPU, unaligned LDR/STR without UAL support, + or incorrect condition code encoding. + losses: [L-5] + + - id: H-5 + title: Control flow translation loses structured control flow semantics + description: > + The block/loop/if/br/br_if translation to ARM labels and branches + produces incorrect branch targets. A br targets the wrong label, + a loop back-edge jumps to the wrong address, or an if/else branch + falls through to the wrong arm. + losses: [L-1] + + - id: H-6 + title: Register allocator corrupts live value + description: > + The register allocator spills or restores a value incorrectly, + overwrites a live register, or uses a register that is still needed + by a subsequent instruction. The virtual stack model diverges from + the physical register state. + losses: [L-1] + + - id: H-7 + title: ELF builder produces malformed binary + description: > + The ELF output has incorrect section headers, wrong program header + load addresses, incorrect symbol table entries, wrong relocations, + or a malformed vector table. The binary loads at the wrong address, + the reset handler jumps to wrong code, or the HardFault handler is + missing. + losses: [L-4, L-5] + + - id: H-8 + title: Meld dispatch ABI is misimplemented + description: > + The __meld_dispatch_import calling convention disagrees between + Synth (which generates the BL + relocation) and Kiln (which provides + the handler). Import index is placed in the wrong register, arguments + are in the wrong order, or the return value convention is wrong. + losses: [L-4] + + - id: H-9 + title: Verification gap between proven rules and actual codegen + description: > + A Rocq proof or Z3 check covers a specification of the rule, but + the Rust implementation diverges from that specification. The proof + assumes properties that the implementation does not guarantee. The + 52 Admitted proofs hide unsound assumptions. The OCaml-extracted + validator is not used in the production pipeline. + losses: [L-3] + + - id: H-10 + title: Canonical ABI lowering disagrees with Meld/Kiln + description: > + Synth's synth-abi crate computes different canonical ABI layouts + than Meld's parser.rs or Kiln's kiln-component. When a meld-fused + component is compiled by Synth, the compiled import dispatch + passes arguments with wrong offsets or sizes. + losses: [L-1, L-4] + +sub-hazards: + - id: H-1.1 + parent: H-1 + title: Float-to-int conversion uses wrong ARM instruction + description: > + VCVT vs VCVTR confusion, or missing saturation for wasm's + i32.trunc_sat_f32_s vs i32.trunc_f32_s semantics. + + - id: H-1.2 + parent: H-1 + title: Signed/unsigned confusion in shift or division + description: > + ASR used where LSR needed, or SDIV where UDIV needed, producing + wrong results for negative operands. + + - id: H-5.1 + parent: H-5 + title: Loop back-edge offset calculated incorrectly + description: > + The branch offset for a loop's back-edge is wrong because + instruction sizes were miscounted (ARM vs Thumb-2 encoding + widths vary per instruction). diff --git a/safety/stpa/losses.yaml b/safety/stpa/losses.yaml new file mode 100644 index 0000000..b82a27e --- /dev/null +++ b/safety/stpa/losses.yaml @@ -0,0 +1,78 @@ +# STPA Step 1a: Losses +# +# System: Synth — WebAssembly-to-ARM Cortex-M AOT compiler +# System boundary: Synth accepts .wasm/.wat files and produces bare-metal +# ARM ELF binaries. The system boundary includes parsing, instruction +# selection, peephole optimization, ARM encoding, and ELF generation. +# It excludes upstream tools (meld, loom), the runtime (kiln, gale), +# and hardware. +# +# Stakeholders: +# - Developers building safety-critical embedded systems +# - End-users of systems running Synth-compiled code +# - Certification authorities (ISO 26262, DO-178C, IEC 61508) +# - PulseEngine toolchain (Meld, Loom, Kiln, Gale, Sigil) +# +# Relation to BA RFC #46: Synth provides an alternative execution path +# to the RFC's runtime-based approach. Where the RFC proposes a +# core module running on a host runtime, Synth compiles directly to +# native ARM code with __meld_dispatch_import for Kiln bridge calls. +# This eliminates the runtime interpretation overhead but shifts +# correctness responsibility to the compiler. + +losses: + - id: L-1 + title: Loss of compilation correctness + description: > + The compiled ARM code produces different results than the WebAssembly + specification requires. Instructions compute wrong values, control + flow diverges, or traps are missing/spurious. The compiled program + silently computes incorrect results on the target hardware. + stakeholders: [developers, end-users, certification-authorities] + + - id: L-2 + title: Loss of memory safety in compiled code + description: > + The compiled ARM code accesses memory outside the WebAssembly linear + memory bounds. Bounds checks are missing, incorrectly generated, or + optimized away. Stack overflow in compiled code corrupts adjacent + memory. MPU regions are misconfigured for the compiled binary. + stakeholders: [developers, end-users, certification-authorities] + + - id: L-3 + title: Loss of verification validity + description: > + The Z3 SMT validation or Rocq proofs do not cover the actual code + path executed. A rule is proven correct but the implementation + diverges from the proven specification. Admitted proofs hide + unsound assumptions. The OCaml-extracted validator disagrees with + the Rust implementation. + stakeholders: [certification-authorities, developers] + + - id: L-4 + title: Loss of ABI compatibility + description: > + The generated ELF binary uses a calling convention, memory layout, + or import dispatch mechanism that is incompatible with the Kiln + runtime bridge. The __meld_dispatch_import ABI is misimplemented. + Relocations are incorrect. The vector table is malformed. + stakeholders: [developers, end-users] + + - id: L-5 + title: Loss of target fidelity + description: > + The generated ARM instructions are invalid for the target core + (e.g., Thumb-2 instruction on Cortex-M0 which only supports Thumb-1, + VFP instruction on core without FPU, unaligned access on strict- + alignment core). The binary crashes or produces wrong results on + the physical hardware despite passing emulation tests. + stakeholders: [developers, end-users] + + - id: L-6 + title: Loss of build reproducibility + description: > + Identical .wasm input produces different ARM ELF output across + builds, machines, or compiler versions. Non-determinism in + instruction selection, register allocation, or ELF layout breaks + hermetic build guarantees. + stakeholders: [developers, certification-authorities]