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]