diff --git a/CLAUDE.md b/CLAUDE.md index 70481ee1..c74e9f75 100644 --- a/CLAUDE.md +++ b/CLAUDE.md @@ -482,6 +482,18 @@ The Kiln project has completed its migration to a unified build system: - **Integration**: Former kiln-verification-tool functionality integrated into kiln-build-core - **API consistency**: All commands follow consistent patterns and error handling +### Post-RFC #46 Architecture (Current) +The PulseEngine toolchain follows BA RFC #46 for component model support: + +- **Meld** lowers components to core modules at build time +- **Kiln interpreter** (std-only) executes core modules + host intrinsics +- **kiln-builtins** (no_std) provides host intrinsics for synth-compiled code +- **Synth** compiles to native ELF for gale/embedded targets +- Component Model is NOT implemented as a runtime feature — Meld handles it + +The interpreter is std-only. The no_std path is via kiln-builtins for synth-compiled code. +See `docs/architecture/rfc46-toolchain-architecture.md` for details. + ### Removed Legacy Components - Shell scripts: `verify_build.sh`, `fuzz_all.sh`, `verify_no_std.sh`, `test_features.sh`, `documentation_audit.sh` - Kani verification scripts: `test_kani_phase4.sh`, `validate_kani_phase4.sh` diff --git a/docs/COMPONENT_MODEL_IMPLEMENTATION_PLAN.md b/docs/COMPONENT_MODEL_IMPLEMENTATION_PLAN.md deleted file mode 100644 index 9f975509..00000000 --- a/docs/COMPONENT_MODEL_IMPLEMENTATION_PLAN.md +++ /dev/null @@ -1,632 +0,0 @@ -# WebAssembly Component Model Implementation Plan - -## Executive Summary - -This document provides a comprehensive implementation plan for proper Component Model support in Kiln. The current implementation is **Flickschusterei** (patchwork) - infrastructure exists but execution paths are hollow. Hello World works only because it uses primitives that bypass the Component Model entirely. - -### Current State Assessment - -| Component | Status | Reality | -|-----------|--------|---------| -| Canonical ABI (lift/lower) | EXISTS | **NEVER CALLED** - execution bypasses it | -| Component Instantiation | EXISTS | Core modules run directly, no component linking | -| Type Validation | EXISTS | Infrastructure defined, never validates at call boundaries | -| Resource System | EXISTS | Just integer tags, no ownership semantics | -| Component Linking | EXISTS | Components don't link - imports resolve to stubs | - -### Why Hello World Works - -The hello-world component prints successfully because: -1. `wasi:cli/stdout.get-stdout` returns primitive i32 (handle) -2. `wasi:io/streams.blocking-write-and-flush` takes primitive i32 args (handle, ptr, len) -3. All types are primitives that map directly to core WASM values -4. NO lift/lower operations needed for primitives - -**ANY component using strings, lists, records, variants, or resources will fail.** - ---- - -## Phase 1: Canonical ABI Integration into Execution Path - -**Goal**: Route all component function calls through proper lift/lower operations. - -### 1.1 Current Problem - -In `kiln-runtime/src/stackless/engine.rs`, WASI calls are dispatched directly: -```rust -// Line ~3397 -wasip2_host.dispatch(module_name, field_name, args, Some(&mut mem_buffer)) -``` - -This bypasses `CanonicalExecutor::execute_canon_lower()` entirely. The `args` here are already `Value::I32` pulled from the WASM stack - not `ComponentValue` types. - -### 1.2 Required Changes - -#### Step 1: Create Canonical Call Context -```rust -// New file: kiln-runtime/src/canonical_call.rs -pub struct CanonicalCallContext<'a> { - pub memory: &'a mut [u8], - pub realloc: Option, // realloc function index - pub post_return: Option, - pub string_encoding: StringEncoding, -} - -pub struct CanonicalCall { - pub interface: String, - pub function: String, - pub param_types: Vec, - pub result_types: Vec, -} -``` - -#### Step 2: Modify Import Dispatch in stackless/engine.rs - -**Before** (current): -```rust -fn execute_import(&mut self, ...) { - // Pull values from WASM stack - let args = self.pop_values(param_count); - // Call WASI directly - wasip2_host.dispatch(module_name, field_name, args, memory) -} -``` - -**After** (proposed): -```rust -fn execute_import(&mut self, ...) { - // 1. Get canonical function definition for this import - let canon_def = self.get_canonical_definition(module_name, field_name)?; - - // 2. Pull core WASM values from stack - let core_values = self.pop_values(canon_def.core_param_count); - - // 3. LIFT: Convert core values to component values using Canonical ABI - let component_values = self.canonical_abi.lift_values( - &canon_def.param_types, - &core_values, - self.memory.as_ref(), - )?; - - // 4. Dispatch to host - let results = wasip2_host.dispatch(module_name, field_name, component_values, memory)?; - - // 5. LOWER: Convert component results back to core values - let core_results = self.canonical_abi.lower_values( - &canon_def.result_types, - &results, - self.memory.as_mut(), - )?; - - // 6. Push results to WASM stack - self.push_values(&core_results); -} -``` - -#### Step 3: Implement lift_values/lower_values - -The `CanonicalABI` struct in `kiln-component/src/canonical_abi/canonical_abi.rs` has individual `lift_*` and `lower_*` methods, but needs batch operations: - -```rust -impl CanonicalABI { - /// Lift multiple core values to component values - pub fn lift_values( - &self, - types: &[ComponentType], - core_values: &[Value], - memory: &M, - ) -> Result> { - // For primitives: direct conversion - // For strings/lists: read ptr+len from stack, lift from memory - // For records: read field offsets, lift each field - // etc. - } - - /// Lower multiple component values to core values - pub fn lower_values( - &self, - types: &[ComponentType], - component_values: &[ComponentValue], - memory: &mut M, - ) -> Result> { - // For primitives: direct conversion - // For strings/lists: call realloc, write to memory, return ptr+len - // etc. - } -} -``` - -### 1.3 Files to Modify - -| File | Changes | -|------|---------| -| `kiln-runtime/src/stackless/engine.rs` | Add canonical call integration at import dispatch | -| `kiln-component/src/canonical_abi/canonical_abi.rs` | Add `lift_values`, `lower_values` batch methods | -| `kiln-component/src/canonical_executor.rs` | Implement `execute_canon_lift` properly | -| `kiln-runtime/src/wasip2_host.rs` | Accept `ComponentValue` instead of `Value` | - -### 1.4 Test Cases - -1. **String Parameter Test**: Component that calls `wasi:filesystem/preopens.get-directories()` which returns `list>` -2. **String Return Test**: Component that exports a function returning a string -3. **Record Test**: Component using `wasi:http/types.fields` which uses records - ---- - -## Phase 2: Component Linking Infrastructure - -**Goal**: Enable components to import from other components, not just host functions. - -### 2.1 Current Problem - -The `ComponentLinker` in `kiln-component/src/components/component_instantiation.rs` defines structures but: -- `instantiate()` creates standalone instances -- No instance-to-instance linking -- All imports resolve to host or fail - -### 2.2 Required Changes - -#### Step 1: Instance Registry with Export Mapping - -```rust -pub struct ComponentRegistry { - instances: HashMap, - exports: HashMap<(InstanceId, String), ExportDefinition>, - instance_order: Vec, // Topological order for initialization -} - -impl ComponentRegistry { - /// Register an export that can satisfy imports - pub fn register_export( - &mut self, - instance: InstanceId, - name: &str, - export: ExportDefinition, - ) -> Result<()>; - - /// Find which instance provides a given import - pub fn resolve_import( - &self, - module: &str, - name: &str, - ) -> Result<(InstanceId, ExportDefinition)>; -} -``` - -#### Step 2: Cross-Instance Function Calls - -When a component calls an imported function that's provided by another component: - -```rust -fn execute_component_import(&mut self, import: &ResolvedImport) -> Result> { - // 1. Get target instance - let target = self.registry.get_instance(import.provider_id)?; - - // 2. Get target function - let func = target.get_export(&import.provider_export)?; - - // 3. Marshal arguments (lift from caller, lower to callee) - let callee_args = self.marshal_args_to_callee( - &self.current_memory(), - &target.memory(), - &args, - &func.param_types, - )?; - - // 4. Execute in target context - let results = self.execute_in_context(target, func, callee_args)?; - - // 5. Marshal results back (lift from callee, lower to caller) - let caller_results = self.marshal_results_to_caller( - &target.memory(), - &self.current_memory(), - &results, - &func.result_types, - )?; - - Ok(caller_results) -} -``` - -### 2.3 Instantiation Order - -Components must be instantiated in dependency order: - -```rust -impl ComponentRegistry { - pub fn instantiate_all(&mut self, components: &[ComponentBinary]) -> Result<()> { - // 1. Build dependency graph - let deps = self.build_dependency_graph(components)?; - - // 2. Topological sort - let order = topological_sort(&deps)?; - - // 3. Instantiate in order - for component_id in order { - let component = &components[component_id]; - - // Resolve imports from already-instantiated components - let imports = self.resolve_imports(component)?; - - // Create instance - let instance = self.create_instance(component, imports)?; - - // Register exports for later components - self.register_exports(instance)?; - } - - Ok(()) - } -} -``` - -### 2.4 Files to Modify - -| File | Changes | -|------|---------| -| `kiln-component/src/components/component_instantiation.rs` | Implement `ComponentRegistry` | -| `kiln-component/src/components/component_linker.rs` | Add dependency resolution | -| `kiln-runtime/src/stackless/engine.rs` | Add cross-instance dispatch | - ---- - -## Phase 3: Resource System (own, borrow) - -**Goal**: Implement proper resource ownership and borrowing semantics. - -### 3.1 Current Problem - -Resources are just u32 handles with no ownership tracking: -```rust -// Current implementation in kiln-component/src/resource_management.rs -pub struct ResourceHandle(pub u32); -``` - -This allows: -- Using a dropped resource (use-after-free) -- Leaking resources (no automatic cleanup) -- Borrowing from a dropped owner (dangling borrow) - -### 3.2 Required Changes - -#### Step 1: Resource Table per Component Instance - -```rust -/// Resource entry with ownership information -pub struct ResourceEntry { - /// Resource type ID - pub type_id: ResourceTypeId, - /// The actual representation (impl-defined) - pub rep: u32, - /// Is this an owned handle or borrowed? - pub is_owned: bool, - /// For owned: number of active borrows - pub borrow_count: u32, - /// For borrowed: the owning handle - pub owner: Option, - /// For borrowed: the task/scope that created the borrow - pub borrow_scope: Option, -} - -pub struct ResourceTable { - entries: Vec>, - free_list: Vec, -} -``` - -#### Step 2: Canonical Built-ins - -```rust -impl ResourceTable { - /// canon resource.new - create a new owned resource - pub fn resource_new(&mut self, type_id: ResourceTypeId, rep: u32) -> ResourceHandle { - let entry = ResourceEntry { - type_id, - rep, - is_owned: true, - borrow_count: 0, - owner: None, - borrow_scope: None, - }; - self.allocate(entry) - } - - /// canon resource.drop - drop an owned resource - pub fn resource_drop(&mut self, handle: ResourceHandle) -> Result { - let entry = self.get_mut(handle)?; - - // Cannot drop if borrows exist - if entry.borrow_count > 0 { - return Err(Error::resource_error("Cannot drop resource with active borrows")); - } - - if !entry.is_owned { - return Err(Error::resource_error("Cannot drop borrowed resource")); - } - - let rep = entry.rep; - self.deallocate(handle); - Ok(rep) - } - - /// Create a borrow from an owned resource - pub fn borrow(&mut self, owner: ResourceHandle, scope: TaskId) -> Result { - let owner_entry = self.get_mut(owner)?; - - if !owner_entry.is_owned { - return Err(Error::resource_error("Cannot borrow from borrowed resource")); - } - - owner_entry.borrow_count += 1; - - let borrow_entry = ResourceEntry { - type_id: owner_entry.type_id, - rep: owner_entry.rep, - is_owned: false, - borrow_count: 0, - owner: Some(owner), - borrow_scope: Some(scope), - }; - - Ok(self.allocate(borrow_entry)) - } - - /// End a borrow (called when borrow scope ends) - pub fn end_borrow(&mut self, handle: ResourceHandle) -> Result<()> { - let entry = self.get(handle)?; - - if entry.is_owned { - return Err(Error::resource_error("Cannot end borrow on owned resource")); - } - - let owner = entry.owner.ok_or_else(|| Error::resource_error("Borrow missing owner"))?; - - self.deallocate(handle); - - // Decrement owner's borrow count - let owner_entry = self.get_mut(owner)?; - owner_entry.borrow_count -= 1; - - Ok(()) - } -} -``` - -#### Step 3: Integrate with Canonical ABI - -When lifting/lowering resource handles: - -```rust -impl CanonicalABI { - pub fn lift_own( - &self, - memory: &M, - offset: u32, - resource_table: &mut ResourceTable, - ) -> Result { - let handle_value = memory.read_u32_le(offset)?; - let handle = ResourceHandle(handle_value); - - // Validate the handle exists and is owned - let entry = resource_table.get(handle)?; - if !entry.is_owned { - return Err(Error::resource_error("Expected owned resource")); - } - - Ok(handle) - } - - pub fn lower_borrow( - &self, - memory: &mut M, - offset: u32, - handle: ResourceHandle, - scope: TaskId, - resource_table: &mut ResourceTable, - ) -> Result<()> { - // Create a borrow for the callee's scope - let borrow_handle = resource_table.borrow(handle, scope)?; - memory.write_u32_le(offset, borrow_handle.0) - } -} -``` - -### 3.3 Files to Modify - -| File | Changes | -|------|---------| -| `kiln-component/src/resource_management.rs` | Implement `ResourceTable` with ownership | -| `kiln-component/src/canonical_abi/canonical_abi.rs` | Add `lift_own`, `lift_borrow`, `lower_own`, `lower_borrow` | -| `kiln-runtime/src/wasip2_host.rs` | Use resource table for WASI handles | - ---- - -## Phase 4: Multi-Component Composition - -**Goal**: Support composing multiple components with proper type checking. - -### 4.1 Current Problem - -Components are treated as standalone. No composition: -- No WIT type compatibility checking -- No interface matching -- No component graph management - -### 4.2 Required Changes - -#### Step 1: WIT Type Registry - -```rust -/// Registry of component types for validation -pub struct TypeRegistry { - /// Named interfaces - interfaces: HashMap, - /// Type definitions - types: HashMap, -} - -pub struct InterfaceDefinition { - pub name: String, - pub version: Version, - pub types: HashMap, - pub functions: HashMap, -} -``` - -#### Step 2: Import/Export Type Checking - -```rust -impl ComponentLinker { - /// Validate that an export satisfies an import - fn check_type_compatibility( - &self, - import: &ImportDefinition, - export: &ExportDefinition, - ) -> Result<()> { - match (import, export) { - (ImportDefinition::Function(import_fn), ExportDefinition::Function(export_fn)) => { - // Check parameter types match - if import_fn.params.len() != export_fn.params.len() { - return Err(Error::type_error("Parameter count mismatch")); - } - - for (imp, exp) in import_fn.params.iter().zip(export_fn.params.iter()) { - self.check_subtype(exp, imp)?; // contravariance - } - - // Check return types match - for (imp, exp) in import_fn.results.iter().zip(export_fn.results.iter()) { - self.check_subtype(imp, exp)?; // covariance - } - - Ok(()) - } - _ => Err(Error::type_error("Import/export kind mismatch")) - } - } -} -``` - -#### Step 3: Component Composition DSL - -```rust -/// Builder for component composition -pub struct CompositionBuilder { - components: HashMap, - links: Vec, -} - -pub struct Link { - pub from_component: String, - pub from_export: String, - pub to_component: String, - pub to_import: String, -} - -impl CompositionBuilder { - pub fn add_component(&mut self, name: &str, binary: &[u8]) -> Result<&mut Self>; - pub fn link(&mut self, link: Link) -> Result<&mut Self>; - pub fn build(&self) -> Result; -} -``` - -### 4.3 Files to Create/Modify - -| File | Changes | -|------|---------| -| `kiln-component/src/wit/type_registry.rs` | NEW: Type registry | -| `kiln-component/src/wit/compatibility.rs` | NEW: Type compatibility checking | -| `kiln-component/src/composition.rs` | NEW: Composition builder | -| `kiln-component/src/components/component_linker.rs` | Integrate type checking | - ---- - -## Implementation Order and Dependencies - -``` -Phase 1 (Canonical ABI Integration) - │ - ├── 1.1 Batch lift/lower operations - ├── 1.2 Call context with realloc - └── 1.3 Integration into stackless/engine.rs - │ - v -Phase 2 (Component Linking) - │ - ├── 2.1 Instance registry - ├── 2.2 Cross-instance calls - └── 2.3 Dependency ordering - │ - v -Phase 3 (Resource System) - │ - ├── 3.1 Resource table - ├── 3.2 own/borrow semantics - └── 3.3 Integration with ABI - │ - v -Phase 4 (Multi-Component Composition) - │ - ├── 4.1 Type registry - ├── 4.2 Compatibility checking - └── 4.3 Composition builder -``` - ---- - -## Verification Milestones - -### Milestone 1: String Support -- [ ] Component can receive a string parameter from host -- [ ] Component can return a string to host -- [ ] String encoding (UTF-8) is correctly handled - -### Milestone 2: List Support -- [ ] Component can receive a list parameter -- [ ] Component can return a list -- [ ] Nested lists work correctly - -### Milestone 3: Record/Variant Support -- [ ] Component can use records in function signatures -- [ ] Component can use variants (enums with payloads) -- [ ] Option and Result types work correctly - -### Milestone 4: Resource Ownership -- [ ] `own` correctly transfers ownership -- [ ] `borrow` correctly creates borrows -- [ ] Dropped borrows decrement owner count -- [ ] Cannot drop owner while borrows exist - -### Milestone 5: Component Linking -- [ ] Component A can import function from Component B -- [ ] Dependency order is respected -- [ ] Type checking prevents mismatched links - -### Milestone 6: Full WASI Preview 2 -- [ ] wasi:filesystem works (uses strings, records, resources) -- [ ] wasi:http works (complex types) -- [ ] wasi:sockets works (complex types) - ---- - -## Risk Assessment - -| Risk | Impact | Mitigation | -|------|--------|------------| -| Breaking existing hello-world | HIGH | Keep primitive passthrough, add lift/lower for complex types | -| Performance regression | MEDIUM | Optimize primitive case to avoid unnecessary conversions | -| Memory allocation in lift/lower | MEDIUM | Use realloc properly, pool allocations | -| Complex type edge cases | HIGH | Extensive testing with real WASI components | - ---- - -## Conclusion - -The current Kiln Component Model implementation is a facade. Making it real requires: - -1. **Route all calls through Canonical ABI** - not just documentation, actual execution -2. **Implement component linking** - instances resolving imports from other instances -3. **Real resource ownership** - not just integer tags -4. **Type validation** - at link time and call time - -This plan provides a roadmap to transform the existing infrastructure into a working Component Model implementation. diff --git a/docs/architecture/rfc46-toolchain-architecture.md b/docs/architecture/rfc46-toolchain-architecture.md new file mode 100644 index 00000000..547acaa0 --- /dev/null +++ b/docs/architecture/rfc46-toolchain-architecture.md @@ -0,0 +1,140 @@ +# RFC #46 Toolchain Architecture + +BA RFC #46 defines how the PulseEngine toolchain handles WebAssembly Component Model support. The key principle is that component model complexity is resolved at **build time** by Meld, not at runtime by Kiln. + +## Toolchain Overview + +``` + Build Time Runtime + +-----------------+ +---------------------+ + .wasm/.wit | | core .wasm| | + components ----> Meld +----------->| Kiln interpreter | (std) + | (lower to core)| | + host intrinsics | + +-----------------+ +---------------------+ + | + | core .wasm + v + +-----------------+ +---------------------+ + | | native ELF| | + | Synth +----------->| gale / embedded | (no_std) + | (AOT compile) | | + kiln-builtins | + +-----------------+ +---------------------+ +``` + +## Components + +### Meld (Build Time) + +Meld lowers Component Model constructs to core WebAssembly modules at build time. This includes: + +- Resolving component imports and exports to core-level wiring +- Performing canonical ABI lift/lower transformations statically +- Fusing multi-component graphs into a single core module (or a set of core modules with a known linking protocol) +- Resolving WIT interface types to concrete core value types + +After Meld processing, the output is one or more **core WebAssembly modules** with no Component Model constructs remaining. Host/WASI imports that cannot be resolved statically are preserved as core-level imports. + +### Kiln Interpreter (std-only, Runtime) + +The Kiln interpreter executes **core WebAssembly modules**. It does not interpret Component Model constructs at runtime. Its responsibilities: + +- Decode and validate core WebAssembly binary format +- Interpret core instructions (MVP through Wasm 3.0 proposals) +- Manage linear memory, tables, globals +- Dispatch host function imports (WASI, custom host functions) +- Enforce fuel metering, memory budgets, and call depth limits +- Provide CFI (Control Flow Integrity) validation + +The interpreter requires `std` (heap allocation, I/O for WASI, threads for shared memory). There is no `no_std` interpreter. + +### kiln-builtins (no_std, Runtime) + +`kiln-builtins` provides host intrinsics for code that Synth has compiled to native. This crate is `no_std` compatible and runs on bare-metal / RTOS targets. It provides: + +- WASI host function implementations suitable for embedded (clocks, random, minimal I/O) +- Memory management intrinsics (linear memory bounds checking, table access) +- Trap handling and fault isolation primitives +- The C ABI surface that Synth-compiled ELF binaries call into + +`kiln-builtins` does **not** contain a WebAssembly interpreter. It only provides the runtime support library for natively compiled code. + +### Synth (Build Time) + +Synth compiles core WebAssembly modules to native ELF binaries for gale and other embedded targets. Its input is the core module output from Meld (or a standalone core module). Synth: + +- Translates core Wasm instructions to native machine code (ARM, RISC-V, x86-64) +- Generates calls to `kiln-builtins` for host intrinsics +- Produces position-independent ELF objects linkable into gale firmware images +- Applies platform-specific optimizations (register allocation, instruction scheduling) + +### gale (Runtime, Embedded) + +The gale RTOS loads and executes Synth-compiled ELF binaries. At runtime, gale provides: + +- Task scheduling for Wasm-derived tasks +- Hardware abstraction (MPU, interrupt routing) +- The `kiln-builtins` library linked into the firmware image + +## Three Execution Paths + +### 1. std Path (Interpreter) + +``` +Component (.wasm) --> Meld --> Core module (.wasm) --> Kiln interpreter (std) +``` + +Used for: development, testing, server-side execution, CI. The Kiln interpreter runs the core module directly with full WASI support and dynamic memory allocation. + +### 2. Embedded Path (Synth + gale) + +``` +Component (.wasm) --> Meld --> Core module (.wasm) --> Synth --> ELF --> gale + kiln-builtins +``` + +Used for: safety-critical embedded targets (ASIL-B through ASIL-D). No interpreter at runtime. All WebAssembly semantics are compiled to native code. `kiln-builtins` provides the minimal runtime support. + +### 3. Direct Core Module Path + +``` +Core module (.wasm) --> Kiln interpreter (std) + --> Synth --> ELF --> gale + kiln-builtins +``` + +Used for: core modules that were never components (e.g., hand-written WAT, third-party core-only modules). Meld is skipped entirely since there are no Component Model constructs to lower. + +## What Kiln Does NOT Do + +- **Full Component Model runtime**: Kiln does not implement component instantiation, canonical ABI lift/lower, or component-level linking at runtime. Meld handles all of this at build time. +- **Canonical ABI at runtime**: There is no runtime canonical ABI encoder/decoder in the interpreter. Values cross the host boundary as core Wasm types (i32, i64, f32, f64, references). +- **Async model**: The Component Model async proposal (streams, futures, subtask scheduling) is not implemented in the Kiln interpreter. Async coordination, if needed, is handled by Meld's lowering or by the host application. +- **no_std interpreter**: There is no `no_std` WebAssembly interpreter. The `no_std` execution path is exclusively through Synth-compiled native code with `kiln-builtins`. +- **Component-to-component runtime linking**: Multiple components communicating at runtime are fused by Meld at build time into core modules with direct call wiring. Kiln does not perform dynamic component linking. + +## Formal Verification Strategy + +### Verus / Kani for kiln-builtins + +`kiln-builtins` is the trusted computing base for the embedded path. It is small, `no_std`, and has a well-defined interface. Formal verification targets: + +- **Memory bounds checking**: Prove that all linear memory accesses through builtins are within allocated bounds (Kani bounded model checking) +- **Trap semantics**: Prove that trap conditions produce correct fault signals, never silent corruption +- **ABI contract**: Verify that the C ABI surface matches what Synth generates (Kani harnesses for representative call patterns) +- **Verus proofs**: For critical arithmetic and state machine logic in builtins (e.g., fuel accounting, capability checks) + +### WAST Conformance for Interpreter + +The Kiln interpreter is validated against the official WebAssembly specification test suite: + +- All WAST test files from the WebAssembly spec repository (excluding legacy exception handling) +- Proposal-specific test suites for enabled proposals (GC, memory64, multi-memory, exception handling, etc.) +- Custom regression tests for edge cases discovered during development + +### Rocq for Specification + +A shared Rocq (Coq) formal specification defines the canonical ABI element sizing, alignment, and string encoding rules. This specification is the single source of truth that Meld, Kiln, and Synth must all agree on: + +- `canonical_abi_element_size` for all component value types +- `align_up` and field layout computation for records and variants +- String transcoding rules (UTF-8, UTF-16, Latin-1 boundaries) + +The Rocq proofs establish that these functions satisfy the WebAssembly Component Model specification. Each tool extracts or reimplements these functions and validates agreement via shared test fixtures. diff --git a/safety/requirements/safety-requirements.yaml b/safety/requirements/safety-requirements.yaml index 3c2565c6..2fb45922 100644 --- a/safety/requirements/safety-requirements.yaml +++ b/safety/requirements/safety-requirements.yaml @@ -101,7 +101,8 @@ artifacts: Any opcode or opcode prefix+suffix combination not defined in the WebAssembly spec shall cause an immediate trap. The default match arm in opcode dispatch shall return Err, not Ok. - status: draft + status: delegated + delegation-note: "Canonical ABI delegated to Meld per BA RFC #46" tags: [execution, correctness, stpa-derived] links: - type: derives-from @@ -122,7 +123,8 @@ artifacts: Maximum call depth shall be checked before call, call_indirect, call_ref, and return_call instructions. The check shall measure actual call depth (not frame count) to correctly handle tail calls. - status: partial + status: delegated + delegation-note: "Canonical ABI delegated to Meld per BA RFC #46" tags: [execution, stack-safety, asil-d, stpa-derived] links: - type: derives-from @@ -145,7 +147,8 @@ artifacts: In multi-memory modules, every memory instruction's memory index operand shall be validated against the module's declared memory count. Invalid indices shall trap. The engine shall not default to memory 0. - status: draft + status: delegated + delegation-note: "Canonical ABI delegated to Meld per BA RFC #46" tags: [execution, memory-safety, stpa-derived] links: - type: derives-from @@ -167,7 +170,8 @@ artifacts: The decoder shall reject modules with duplicate sections, out-of-order sections, invalid LEB128 encodings, and all other malformation checks defined in the WebAssembly spec. - status: partial + status: delegated + delegation-note: "Canonical ABI delegated to Meld per BA RFC #46" tags: [decoder, validation, asil-d, stpa-derived] links: - type: derives-from @@ -191,7 +195,8 @@ artifacts: Decoder shall check configured resource limits before allocating structures for types, functions, memories, tables, globals, and elements. The limit check shall occur before the allocation, not after. - status: partial + status: delegated + delegation-note: "Canonical ABI delegated to Meld per BA RFC #46" tags: [decoder, resource-containment, asil-d, stpa-derived] links: - type: derives-from @@ -219,7 +224,8 @@ artifacts: sequences), UTF-16 (including surrogate pairs), and Latin-1. Multi-byte characters shall not be split across buffer boundaries. Code unit counts shall match the encoding. - status: draft + status: delegated + delegation-note: "Canonical ABI delegated to Meld per BA RFC #46" tags: [component-model, canonical-abi, strings, stpa-derived] links: - type: derives-from @@ -241,7 +247,8 @@ artifacts: Record field offsets shall be computed using align_up(current_offset, field_alignment) as defined in the canonical ABI spec. The align_up function shall be: align_up(x, a) = (x + a - 1) & !(a - 1). - status: draft + status: delegated + delegation-note: "Canonical ABI delegated to Meld per BA RFC #46" tags: [component-model, canonical-abi, alignment, stpa-derived] links: - type: derives-from @@ -262,7 +269,8 @@ artifacts: List element size shall be computed as align_up(sum_of_field_sizes, max_alignment). This shall match Meld's canonical_abi_element_size() for all type families. Disagreement is a blocking defect. - status: draft + status: delegated + delegation-note: "Canonical ABI delegated to Meld per BA RFC #46" tags: [component-model, canonical-abi, cross-toolchain, stpa-derived] links: - type: derives-from @@ -795,6 +803,11 @@ artifacts: usize (on 32-bit targets) is permitted. On 32-bit no_std targets, the effective addressable memory64 range shall be limited to the target's address space and clearly documented. + rationale: > + Per BA RFC #46, the no_std path is via kiln-builtins for synth-compiled + code, not the interpreter. Memory64 safety constraints apply to the + kiln-builtins host intrinsics that manage linear memory on behalf of + synth-compiled modules. status: planned tags: [no-std, memory-safety, memory64, asil-d, stpa-derived] traced_to: [H-2, H-3, H-7] @@ -826,6 +839,11 @@ artifacts: pool capacity shall be configurable via the resource budget system (safe_managed_alloc! integration). Circular references shall be documented as a known limitation in no_std mode. + rationale: > + Per BA RFC #46, the no_std path is via kiln-builtins for synth-compiled + code, not the interpreter. GC reference safety constraints apply to + kiln-builtins allocations backing GC heap objects in synth-compiled + modules. status: planned tags: [no-std, memory-safety, gc, asil-c, stpa-derived] traced_to: [H-1, H-3, H-7] @@ -910,6 +928,63 @@ artifacts: depth limit prevents unbounded recursion from GC init operations; budget configuration API validated at initialization time + # ========================================================================= + # RFC #46 Architecture — ABI and Compatibility + # ========================================================================= + - id: SR-BUILTIN-ABI + type: requirement + title: Kiln builtins must maintain stable ABI for synth-compiled code + description: > + All kiln-builtins host intrinsic functions shall have stable, versioned + ABI signatures. Changes to parameter types, return types, or calling + convention shall require a version bump and coordinated update with + Meld and Synth. The ABI shall be documented in a machine-readable + format (e.g., WIT or C header) that Meld and Synth consume at build + time. ABI-breaking changes without version coordination shall be + detected by integration tests. + status: draft + tags: [builtins, abi-stability, cross-toolchain, rfc46, stpa-derived] + links: + - type: derives-from + target: H-13 + - type: derives-from + target: LS-RF46-1 + - type: derives-from + target: LS-RF46-2 + fields: + implementation: kiln-builtins/ + verification-method: test, analysis + verification-description: > + Integration tests compile a Meld-fused module and execute it against + kiln-builtins; ABI signature registry compared between Meld output + and kiln-builtins declarations; CI fails on signature mismatch + + - id: SR-MELD-COMPAT + type: requirement + title: Kiln must validate Meld-fused module format before execution + description: > + Before executing a Meld-fused core module, Kiln shall validate that + the module's host intrinsic imports match the expected signatures + provided by kiln-builtins or the interpreter's host import handler. + Signature mismatches shall produce a clear error at load time, not + a silent failure or trap at call time. The validation shall cover + function parameter count, parameter types, and return types for + all host intrinsic imports. + status: draft + tags: [validation, meld-compat, cross-toolchain, rfc46, stpa-derived] + links: + - type: derives-from + target: H-13 + - type: derives-from + target: LS-RF46-1 + fields: + implementation: kiln-runtime/src/module_loading.rs + verification-method: test + verification-description: > + Module with mismatched host intrinsic signature is rejected at load + time with descriptive error; valid Meld-fused modules load and + execute successfully + # ========================================================================= # REMOVED from sphinx-needs (with rationale): # diff --git a/safety/stpa-sec/security-hazards.yaml b/safety/stpa-sec/security-hazards.yaml index 867d9b10..074240d7 100644 --- a/safety/stpa-sec/security-hazards.yaml +++ b/safety/stpa-sec/security-hazards.yaml @@ -60,26 +60,30 @@ security-hazards: sound and complete. Incomplete checks enable type confusion. - id: SH-3 - title: Resource exhaustion via unbounded GC allocation in no_std + title: Resource exhaustion via unbounded GC allocation in kiln-builtins description: > - In no_std mode, GC heap objects are allocated from the bounded - allocation pool but never reclaimed (no garbage collector). An - adversary crafts a module that allocates struct/array objects in - a tight loop without ever dropping references. The bounded pool - is exhausted, causing all subsequent allocation attempts (including - those by the runtime for call frames, tables, and other internal - data) to fail. This is a denial-of-service attack that can prevent - safety-critical code from executing. + In the kiln-builtins no_std runtime support library, GC heap objects + are allocated from the bounded allocation pool but never reclaimed + (no garbage collector). An adversary crafts a module that, after + Synth compilation and execution on gale, allocates struct/array + objects in a tight loop without ever dropping references. The bounded + pool is exhausted, causing all subsequent allocation attempts + (including those by kiln-builtins for host intrinsic state, tables, + and other internal data) to fail. This is a denial-of-service attack + that can prevent safety-critical code from executing on embedded + targets. security-losses: [SL-2] safety-hazards: [H-12, H-3] attack-vector: > Module contains: (func (loop (struct.new $large_struct) (br 0))) - where $large_struct has many fields. Each iteration allocates without - possibility of reclamation. + where $large_struct has many fields. After Synth compilation, each + iteration allocates from kiln-builtins pool without possibility of + reclamation. exploitability: high rationale: > - GC allocation shares the same pool as runtime internals. Pool - exhaustion is trivially achievable by an adversary in no_std mode. + GC allocation in kiln-builtins shares the same pool as runtime + intrinsic state. Pool exhaustion is trivially achievable by an + adversary in the embedded execution path. - id: SH-4 title: Timing side channels in atomic operations @@ -147,3 +151,58 @@ security-hazards: rationale: > Wide arithmetic is new and complex. Implementation errors in carry propagation or sign extension are plausible. + + - id: SH-7 + title: ABI mismatch between Synth-compiled code and kiln-builtins + description: > + Synth compiles core WebAssembly modules to native ELF binaries that + call into kiln-builtins via a C ABI interface. If Synth and + kiln-builtins disagree on the calling convention (argument register + assignment, stack layout, return value encoding, struct passing), + an adversary can craft a module whose Synth-compiled output passes + arguments that kiln-builtins misinterprets. This can cause + kiln-builtins to perform memory operations at attacker-controlled + offsets, bypass capability checks by reading wrong argument slots, + or corrupt its internal state by writing return values to wrong + locations. + security-losses: [SL-1, SL-4] + safety-hazards: [H-2, H-1] + attack-vector: > + Adversary provides a component that, after Meld lowering and Synth + compilation, produces a native call sequence where the argument + layout exploits a disagreement between Synth's ABI assumptions and + kiln-builtins' ABI expectations. For example, Synth places a + memory base pointer in register r2 while kiln-builtins reads it + from r3, causing a bounds check to use an attacker-controlled value. + exploitability: medium + rationale: > + The Synth-to-kiln-builtins ABI is defined by convention across two + independent codebases. Version skew or platform-specific calling + convention differences (ARM vs RISC-V) create opportunities for + mismatch. + + - id: SH-8 + title: Capability escalation through Meld component fusion + description: > + Meld fuses multiple components into core modules at build time, + resolving inter-component imports to direct calls. If Meld's fusion + incorrectly wires an import from component A to an export from + component B that has broader capabilities than A is authorized to + use, the fused module grants A access to B's capabilities. An + adversary who controls component A's source can exploit this to + access filesystem, network, or other WASI capabilities that the + original component graph did not authorize for A. + security-losses: [SL-1, SL-3] + safety-hazards: [H-8] + attack-vector: > + Adversary publishes a component that declares a narrow import + (e.g., wasi:clocks/monotonic-clock). Meld's fusion, due to a name + resolution bug or overly permissive matching, wires this import to + a broader export (e.g., wasi:filesystem/types) from another + component in the graph. The adversary's code now has filesystem + access through the misrouted import. + exploitability: medium + rationale: > + Component fusion is a complex graph transformation. Name resolution + across WIT interfaces with versioning and aliasing creates + opportunities for incorrect wiring that escalates capabilities. diff --git a/safety/stpa-sec/vulnerabilities.yaml b/safety/stpa-sec/vulnerabilities.yaml index 2a88bc74..8a851c68 100644 --- a/safety/stpa-sec/vulnerabilities.yaml +++ b/safety/stpa-sec/vulnerabilities.yaml @@ -277,3 +277,96 @@ vulnerabilities: enough to verify exhaustively for representative input classes. status: unmitigated priority: medium + + # =========================================================================== + # SH-7: ABI mismatch between Synth-compiled code and kiln-builtins + # =========================================================================== + - id: V-7 + security-hazard: SH-7 + title: Synth-to-kiln-builtins ABI mismatch + code-locations: + - file: kiln-builtins/src/abi.rs + description: > + The C ABI surface that kiln-builtins exposes to Synth-compiled + native code. Argument register assignments, struct passing + conventions, and return value encoding must exactly match what + Synth generates. + - file: kiln-builtins/src/intrinsics/ + description: > + Host intrinsic implementations called by Synth-compiled code. + Each intrinsic reads arguments from the ABI-defined locations. + Mismatch causes wrong values to be read or written. + mitigations: + - id: MIT-7.1 + description: > + Define the Synth-to-kiln-builtins ABI as a versioned, machine- + readable specification (e.g., a shared header or bindgen input). + Both Synth and kiln-builtins must be generated from or validated + against this single specification. Version the ABI with a magic + number checked at load time. + status: unmitigated + priority: critical + - id: MIT-7.2 + description: > + Add end-to-end ABI conformance tests: compile known modules with + Synth, execute on gale with kiln-builtins, and verify that + argument values, return values, and memory operations match + expected results. Cover all intrinsic functions and all supported + target architectures (ARM, RISC-V, x86-64). + status: unmitigated + priority: high + - id: MIT-7.3 + description: > + Include an ABI version check in the kiln-builtins initialization + path. Synth-compiled ELF binaries embed the ABI version they + were compiled against. kiln-builtins refuses to execute binaries + with a mismatched ABI version, failing loudly rather than + silently misinterpreting arguments. + status: unmitigated + priority: critical + + # =========================================================================== + # SH-8: Capability escalation through Meld component fusion + # =========================================================================== + - id: V-8 + security-hazard: SH-8 + title: Capability escalation through Meld fusion wiring + code-locations: + - file: kiln-component/src/linker.rs + description: > + The Kiln-side linker that resolves remaining host/WASI imports + after Meld fusion. Must verify that the fused module's import + set does not exceed the union of capabilities authorized for + the original components. + - file: kiln-wasi/src/dispatcher.rs + description: > + WASI capability dispatcher. Must enforce per-component capability + sets even after fusion has flattened the component graph into + core modules. + mitigations: + - id: MIT-8.1 + description: > + Meld must emit a capability manifest alongside the fused core + module, listing which original component each import originated + from and what capabilities were authorized. Kiln's linker + validates this manifest against the host's capability policy + before instantiation. + status: unmitigated + priority: critical + - id: MIT-8.2 + description: > + Add integration tests that verify capability boundaries survive + fusion: create a two-component graph where component A has + clock-only capabilities and component B has filesystem + capabilities. After fusion, verify that code paths originating + from A cannot reach filesystem imports. + status: unmitigated + priority: high + - id: MIT-8.3 + description: > + Implement a post-fusion capability audit in Kiln that traces + each import in the fused module back to its originating + component and verifies the capability authorization chain. + Log warnings for any import that cannot be traced. + status: unmitigated + priority: medium diff --git a/safety/stpa/control-structure.yaml b/safety/stpa/control-structure.yaml index 9fcd9778..ff1c3301 100644 --- a/safety/stpa/control-structure.yaml +++ b/safety/stpa/control-structure.yaml @@ -255,6 +255,55 @@ controllers: - from: PROC-BUDGET info: Allocation success/failure, remaining budget + - id: CTRL-MELD + name: Meld Component Lowering (Build Time) + type: automated + description: > + Build-time tool that lowers Component Model constructs to core + WebAssembly modules. Resolves inter-component imports, performs + canonical ABI lift/lower transformations statically, and fuses + multi-component graphs into core modules. Meld runs before Kiln + and produces the artifacts that Kiln or Synth consume. Not part + of the Kiln runtime, but its output format is a trust boundary + for Kiln's decoder and linker. + source-crate: meld-core (external) + control-actions: + - ca: CA-MELD-1 + target: PROC-MODULE + action: Lower component to core module(s) with embedded adapters + - ca: CA-MELD-2 + target: PROC-INSTANCE + action: Resolve inter-component imports to direct core-level wiring + - ca: CA-MELD-3 + target: PROC-CANONICAL + action: Emit static canonical ABI adapter trampolines + feedback: + - from: PROC-MODULE + info: Fused core module bytes, capability manifest, adapter metadata + + - id: CTRL-SYNTH + name: Synth AOT Compiler (Build Time) + type: automated + description: > + Build-time AOT compiler that translates core WebAssembly modules + (typically Meld output) to native ELF binaries for gale and other + embedded targets. Generates native code that calls into + kiln-builtins for host intrinsics. Synth runs before deployment + and produces the native artifacts that gale loads. + source-crate: synth-codegen (external) + control-actions: + - ca: CA-SYNTH-1 + target: PROC-BUILTINS + action: Generate native calls to kiln-builtins host intrinsics + - ca: CA-SYNTH-2 + target: PROC-GALE + action: Emit native ELF binary for target architecture + feedback: + - from: PROC-BUILTINS + info: ABI version compatibility, intrinsic availability + - from: PROC-GALE + info: Target architecture constraints, memory layout + controlled-processes: - id: PROC-INSTRUCTION name: Instruction Stream @@ -315,3 +364,19 @@ controlled-processes: - id: PROC-BUDGET name: Allocation Budget description: Per-crate memory budget tracked by the allocation manager + + - id: PROC-BUILTINS + name: kiln-builtins Host Intrinsics + description: > + The no_std runtime support library providing host intrinsics for + Synth-compiled native code. Includes memory bounds checking, + table access, WASI host functions for embedded targets, and trap + handling. Linked into gale firmware images. + + - id: PROC-GALE + name: Gale Native Execution Environment + description: > + The gale RTOS execution environment that loads and runs + Synth-compiled native ELF binaries. Provides task scheduling, + hardware abstraction (MPU, interrupts), and links against + kiln-builtins for host intrinsic dispatch. diff --git a/safety/stpa/cross-toolchain-consistency.yaml b/safety/stpa/cross-toolchain-consistency.yaml index 2bf265be..3d61d694 100644 --- a/safety/stpa/cross-toolchain-consistency.yaml +++ b/safety/stpa/cross-toolchain-consistency.yaml @@ -22,11 +22,14 @@ cross-toolchain-hazards: title: Canonical ABI element size disagreement (Meld ↔ Kiln) tools: [meld, kiln] description: > - Meld's parser.rs::canonical_abi_element_size() and Kiln's - kiln-component canonical_abi compute different element sizes for - the same component type. When running a Meld-fused P2 component, - adapters (computed by Meld) allocate buffers with wrong sizes vs. - what Kiln's lift/lower expects. + Meld lowers components to core modules at build time, computing + canonical ABI element sizes for adapter code it embeds. Kiln's + interpreter executes the resulting core modules and dispatches + host intrinsics. If Meld's parser.rs::canonical_abi_element_size() + and Kiln's kiln-component canonical_abi compute different element + sizes for the same component type, the adapter code embedded by + Meld allocates buffers with wrong sizes vs. what Kiln's host + intrinsic dispatch expects to read. affected-types: - "list> with non-trivial padding" - "record with mixed-size fields (u8, u32, u64)" @@ -47,12 +50,15 @@ cross-toolchain-hazards: # XH-3: Synth ↔ Kiln element size disagreement # ========================================================================= - id: XH-3 - title: Canonical ABI element size disagreement (Synth ↔ Kiln) - tools: [synth, kiln] + title: Canonical ABI element size disagreement (Synth ↔ kiln-builtins) + tools: [synth, kiln-builtins] description: > - Synth's synth-abi crate computes element sizes for AOT compilation. - When Synth-compiled code runs on Kiln (via Gale), the import dispatch - argument layout must match what Kiln expects to read. + Synth compiles Meld-lowered core modules to native ELF for gale. + Synth's synth-abi crate computes element sizes for the native call + ABI. When Synth-compiled code runs on gale with kiln-builtins as + the host intrinsic library, the argument layout in native calls to + kiln-builtins must match what kiln-builtins expects to read. This + is a native ABI boundary, not a Wasm-level boundary. affected-types: - "Import arguments with composite types" - "Return values written via retptr" @@ -112,6 +118,68 @@ cross-toolchain-hazards: kiln-implementation: kiln-component/src/canonical_abi/ requirement: SR-10 + # ========================================================================= + # XH-6: Meld fusion format versioning + # ========================================================================= + - id: XH-6 + title: Meld fusion output format versioning (Meld ↔ Kiln) + tools: [meld, kiln] + description: > + Meld produces fused core modules with a specific encoding of + adapter trampolines, import tables, and metadata sections. If + Meld's output format evolves (e.g., new trampoline encoding, + changed custom section layout) without a corresponding update + in Kiln's decoder and linker, Kiln may misparse the fused + module, skip adapter code, or resolve imports incorrectly. + The fused module format is not part of the WebAssembly spec + and is a private contract between Meld and Kiln. + affected-types: + - "Custom sections encoding adapter metadata" + - "Trampoline function signatures" + - "Import/export name mangling conventions" + impact: > + Kiln silently loads a fused module but misinterprets adapter + metadata. Host intrinsic calls receive wrong arguments or are + dispatched to wrong handlers. No trap occurs because the core + module is structurally valid. + mitigation: + primary: "Version tag in Meld's custom section, checked by Kiln at load time" + secondary: "Shared integration test suite using pinned Meld output artifacts" + kiln-implementation: kiln-decoder/src/custom_sections.rs + meld-implementation: meld-core/src/fusion/output.rs + requirement: SR-11 + + # ========================================================================= + # XH-7: kiln-builtins ABI stability + # ========================================================================= + - id: XH-7 + title: kiln-builtins ABI stability (Synth ↔ kiln-builtins) + tools: [synth, kiln-builtins] + description: > + Synth generates native code that calls kiln-builtins host + intrinsics via a C ABI. The function signatures, argument + passing conventions, and struct layouts must remain stable + across kiln-builtins releases, or Synth-compiled binaries + built against one version will malfunction when linked with + a different version. Unlike the Wasm-level ABI (which is + spec-defined), this native ABI is a private contract between + Synth and kiln-builtins with no external specification. + affected-types: + - "Host intrinsic function signatures" + - "Memory descriptor structs passed by pointer" + - "Error code enumerations" + impact: > + Synth-compiled binary calls kiln-builtins function with wrong + argument layout. kiln-builtins reads corrupted values, leading + to memory safety violations or incorrect execution on embedded + targets. + mitigation: + primary: "Versioned ABI header shared between Synth and kiln-builtins via build dependency" + secondary: "ABI version magic number embedded in ELF, checked at load time by kiln-builtins" + kiln-implementation: kiln-builtins/src/abi.rs + synth-implementation: synth-codegen/src/abi/builtins.rs + requirement: SR-24 + # ========================================================================= # Fixture Coverage Matrix # ========================================================================= diff --git a/safety/stpa/hazards.yaml b/safety/stpa/hazards.yaml index 8a423037..d9e325d8 100644 --- a/safety/stpa/hazards.yaml +++ b/safety/stpa/hazards.yaml @@ -86,6 +86,8 @@ hazards: The fuel-aware waker interferes with deterministic scheduling. Task cancellation leaves dangling references. losses: [L-4, L-6] + scope: deferred + note: "Async not in P2 scope" - id: H-8 title: WASI host function violates capability boundary @@ -152,6 +154,16 @@ hazards: cast operations, leading to unsound type coercions. losses: [L-1, L-2, L-3, L-7] + - id: H-13 + title: Meld-fused module ABI mismatch + description: > + Meld produces a core module whose host intrinsic signatures don't + match Kiln/kiln-builtins expectations. The fused module calls a + host intrinsic with the wrong number of parameters, wrong types, + or wrong calling convention, causing a trap, silent data corruption, + or undefined behavior at the host boundary. + losses: [L-1, L-2] + # Sub-hazards for complex areas sub-hazards: # Refinements of H-4 (Canonical ABI) @@ -162,6 +174,8 @@ sub-hazards: UTF-8 to UTF-16 or Latin-1 conversion produces invalid sequences, miscounts code units, or doesn't handle surrogate pairs. Matches Meld H-4.4 but at runtime rather than fusion time. + scope: delegated-to-meld + note: "Canonical ABI operations performed at build time by Meld per BA RFC #46" - id: H-4.2 parent: H-4 @@ -171,6 +185,8 @@ sub-hazards: parser.rs canonical_abi_element_size for the same type. When running meld-fused modules, the adapter allocates N bytes but kiln's lift reads M bytes (M ≠ N), causing data corruption. + scope: delegated-to-meld + note: "Canonical ABI operations performed at build time by Meld per BA RFC #46" - id: H-4.3 parent: H-4 @@ -179,6 +195,8 @@ sub-hazards: Record fields are laid out with incorrect alignment, causing loads/stores to read from wrong offsets within the record's linear memory representation. + scope: delegated-to-meld + note: "Canonical ABI operations performed at build time by Meld per BA RFC #46" # Refinements of H-5 (cross-component) - id: H-5.1 diff --git a/safety/stpa/loss-scenarios.yaml b/safety/stpa/loss-scenarios.yaml index 97fd8aae..f1965c9c 100644 --- a/safety/stpa/loss-scenarios.yaml +++ b/safety/stpa/loss-scenarios.yaml @@ -497,3 +497,46 @@ loss-scenarios: - Lock scope does not cover the entire read-modify-write sequence - Single-threaded testing does not reveal the atomicity gap - No formal model of the memory ordering semantics + + # ========================================================================= + # RFC #46 Architecture scenarios + # ========================================================================= + - id: LS-RF46-1 + title: Meld produces lowered module with ABI incompatible with Kiln host intrinsics + uca: UCA-BI-1 + hazards: [H-13] + type: inadequate-process-model + scenario: > + Meld lowers a component to a core module and emits host intrinsic + calls (e.g., memory.copy, string transcoding stubs) using a calling + convention or signature that differs from what Kiln's host import + handler or kiln-builtins expects. At runtime, the fused module calls + the intrinsic with the wrong number of arguments or wrong types. The + host handler either traps with an opaque "signature mismatch" error + or, worse, silently interprets the arguments incorrectly, producing + corrupted data. + causal-factors: + - Meld and Kiln define host intrinsic signatures independently + - No shared IDL or machine-readable contract for host intrinsic ABI + - Version skew between Meld and Kiln releases + process-model-flaw: > + Meld assumes Kiln's host intrinsic ABI matches its own emitted calls; + no compile-time or load-time ABI verification exists + + - id: LS-RF46-2 + title: Synth-compiled code calls kiln-builtin with wrong calling convention + uca: UCA-BI-1 + hazards: [H-13] + type: inadequate-control-algorithm + scenario: > + Synth compiles a Meld-fused core module to native ELF for an embedded + target. The compiled code calls a kiln-builtin function using the + platform's C calling convention, but the builtin was compiled with a + different convention (e.g., different register allocation for i64 + return values on 32-bit ARM). The return value is read from the wrong + register or stack location, producing garbage data that propagates + silently through the application. + causal-factors: + - Synth and kiln-builtins compiled with different ABI settings + - No ABI compatibility check at link time for embedded targets + - 32-bit platforms split 64-bit values across register pairs differently diff --git a/safety/stpa/ucas.yaml b/safety/stpa/ucas.yaml index ab079312..cad002b5 100644 --- a/safety/stpa/ucas.yaml +++ b/safety/stpa/ucas.yaml @@ -157,6 +157,7 @@ component-model-ucas: miscounts code units or produces invalid sequences. context: "String containing multi-byte UTF-8 characters" hazards: [H-4] + scope: delegated-to-meld - id: UCA-CM-2 description: > @@ -164,6 +165,7 @@ component-model-ucas: incorrect alignment calculation. context: "Record with mixed-size fields (u8, u32, u64)" hazards: [H-4] + scope: delegated-to-meld - id: UCA-CM-3 description: > @@ -171,6 +173,7 @@ component-model-ucas: past the end of the list buffer or leaving uninitialized gaps. context: "list> where element_size != sum of field sizes" hazards: [H-4] + scope: delegated-to-meld - id: UCA-CM-4 description: > @@ -178,6 +181,7 @@ component-model-ucas: previously-dropped but not-yet-reclaimed handle. context: "Rapid create/drop cycle filling resource table" hazards: [H-6] + scope: reduced - id: UCA-CM-5 description: > @@ -185,6 +189,7 @@ component-model-ucas: resource table's free list or dropping the wrong resource. context: "Component error path that drops handle in both normal and cleanup code" hazards: [H-6] + scope: reduced - id: UCA-CM-7 description: > @@ -192,6 +197,7 @@ component-model-ucas: instance index lookup in the linker's resolution table. context: "Multiple component instances with same export name" hazards: [H-5] + scope: delegated-to-meld - id: UCA-CM-8 description: > @@ -200,6 +206,7 @@ component-model-ucas: modules to corrupt data at the kiln lift/lower boundary. context: "Running a meld-fused component through kiln with P2 wrapper" hazards: [H-4] + scope: reduced rationale: > This is a cross-tool consistency hazard. Meld computes CopyLayout at fusion time; Kiln computes canonical ABI layout at runtime. If @@ -213,6 +220,7 @@ component-model-ucas: freed state. context: "Task cancellation racing with stream data arrival" hazards: [H-7] + scope: deferred linker-ucas: control-action: "Resolve imports to exports across component instances" @@ -380,3 +388,18 @@ gc-ucas: within its configured budget. context: "Module that allocates millions of small structs without growing linear memory" hazards: [H-12, H-3, H-10] + +builtins-ucas: + control-action: "Provide host intrinsic implementations for synth-compiled code" + controller: CTRL-BUILTINS + + providing: + - id: UCA-BI-1 + description: > + Builtin provides wrong return type to synth-compiled code. A + kiln-builtin host intrinsic returns a value whose type (e.g., i64 + instead of i32, or wrong struct layout) does not match what the + synth-compiled caller expects, causing the caller to misinterpret + the return value and produce incorrect results or memory corruption. + context: "Synth-compiled module calling kiln-builtin after Meld fusion" + hazards: [H-13]