diff --git a/.rivet/agent-context.md b/.rivet/agent-context.md new file mode 100644 index 000000000..411c856bb --- /dev/null +++ b/.rivet/agent-context.md @@ -0,0 +1,146 @@ +# Rivet Agent Context + +Auto-generated by `rivet context` — do not edit. + +## Project + +- **Name:** kiln +- **Version:** 0.1.0 +- **Schemas:** common, stpa, dev +- **Sources:** safety/stpa (stpa-yaml), safety/requirements (generic-yaml) +- **Docs:** docs + +## Artifacts + +| Type | Count | Example IDs | +|------|-------|-------------| +| control-action | 32 | CA-HOST-1, CA-HOST-2, CA-HOST-3 | +| controlled-process | 12 | PROC-INSTRUCTION, PROC-MEMORY, PROC-STACK | +| controller | 9 | CTRL-HOST, CTRL-ENGINE, CTRL-DECODER | +| controller-constraint | 29 | CC-E-1, CC-E-2, CC-E-3 | +| design-decision | 18 | SM-MEM-001, SM-MEM-002, SM-CFI-001 | +| feature | 16 | AC-RUNTIME, AC-MEMORY, AC-COMPONENT | +| hazard | 10 | H-1, H-2, H-3 | +| loss | 8 | L-1, L-2, L-3 | +| loss-scenario | 21 | LS-E-1, LS-E-2, LS-E-3 | +| requirement | 62 | SR-1, SR-2, SR-3 | +| sub-hazard | 5 | H-4.1, H-4.2, H-4.3 | +| system-constraint | 11 | SC-1, SC-2, SC-3 | +| uca | 29 | UCA-A-1, UCA-A-2, UCA-BZ-1 | +| **Total** | **262** | | + +## Schema + +- **`control-action`** — An action issued by a controller to a controlled process or another controller. + + Required fields: action +- **`controlled-process`** — A process being controlled — the physical or data transformation acted upon by controllers. + + Required fields: (none) +- **`controller`** — A system component (human or automated) responsible for issuing control actions. Each controller has a process model — its internal beliefs about the state of the controlled process. + + Required fields: (none) +- **`controller-constraint`** — A constraint on a controller's behavior derived by inverting a UCA. Specifies what the controller must or must not do. + + Required fields: constraint +- **`design-decision`** — An architectural or design decision with rationale + Required fields: rationale +- **`feature`** — A user-visible capability or feature + Required fields: (none) +- **`hazard`** — A system state or set of conditions that, together with worst-case environmental conditions, will lead to a loss. + + Required fields: (none) +- **`loss`** — An undesired or unplanned event involving something of value to stakeholders. Losses define what the analysis aims to prevent. + + Required fields: (none) +- **`loss-scenario`** — A causal pathway describing how a UCA could occur or how the control action could be improperly executed, leading to a hazard. + + Required fields: (none) +- **`requirement`** — A functional or non-functional requirement + Required fields: (none) +- **`sub-hazard`** — A refinement of a hazard into a more specific unsafe condition. + + Required fields: (none) +- **`system-constraint`** — A condition or behavior that must be satisfied to prevent a hazard. Each constraint is the inversion of a hazard. + + Required fields: (none) +- **`uca`** — An Unsafe Control Action — a control action that, in a particular context and worst-case environment, leads to a hazard. Four types (provably complete): + 1. Not providing the control action leads to a hazard + 2. Providing the control action leads to a hazard + 3. Providing too early, too late, or in the wrong order + 4. Control action stopped too soon or applied too long + + Required fields: uca-type + +### Link Types + +- `acts-on` (inverse: `acted-on-by`) +- `allocated-to` (inverse: `allocated-from`) +- `caused-by-uca` (inverse: `causes-scenario`) +- `constrained-by` (inverse: `constrains`) +- `constrains-controller` (inverse: `controller-constrained-by`) +- `depends-on` (inverse: `depended-on-by`) +- `derives-from` (inverse: `derived-into`) +- `implements` (inverse: `implemented-by`) +- `inverts-uca` (inverse: `inverted-by`) +- `issued-by` (inverse: `issues`) +- `leads-to-hazard` (inverse: `hazard-caused-by`) +- `leads-to-loss` (inverse: `loss-caused-by`) +- `mitigates` (inverse: `mitigated-by`) +- `prevents` (inverse: `prevented-by`) +- `refines` (inverse: `refined-by`) +- `satisfies` (inverse: `satisfied-by`) +- `traces-to` (inverse: `traced-from`) +- `verifies` (inverse: `verified-by`) + +## Traceability Rules + +| Rule | Source Type | Severity | Description | +|------|------------|----------|-------------| +| hazard-has-loss | hazard | error | Every hazard must link to at least one loss | +| constraint-has-hazard | system-constraint | error | Every system constraint must link to at least one hazard | +| uca-has-hazard | uca | error | Every UCA must link to at least one hazard | +| uca-has-controller | uca | error | Every UCA must link to a controller | +| controller-constraint-has-uca | controller-constraint | error | Every controller constraint must link to at least one UCA | +| hazard-has-constraint | hazard | warning | Every hazard should be addressed by at least one system constraint | +| uca-has-controller-constraint | uca | warning | Every UCA should be addressed by at least one controller constraint | +| requirement-coverage | requirement | warning | Every requirement should be satisfied by at least one design decision or feature | +| decision-justification | design-decision | error | Every design decision must link to at least one requirement | + +## Coverage + +**Overall: 93.0%** + +| Rule | Source Type | Covered | Total | % | +|------|------------|---------|-------|---| +| hazard-has-loss | hazard | 10 | 10 | 100.0% | +| constraint-has-hazard | system-constraint | 11 | 11 | 100.0% | +| uca-has-hazard | uca | 29 | 29 | 100.0% | +| uca-has-controller | uca | 29 | 29 | 100.0% | +| controller-constraint-has-uca | controller-constraint | 29 | 29 | 100.0% | +| hazard-has-constraint | hazard | 10 | 10 | 100.0% | +| uca-has-controller-constraint | uca | 29 | 29 | 100.0% | +| requirement-coverage | requirement | 46 | 62 | 74.2% | +| decision-justification | design-decision | 18 | 18 | 100.0% | + +## Validation + +0 errors, 16 warnings + +## Commands + +```bash +rivet validate # validate all artifacts +rivet list # list all artifacts +rivet list -t # filter by type +rivet stats # artifact counts + orphans +rivet coverage # traceability coverage report +rivet matrix --from X --to Y # traceability matrix +rivet diff --base A --head B # compare artifact sets +rivet schema list # list schema types +rivet schema show # show type details +rivet schema rules # list traceability rules +rivet export -f generic-yaml # export as YAML +rivet serve # start dashboard on :3000 +rivet context # regenerate this file +``` diff --git a/docs/requirements.txt b/docs/requirements.txt index a9b7352ec..a5a409333 100644 --- a/docs/requirements.txt +++ b/docs/requirements.txt @@ -1,5 +1,4 @@ sphinx>=7.1.2 -sphinx-needs>=1.2.1 sphinx-book-theme>=0.0.1 myst-parser>=2.0.0 sphinxcontrib-plantuml>=0.25.0 diff --git a/docs/source/conf.py b/docs/source/conf.py index b08f89a8e..420b03174 100644 --- a/docs/source/conf.py +++ b/docs/source/conf.py @@ -103,17 +103,12 @@ def patched_process_doc(self, env, docname, document): # Add our custom JavaScript for code copy app.add_js_file('js/code-copy.js') - # Register the dynamic function for extracting requirements - from sphinx_needs.api.configuration import add_dynamic_function - add_dynamic_function(app, extract_reqs) - return {'version': '0.1', 'parallel_read_safe': True} extensions = [ 'sphinx.ext.autodoc', 'sphinx.ext.viewcode', 'sphinx.ext.napoleon', - 'sphinx_needs', 'myst_parser', 'sphinxcontrib.plantuml', "sphinxcontrib_rust", @@ -188,103 +183,9 @@ def patched_process_doc(self, env, docname, document): # Allow customization through environment variables plantuml_output_format = os.environ.get('PLANTUML_FORMAT', 'svg') -# Sphinx-needs configuration -needs_types = [ - dict(directive="req", title="Requirement", prefix="REQ_", color="#BFD8D2", style="node"), - dict(directive="spec", title="Specification", prefix="SPEC_", color="#FEDCD2", style="node"), - dict(directive="impl", title="Implementation", prefix="IMPL_", color="#DF744A", style="node"), - dict(directive="test", title="Test Case", prefix="T_", color="#DCB239", style="node"), - dict(directive="safety", title="Safety", prefix="SAFETY_", color="#FF5D73", style="node"), - dict(directive="qual", title="Qualification", prefix="QUAL_", color="#9370DB", style="node"), - dict(directive="constraint", title="Constraint", prefix="CNST_", color="#4682B4", style="node"), - dict(directive="panic", title="Panic", prefix="KILNQ_", color="#E74C3C", style="node"), - dict(directive="src", title="Source file", prefix="SRC_", color="#C6C6FF", style="node"), - # Architecture-specific types - dict(directive="arch_component", title="Architectural Component", prefix="ARCH_COMP_", color="#FF6B6B", style="node"), - dict(directive="arch_interface", title="Interface", prefix="ARCH_IF_", color="#4ECDC4", style="node"), - dict(directive="arch_decision", title="Design Decision", prefix="ARCH_DEC_", color="#45B7D1", style="node"), - dict(directive="arch_constraint", title="Design Constraint", prefix="ARCH_CON_", color="#96CEB4", style="node"), - dict(directive="arch_pattern", title="Design Pattern", prefix="ARCH_PAT_", color="#FECA57", style="node"), -] - -# Add ID regex pattern for sphinx-needs -needs_id_regex = '^[A-Z0-9_]{5,}$' - -# Add option specs to register additional options for directives -needs_extra_options = [ - 'rationale', - 'verification', - 'mitigation', - 'implementation', - 'safety_impact', - 'item_status', - 'handling_strategy', - 'last_updated', - 'file', - 'implements', - # Architecture-specific options - 'crate', - 'provides', - 'requires', - 'allocated_requirements', - 'environment', - 'variant_of', - 'impacts', - 'deciders', - 'alternatives', - 'stability', - 'protocol', -] - -# Allow all sphinx-needs options for all directives -needs_allow_unsafe_options = True - -# Disable warnings for unknown link targets to avoid the many outgoing link warnings -needs_warnings_always_warn = False - -# Custom sphinx-needs templates for qualification and safety -needs_templates = { - 'safety_template': '**Hazard**: {{content}}\n\n**Mitigation**: {{mitigation}}', - 'qualification_template': '**Status**: {{item_status}}\n\n**Implementation**: {{implementation}}', - 'constraint_template': '**Constraint**: {{content}}\n\n**Rationale**: {{rationale}}\n\n**Verification**: {{verification}}', - 'panic_template': '**Panic Condition**: {{content}}\n\n**Safety Impact**: {{safety_impact}}\n\n**Status**: {{item_status}}\n\n**Handling Strategy**: {{handling_strategy}}', -} - -# Tags for filtering and displaying panic entries -needs_tags = [ - dict(name="panic", description="Panic documentation entry", bgcolor="#E74C3C"), - dict(name="low", description="Low safety impact", bgcolor="#2ECC71"), - dict(name="medium", description="Medium safety impact", bgcolor="#F39C12"), - dict(name="high", description="High safety impact", bgcolor="#E74C3C"), - dict(name="unknown", description="Unknown safety impact", bgcolor="#95A5A6"), - # Architecture tags - dict(name="core", description="Core architecture component", bgcolor="#FF6B6B"), - dict(name="portability", description="Multi-platform portability", bgcolor="#4ECDC4"), - dict(name="safety", description="Safety-critical component", bgcolor="#FF5D73"), - dict(name="performance", description="Performance-critical component", bgcolor="#FECA57"), - dict(name="testing", description="Testing and verification", bgcolor="#96CEB4"), -] - -# Configure needs roles for referencing -needs_role_need_template = "{title} ({id})" -needs_role_need_max_title_length = 30 -needs_id_length = 7 -needs_title_optional = True -needs_file_pattern = '**/*.rst' - -# New extra links configuration -needs_extra_links = [ - dict( - option = "realizes", - incoming = "is realized by", - outgoing = "realizes", - style = "solid,#006A6A", - ), -] - -# Regular expression for finding requirement IDs -REQ_RE = re.compile(r"SW-REQ-ID\\s*:\\s*(REQ_\\w+)", re.I) +# Requirement/safety traceability has been migrated to rivet (safety/ directory). +# See: rivet validate, rivet coverage, rivet serve # Initialize source_suffix before attempting to modify it source_suffix = { @@ -308,50 +209,6 @@ def patched_process_doc(self, env, docname, document): '.md': 'markdown', } -# Dynamic function to extract requirement IDs from a file -def extract_reqs(app, need, needs, *args, **kwargs): - """ - Return all REQ_xxx IDs that occur in the file given via :file:. - Called as a *dynamic function* during the build. - """ - relative_file_path_from_doc_source = need.get("file") - if not relative_file_path_from_doc_source: - return "" - - # Construct the absolute path to the source file. - # app.confdir is the directory of conf.py (e.g., /path/to/workspace/docs/source) - # relative_file_path_from_doc_source is like '../../kiln/src/some_file.rs' - # So, Path(app.confdir) / relative_file_path_from_doc_source gives the absolute path. - absolute_src_file_path = (pathlib.Path(app.confdir) / relative_file_path_from_doc_source).resolve() - - try: - text = absolute_src_file_path.read_text(errors="ignore") - ids = REQ_RE.findall(text) - return ";".join(sorted(set(ids))) # needs wants ';' as separator - except FileNotFoundError: - print(f"WARNING: [extract_reqs] File not found: {absolute_src_file_path} (original path in need: {relative_file_path_from_doc_source})") - return "" - except Exception as e: - print(f"ERROR: [extract_reqs] Could not read file {absolute_src_file_path}: {e}") - return "" - -# Configuration to make specific strings in RST linkable -needs_string_links = { - # Link REQ_XXX to its definition - "req_inline": { - "regex": r"(?PREQ_\w+)", - "link_url": "#{{value}}", - "link_name": "{{value}}", - "options": [], - }, - # Link file paths in :file: option to GitHub - "source_file_link": { - "regex": r"^(?P(?:\.\.\/)*[a-zA-Z0-9_\-\/]+\.rs)$", - "link_url": "https://github.com/pulseengine/kiln/blob/main/{{value.replace('../../', '')}}", - "link_name": "{{value}}", - "options": ["file"], - } -} # Rust documentation configuration # Start with core working crates first diff --git a/docs/source/qualification/evaluation_plan.rst b/docs/source/qualification/evaluation_plan.rst deleted file mode 100644 index 2db0a861d..000000000 --- a/docs/source/qualification/evaluation_plan.rst +++ /dev/null @@ -1,148 +0,0 @@ -Evaluation Plan -=============== - -This document defines the evaluation approach for the Kiln project to determine qualification levels and activities. - -Introduction ------------- - -The evaluation plan establishes the criteria for determining the appropriate qualification levels for the Kiln project and outlines the activities required to meet those levels. - -Qualification Levels Assessment -------------------------------- - -This section assesses the target qualification levels for the Kiln project. - -.. qual:: ISO-26262 Qualification Level - :id: QUAL_100 - :item_status: targeted - :implementation: The Kiln targets ASIL D qualification according to ISO-26262 for automotive applications. - - ASIL D is the highest automotive safety integrity level and requires: - - Systematic capability 4 - - Diagnostic coverage >99% - - Single-point fault metric >99% - - Latent fault metric >90% - - Full statement, branch, and MC/DC coverage - -.. qual:: IEC-61508 Qualification Level - :id: QUAL_101 - :item_status: targeted - :implementation: The Kiln targets SIL 3 qualification according to IEC-61508 for general functional safety applications. - - SIL 3 requires: - - High diagnostic coverage - - Redundancy through diverse implementations - - Formal verification of critical algorithms - - Comprehensive testing - - Static analysis with no critical findings - -.. qual:: IEC-62304 Qualification Level - :id: QUAL_102 - :item_status: targeted - :implementation: The Kiln targets Class C qualification according to IEC-62304 for medical device software. - - Class C is for software that could directly contribute to serious injury or death, requiring: - - Complete documentation - - Risk management - - Design verification and validation - - Full traceability - - Comprehensive testing - -Safety Criticality Assessment ------------------------------ - -This section assesses the safety criticality of the Kiln components. - -.. list-table:: Component Safety Criticality - :widths: 20 15 65 - :header-rows: 1 - - * - Component - - Criticality - - Rationale - * - kiln-runtime - - High - - Core execution engine that handles all WebAssembly instructions - * - kiln-instructions - - High - - Implements instruction semantics crucial for correct execution - * - kiln-component - - Medium - - Handles interface types but doesn't affect core execution - * - kiln-sync - - High - - Critical for thread safety and resource coordination - * - kiln-logging - - Low - - Observability component not directly affecting execution - * - kilnd - - Medium - - Command-line interface that mediates access to runtime - -Qualification Activities Plan ------------------------------ - -The following activities are required for qualification: - -1. **Requirements Verification** - - Formal review of requirements - - Completeness analysis - - MCDC test coverage of requirements - - Traceability to specifications - -2. **Architecture Verification** - - Formal review of architecture - - Interface analysis - - Error handling analysis - - Resource usage analysis - -3. **Implementation Verification** - - Static analysis - - Dynamic analysis - - Formal verification where applicable - - Code review - -4. **Testing Strategy** - - Unit testing (100% statement coverage) - - Integration testing (100% branch coverage) - - System testing - - Performance testing - - MCDC testing for safety-critical components - -5. **Documentation** - - Requirements documentation - - Architecture documentation - - Implementation documentation - - Test documentation - - Traceability documentation - - Safety analysis - - Qualification evidence - -Evaluation Criteria -------------------- - -The following criteria will be used to evaluate the qualification status: - -.. list-table:: Qualification Criteria - :widths: 25 75 - :header-rows: 1 - - * - Criterion - - Passing Threshold - * - Statement Coverage - - 100% for safety-critical components - * - Branch Coverage - - 100% for safety-critical components - * - MC/DC Coverage - - 100% for safety-critical components - * - Static Analysis - - Zero high or critical findings - * - Runtime Assertion Failures - - Zero in qualification testing - * - Requirements Coverage - - 100% of requirements have tests - * - Formal Verification - - Critical algorithms formally verified - * - Safety Review - - All hazards identified and mitigated \ No newline at end of file diff --git a/docs/source/qualification/panic_registry.rst b/docs/source/qualification/panic_registry.rst deleted file mode 100644 index 0a2596d05..000000000 --- a/docs/source/qualification/panic_registry.rst +++ /dev/null @@ -1,133 +0,0 @@ -.. _panic-registry: - -Panic Registry -============== - -.. note:: - This document is automatically generated by the ``cargo-kiln update-panic-registry`` command. - Do not edit it directly. Panic information should be updated in the source code comments. - -This document contains all documented panic conditions in the Kiln codebase. -Each panic is tracked as a qualification requirement using sphinx-needs. - -.. contents:: Table of Contents - :local: - :depth: 2 - -Summary -------- - -* Total panic points: 10 -* Status: - * Todo: 10 - * In Progress: 0 - * Resolved: 0 - -The original CSV version of this registry is maintained at: -docs/source/development/panic_registry.csv - -.. csv-table:: Panic Registry CSV - :file: ../development/panic_registry.csv - :header-rows: 1 - :widths: auto - -Panic Details -------------- - -.. qual:: f32_nearest - :id: KILNQ_001 - :item_status: Todo - :implementation: - :tags: panic, unknown - :safety_impact: LOW - Limited impact, only affects specific F32 operations - :last_updated: 2025-04-25 - - **File:** kiln/src/execution.rs - **Line:** 389 - **Function:** f32_nearest - - This function will panic if the provided value is not an F32 value. - -.. qual:: f64_nearest - :id: KILNQ_002 - :item_status: Todo - :implementation: - :tags: panic, unknown - :safety_impact: LOW - Limited impact, only affects specific F64 operations - :last_updated: 2025-04-25 - - **File:** kiln/src/execution.rs - **Line:** 425 - **Function:** f64_nearest - - This function will panic if the provided value is not an F64 value. - -.. qual:: new - :id: KILNQ_003 - :item_status: Todo - :implementation: - :tags: panic, unknown - :safety_impact: LOW - This function does not actually panic - :last_updated: 2025-04-25 - - **File:** kiln-sync/src/mutex.rs - **Line:** 53 - **Function:** new - - This function does not panic. - -.. qual:: new - :id: KILNQ_004 - :item_status: Todo - :implementation: - :tags: panic, unknown - :safety_impact: MEDIUM - Memory corruption could cause system instability - :last_updated: 2025-04-25 - - **File:** kiln-foundation/src/safe_memory.rs - **Line:** 50 - **Function:** new - - This function will panic if the initial integrity verification fails. This can happen if memory corruption is detected during initialization. - -.. qual:: push - :id: KILNQ_005 - :item_status: Todo - :implementation: Return Result instead of panic - :tags: panic, unknown - :safety_impact: LOW - This function does not actually panic - :last_updated: 2025-04-25 - - **File:** kiln-foundation/src/bounded.rs - **Line:** 196 - **Function:** push - - This function does not panic. - -.. qual:: encode - :id: KILNQ_006 - :item_status: Todo - :implementation: Add checks for empty vector - :tags: panic, unknown - :safety_impact: MEDIUM - Could cause unexpected termination during module loading - :last_updated: 2025-04-25 - - **File:** kiln-decoder/src/module.rs - **Line:** 214 - **Function:** encode - - This function will panic if it attempts to access the last element of an empty custom_sections vector, which can happen if the implementation tries to process a custom section before any custom sections have been added to the module. - -.. qual:: buffer - :id: KILNQ_007 - :item_status: Todo - :implementation: Improve error handling - :tags: panic, unknown - :safety_impact: MEDIUM - Memory access issues could cause system instability - :last_updated: 2025-04-25 - - **File:** kiln-runtime/src/memory.rs - **Line:** 229 - **Function:** buffer - - In `no_std` \ No newline at end of file diff --git a/docs/source/qualification/plan.rst b/docs/source/qualification/plan.rst deleted file mode 100644 index a3ce64de1..000000000 --- a/docs/source/qualification/plan.rst +++ /dev/null @@ -1,356 +0,0 @@ -Qualification Plan -================== - -Overview --------- - -This qualification plan outlines the activities needed to implement a comprehensive qualification framework for the WebAssembly Runtime (Kiln) project. The plan identifies which qualification materials are already in place, which need to be implemented, and how to integrate them within the existing codebase structure. - -Qualification Materials Assessment ----------------------------------- - -We've assessed our current implementation status: - -.. list-table:: Qualification Materials Status - :widths: 30 15 55 - :header-rows: 1 - - * - Qualification Material - - Status - - Location/Implementation Plan - * - Evaluation Plan - - Partial - - Defined in :doc:`../requirements/index` - * - Evaluation Report - - Not Started - - TBD - * - Qualification Plan - - Started - - This document (qualification.rst) - * - Qualification Report - - Not Started - - To be implemented - * - Traceability Matrix - - Partial - - Partially in :doc:`../requirements/index` - * - Document List - - Not Started - - TBD - * - Internal Procedures - - Partial - - Partially in justfile - * - Technical Report - - Not Started - - To be implemented - * - Requirements - - Partial - - Defined in :doc:`../requirements/index` - -Implementation Requirements ---------------------------- - -1. Evaluation Plan Enhancements -^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ - -.. spec:: Evaluation Plan Enhancement - :id: QUAL_201 - :links: REQ_012, REQ_013 - - **Current Status**: Partial implementation in ../requirements/index.rst - - **Implementation Location**: docs/source/evaluation_plan.rst - - **Implementation Plan**: - - * Extend existing requirements linkage in ../requirements/index.rst - -2. Evaluation Report -^^^^^^^^^^^^^^^^^^^^ - -.. spec:: Evaluation Report Implementation - :id: QUAL_202 - - **Current Status**: Not Started - - **Implementation Location**: docs/source/evaluation_report.rst - - **Implementation Plan**: - - * Create a new document that evaluates: - - Hazardous events identification - - Risk assessment - - Mitigation strategies - - Safety assessment - -3. Complete Qualification Plan -^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ - -.. spec:: Qualification Plan Completion - :id: QUAL_103 - :links: REQ_012 - - **Current Status**: Started (this document) - - **Implementation Location**: docs/source/qualification_plan.rst - - **Implementation Plan**: - - * Formalize this qualification plan in RST format - * Add detailed phases and activities for achieving TCL 3/ASIL D qualification - * Define testing approach for IEC-61508 and IEC-62304 compliance - -4. Qualification Report -^^^^^^^^^^^^^^^^^^^^^^^ - -.. spec:: Qualification Report Creation - :id: QUAL_104 - :links: REQ_012, REQ_013 - - **Current Status**: Not Started - - **Implementation Location**: docs/source/qualification_report.rst - - **Implementation Plan**: - - * Create a template for documenting qualification evidence - * Connect qualification activities to test results - * Document validation approaches for each qualification activity - -5. Complete Traceability Matrix -^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ - -.. spec:: Traceability Matrix Enhancement - :id: QUAL_105 - :links: REQ_012 - - **Current Status**: Partial - - **Implementation Location**: docs/source/traceability_matrix.rst - - **Implementation Plan**: - - * Extend existing requirements linkage in requirements/index.rst - * Create a dedicated traceability matrix document - * Map requirements to test cases and test results - * Integrate with Sphinx for matrix generation - -6. Document List -^^^^^^^^^^^^^^^^ - -.. spec:: Document List Creation - :id: QUAL_106 - - **Current Status**: Not Started - - **Implementation Location**: docs/source/document_list.rst - - **Implementation Plan**: - - * Create a comprehensive document list - * Include reference documents used for qualification - * Add industry standards references (ISO-26262, IEC-61508, IEC-62304) - -7. Internal Procedures Enhancement -^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ - -.. spec:: Internal Procedures Documentation - :id: QUAL_107 - :links: REQ_012 - - **Current Status**: Partial (in justfile) - - **Implementation Location**: docs/source/internal_procedures.rst - - **Implementation Plan**: - - * Formalize testing procedures from justfile into documentation - * Document development environment setup - * Define code review procedures - * Create verification and validation procedures - -8. Technical Report -^^^^^^^^^^^^^^^^^^^ - -.. spec:: Technical Report Creation - :id: QUAL_108 - :links: REQ_012, REQ_013 - - **Current Status**: Not Started - - **Implementation Location**: docs/source/technical_report.rst - - **Implementation Plan**: - - * Create a technical report template - * Document architecture validation - * Include performance analysis - * Summarize qualification evidence - -Integration with Existing Tools -------------------------------- - -cargo-kiln Integration -^^^^^^^^^^^^^^^^^^^^^ - -The qualification process will be integrated with the unified cargo-kiln build system: - -* Add new cargo-kiln commands for qualification activities: - -.. code-block:: rust - - // In cargo-kiln/src/main.rs - pub enum QualificationCommand { - Traceability, - SafetyAnalysis, - Report, - } - - // Integrated into cargo-kiln subcommands - cargo-kiln qualification traceability - cargo-kiln qualification safety-analysis - cargo-kiln qualification report - -* Implement traceability matrix generation: - -.. code-block:: rust - - // In kiln-build-core/src/qualification.rs - pub fn generate_traceability_matrix() -> Result<()> { - // Implementation to extract requirements and tests - // Integrated into cargo-kiln qualification commands - // and generate a traceability matrix - }) - } - -justfile Integration -^^^^^^^^^^^^^^^^^^^^^^^^^ - -Add qualification-specific recipes to the justfile: - -.. code-block:: makefile - - # Generate qualification documentation - qualification-docs: docs-common - # Generate traceability matrix - cargo-kiln qualification traceability - # Build qualification documentation - {{sphinx_build}} -M html "{{sphinx_source}}" "{{sphinx_build_dir}}" {{sphinx_opts}} - - # Run qualification assessment - qualification-assessment: - cargo-kiln qualification assess - # Report qualification status - cargo-kiln qualification report-status - -Implementation Schedule ------------------------ - -1. **Phase 1: Documentation Structure** - - * Create required RST files in docs/source/ - * Implement cargo-kiln qualification commands - * Add justfile recipes - -2. **Phase 2: Traceability Implementation** - - * Complete requirements documentation - * Implement traceability matrix generation - * Link requirements to test cases - -3. **Phase 3: Safety Analysis** - - * Perform hazard analysis - * Document safety requirements - * Implement safety validation tests - -4. **Phase 4: Qualification Evidence** - - * Generate qualification reports - * Document test coverage results - * Prepare final qualification package - -Crate-Specific Qualification Activities ---------------------------------------- - -Each crate in the Kiln ecosystem requires specific qualification activities: - -kiln-runtime -^^^^^^^^^^^ - -Core functionality qualification: - -* MCDC (Modified Condition/Decision Coverage) testing -* Formal verification of critical algorithms -* Performance bounds validation - -kiln-foundation -^^^^^^^^^ - -Type system qualification: - -* Exhaustive type validation testing -* Boundary condition analysis -* Formal verification of type conversions - -kiln-component -^^^^^^^^^^^^^ - -Component model qualification: - -* Component model specification compliance testing -* Resource lifetime validation -* Interface mapping verification - -kiln-instructions -^^^^^^^^^^^^^^^^ - -Instruction qualification: - -* Instruction semantic verification -* Control flow validation -* Stack manipulation verification - -kiln-sync -^^^^^^^^ - -Synchronization qualification: - -* Thread safety verification -* Deadlock prevention validation -* Race condition testing - -kiln-logging -^^^^^^^^^^^ - -Logging qualification: - -* Logging performance impact testing -* Non-interference verification -* Resource usage validation - -kiln-host -^^^^^^^^ - -Host interface qualification: - -* Host function integrity testing -* Resource management verification -* Error handling validation - -kilnd -^^^^ - -Command-line interface qualification: - -* Input validation testing -* Error handling verification -* Performance validation - -Conclusion ----------- - -This qualification plan provides a roadmap for implementing the necessary qualification materials to achieve certification alignment with standards like ISO-26262 and IEC-61508. By following this plan, we will systematically extend our existing documentation and testing infrastructure to support formal qualification activities. - -.. needtable:: - :columns: id;title;status - :filter: id in ['QUAL_101', 'QUAL_102', 'QUAL_103', 'QUAL_104', 'QUAL_105', 'QUAL_106', 'QUAL_107', 'QUAL_108', 'SAFETY_MEM_001', 'SAFETY_RESOURCE_001', 'SAFETY_RECOVERY_001', 'SAFETY_IMPORTS_001', 'SAFETY_UNSAFE_001', 'SAFETY_FUZZ_001'] \ No newline at end of file diff --git a/docs/source/qualification/safety_analysis.rst b/docs/source/qualification/safety_analysis.rst deleted file mode 100644 index 52407ae19..000000000 --- a/docs/source/qualification/safety_analysis.rst +++ /dev/null @@ -1,128 +0,0 @@ -Safety Analysis Report -====================== - -This document contains the safety analysis for the WebAssembly Runtime (Kiln) project. - -Introduction ------------- - -This safety analysis identifies potential hazards that could arise from the use of the Kiln runtime in safety-critical applications and evaluates their potential impact. It also identifies mitigation strategies to address these hazards. - -Hazard Identification ---------------------- - -This section identifies potential hazards in the Kiln system and their mitigations. - -Safety-Critical Requirements -------------------------------- - -.. commenting out needfilter directives until they can be fixed -.. -.. .. needfilter:: -.. :types: req -.. :regex_filter: title, .*[Ss]afety.*|.*[Bb]ound.*|.*[Ll]imit.*|.*[Hh]azard.* - -.. safety:: Unbounded Execution - :id: SAFETY_001 - :status: mitigated - :links: REQ_003, REQ_007 - :mitigation: The Kiln implements bounded execution using the fuel mechanism (REQ_003, REQ_007), ensuring that execution will always yield back control flow after a configurable number of operations. - - A WebAssembly module could enter an infinite loop, causing the host system to become unresponsive or consume excessive resources. - -.. safety:: Memory Access Violations - :id: SAFETY_002 - :status: mitigated - :links: REQ_018 - :mitigation: The Kiln implements strict memory bounds checking as part of the WebAssembly specification compliance. All memory accesses are validated before execution. - - Improper memory access could lead to data corruption or system crashes. - -.. safety:: Resource Exhaustion - :id: SAFETY_003 - :status: mitigated - :links: REQ_014, REQ_024 - :mitigation: The Kiln implements resource limits and tracking, ensuring that memory allocation is bounded and monitored. The efficient operand stack implementation (REQ_024) minimizes memory overhead. - - A WebAssembly module could exhaust system resources such as memory. - -.. safety:: Interface Type Mismatch - :id: SAFETY_004 - :status: mitigated - :links: REQ_014, REQ_019 - :mitigation: The Kiln strictly validates type compatibility as part of the Component Model implementation. Interface types are checked during component instantiation. - - Type mismatches at component interfaces could lead to incorrect data interpretation and potentially unsafe operations. - -Risk Assessment ---------------- - -This section assesses the risk of each identified hazard. - -.. list-table:: Risk Assessment Matrix - :widths: 30 20 20 30 - :header-rows: 1 - - * - Hazard - - Severity - - Probability - - Risk Level - * - Unbounded Execution (SAFETY_001) - - High - - Low - - Medium - * - Memory Access Violations (SAFETY_002) - - High - - Low - - Medium - * - Resource Exhaustion (SAFETY_003) - - Medium - - Medium - - Medium - * - Interface Type Mismatch (SAFETY_004) - - Medium - - Low - - Low - -Mitigation Strategies ---------------------- - -Summary of hazards and their mitigation status: - -.. needtable:: - :columns: id;title;status;links - :filter: id in ['SAFETY_001', 'SAFETY_002', 'SAFETY_003', 'SAFETY_004'] - -Safety Validation ------------------ - -The following validation activities are required to ensure safety properties: - -1. **Testing of Bounded Execution** - - Verify that fuel consumption mechanism correctly limits execution - - Test with modules containing infinite loops - - Verify deterministic behavior when execution is resumed - -2. **Memory Safety Testing** - - Test memory access at boundaries - - Verify out-of-bounds access is properly trapped - - Validate memory growth constraints - -3. **Resource Monitoring** - - Test memory allocation limits - - Verify proper cleanup of resources - - Validate that peak memory usage is accurately tracked - -4. **Interface Type Validation** - - Test type validation with malformed components - - Verify correct validation of interface types - - Test with boundary conditions for complex types - -Safety Requirement Relationships --------------------------------- - -The following diagram shows the relationships between safety hazards and their mitigating requirements: - -.. needflow:: - :filter: id in ['SAFETY_001', 'SAFETY_002', 'SAFETY_003', 'SAFETY_004', 'REQ_001', 'REQ_003', 'REQ_007', 'REQ_014', 'REQ_018', 'REQ_019', 'REQ_024'] - :show_link_names: \ No newline at end of file diff --git a/docs/source/qualification/traceability_matrix.rst b/docs/source/qualification/traceability_matrix.rst deleted file mode 100644 index d37a9545d..000000000 --- a/docs/source/qualification/traceability_matrix.rst +++ /dev/null @@ -1,72 +0,0 @@ -Traceability Matrix -=================== - -This document provides traceability between requirements, specifications, implementations, and test cases. - -Overview --------- - -The traceability matrix maps relationships between different artifact types to ensure complete requirements coverage and verification. - -Requirements to Specifications ------------------------------- - -This section shows how requirements are addressed by specifications. - -.. needflow:: - :types: req, spec - :show_link_names: - -Specifications to Implementations ---------------------------------- - -This section shows how specifications are implemented. - -.. needflow:: - :types: spec, impl - :show_link_names: - -Safety Requirements Tracing ---------------------------- - -This section specifically traces safety requirements to their implementations. - -.. needflow:: - :types: req, spec, impl, safety - :show_link_names: - -Complete Requirement Coverage ------------------------------ - -This table shows the complete mapping of requirements to their corresponding specifications and implementations. - -.. needtable:: - :columns: id;title;status;links - :filter: type == "req" - -All Specifications ------------------- - -This table lists all specifications and their implementation status. - -.. needtable:: - :columns: id;title;status;links - :filter: type == "spec" - -All Implementations -------------------- - -This table lists all implementation details. - -.. needtable:: - :columns: id;title;status;links - :filter: type == "impl" - -Qualification Requirements Coverage ------------------------------------ - -This section shows the traceability for qualification-specific requirements. - -.. needtable:: - :columns: id;title;status;links - :filter: id in ['QUAL_001', 'QUAL_002', 'QUAL_003', 'QUAL_004', 'QUAL_005', 'QUAL_006', 'QUAL_007', 'QUAL_008'] \ No newline at end of file diff --git a/docs/source/requirements.rst b/docs/source/requirements.rst deleted file mode 100644 index f74020b4d..000000000 --- a/docs/source/requirements.rst +++ /dev/null @@ -1,342 +0,0 @@ -Requirements -============ - -This section contains the requirements for the Kiln project. - -Functional Requirements ------------------------ - -.. req:: Platform Abstraction Layer - :id: REQ_PLATFORM_001 - :status: implemented - - The runtime shall provide a platform abstraction layer (PAL) with distinct backends - for target operating systems (macOS, Linux, QNX, Zephyr) and bare-metal environments, - selectable via compile-time features. The PAL shall abstract OS-specific APIs for - memory allocation/protection and synchronization primitives (futex-like operations). - -.. req:: Resumable Interpreter - :id: REQ_FUNC_001 - :status: implemented - - The interpreter shall be resumable, allowing operation with fuel or other implementations of bounded run-time that require the interpreter to be halted and later resumed as if it was not halted. - -.. req:: Baremetal Support - :id: REQ_FUNC_002 - :status: implemented - - The interpreter shall be executable on bare-metal environments with no reliance on any specific functionality from the provided execution environment, as it shall be ready for embedding to any environment that Rust can compile for. - -.. req:: Bounded Execution - :id: REQ_FUNC_003 - :status: implemented - - The interpreter shall yield back control flow eventually, allowing users to call the interpreter with a bound and expect a result in a finite amount of time or bytecode operations, even if the bytecode itself never finishes execution. - -.. req:: State Migration - :id: REQ_FUNC_004 - :status: planned - - The interpreter state shall be able to halt on one computer and continue execution on another, enabling various workflows in deployments of multiple computers for load-balancing or redundancy purposes. - -.. req:: WebAssembly Component Model Support - :id: REQ_FUNC_014 - :status: partial - - The interpreter shall implement the WebAssembly Component Model Preview 2 specification, including: - - Component model validation - - Resource type handling - - Interface types - - Component instantiation and linking - - Resource lifetime management (see REQ_CMP_020, status: active) - - Custom section handling - - Component model binary format parsing - -.. req:: Component Model Binary Format - :id: REQ_FUNC_021 - :status: partial - :links: REQ_FUNC_014 - - The interpreter shall strictly implement the WebAssembly Component Model binary format as specified in - the official WebAssembly Component Model specification at - https://github.com/WebAssembly/component-model/blob/main/design/mvp/Binary.md, including: - - - Magic bytes (0x00, 0x61, 0x73, 0x6D) followed by version (0x0D, 0x00, 0x01, 0x00) - - Component sections with proper section IDs - - Type section encoding with canonical type representation - - Import section handling with component, instance, and function imports - - Core module sections including validation and embedding - - Component instances section with proper instance creation - - Export section with named exports and index references - - Component custom sections for metadata and tooling - - Canonical ABI encoding/decoding for interface values - - LEB128 encoding for integers and field counts - -.. req:: WASI Logging Support - :id: REQ_FUNC_015 - :status: implemented - - The interpreter shall implement the WASI logging API as specified in the wasi-logging proposal, providing: - - Support for all defined log levels (Error, Warn, Info, Debug, Trace) - - Context-based logging - - Stderr integration - - Thread-safe logging operations - -.. req:: Platform-Specific Logging - :id: REQ_FUNC_016 - :status: planned - :links: REQ_FUNC_015 - - The WASI logging implementation shall provide platform-specific backends: - - Linux: syslog integration with proper facility and priority mapping - - macOS: Unified Logging System (os_log) integration - - Generic fallback implementation for other platforms - -.. req:: WAST Test Suite Compatibility - :id: REQ_FUNC_022 - :status: partial - - The interpreter shall be testable against the official WebAssembly specification (WAST) test suite to ensure conformance and correctness. - -Low-Level Functional Requirements ---------------------------------- - -.. req:: Helper Runtime C ABI Exports - :id: REQ_HELPER_ABI_001 - :status: new - - The AOT helper runtime (`libkiln_helper`) shall export a stable C ABI including - functions for Wasm operations not efficiently inlined by the AOT compiler. - This shall include `kiln_memory_copy`, `kiln_memory_fill`, `kiln_memory_grow`, - `kiln_atomic_wait`, and `kiln_atomic_notify`. - -.. req:: Stackless Implementation - :id: REQ_LFUNC_005 - :status: implemented - :links: REQ_FUNC_001 - - The interpreter shall be stackless, storing the stack of the interpreted bytecode in a traditional data structure rather than using function calls in the host environment. - -.. req:: No Standard Library - :id: REQ_LFUNC_006 - :status: implemented - :links: REQ_FUNC_002 - - The interpreter shall be implemented in no_std Rust, only relying on functionality provided by no_std to enable execution on bare environments where no operating system is available. - -.. req:: Fuel Mechanism - :id: REQ_LFUNC_007 - :status: implemented - :links: REQ_FUNC_003 - - The interpreter shall support fuel bounded execution, where each bytecode instruction is associated with a specific amount of fuel consumed during execution. - -.. req:: State Serialization - :id: REQ_LFUNC_008 - :status: planned - :links: REQ_FUNC_004 - - The interpreter state shall be de-/serializable to enable migration to other computers and support check-point/lock-step execution. - -.. req:: WebAssembly Core Implementation - :id: REQ_LFUNC_018 - :status: partial - :links: REQ_FUNC_014 - - The interpreter shall implement the WebAssembly Core specification, including: - - Module validation (see REQ_WASM_001 in safety_requirements.rst, status: active) - - Value types and reference types - - Instructions and control flow - - Function calls and tables - - Memory and data segments - - Global variables - - Exception handling - - SIMD operations - - Threading support - -.. req:: Component Model Implementation - :id: REQ_LFUNC_019 - :status: partial - :links: REQ_FUNC_014 - - The interpreter shall implement the Component Model specification, including: - - WIT format parsing and validation - - Component model binary format parsing - - Resource type implementation - - Interface type handling - - Component instantiation - - Component linking - - Resource lifetime management - -.. req:: Optimized Instruction Dispatch - :id: REQ_LFUNC_023 - :status: planned - :links: REQ_LFUNC_005 - - The core instruction dispatch loop within the stackless engine shall be specifically optimized for execution speed. Techniques such as efficient instruction decoding, minimizing branching overhead, or platform-specific optimizations (where compatible with certifiability) should be considered. - -.. req:: Efficient Operand Stack Implementation - :id: REQ_LFUNC_024 - :status: planned - :links: REQ_LFUNC_005 - - The stackless operand stack implementation (`StacklessStack` or equivalent) shall be designed and optimized for efficient push/pop operations, minimal memory overhead, and robust handling of potential overflow conditions suitable for the target `no_std` environments. - -.. req:: Efficient Branch Pre-calculation - :id: REQ_LFUNC_025 - :status: planned - :links: REQ_LFUNC_005, REQ_LFUNC_018 - - The pre-calculation of branch targets (e.g., `label.continuation` values) shall be performed efficiently, ideally integrated with the module validation or loading process, to minimize runtime startup costs. - -.. req:: Minimize Code Complexity for Certification - :id: REQ_LFUNC_026 - :status: planned - :links: REQ_OBS_012, REQ_OBS_013 - - To enhance certifiability and maintainability, the Kiln interpreter codebase shall strive for simplicity, minimize the use of complex language features (e.g., procedural macros), and restrict external dependencies to those strictly necessary for core functionality or explicitly required features (like logging or `no_std` math). - -Dependency Requirements ------------------------ - -.. req:: Logging Support - :id: REQ_DEP_009 - :status: implemented - - The interpreter shall have an optional dependency on the ``log`` crate version ``0.4.22`` for observability and debugging purposes. - -.. req:: Math Library - :id: REQ_DEP_010 - :status: planned - - The interpreter may depend on the ``libm`` crate version ``0.2.8`` for floating-point operations required in no_std environments. - -.. req:: Rust Version - :id: REQ_DEP_011 - :status: implemented - - The interpreter shall compile on Rust ``1.76.0`` and later versions. - - -Observability Requirements --------------------------- - -.. req:: Instrumentation Support - :id: REQ_OBS_012 - :status: partial - - The interpreter shall implement means for instrumentation to support certification evidence generation, debugging, and run-time monitoring. - -.. req:: Coverage Measurement - :id: REQ_OBS_013 - :status: partial - :links: REQ_OBS_012 - - The instrumentation shall enable the measurement of: - - - Statement coverage (DO-178C DAL-C) - - Decision coverage (DO-178C DAL-B) - - Modified condition/decision coverage (DO-178C DAL-A) - -Advanced Runtime Requirements ------------------------------ - -.. req:: Async/Await Runtime Support - :id: REQ_FUNC_030 - :status: implemented - - The interpreter shall provide comprehensive async/await runtime support for WebAssembly Component Model, including: - - Async canonical lifting and lowering - - Async execution engine with future-based task management - - Async resource cleanup and lifecycle management - - Runtime bridge for async-to-sync interoperability - - Context preservation across async boundaries - -.. req:: Advanced Threading Support - :id: REQ_FUNC_031 - :status: partial - - The interpreter shall implement advanced threading capabilities including: - - Task manager with cancellation support - - Thread spawning with fuel-based resource control - - Waitable set primitives for thread synchronization - - Thread-safe builtin operations - - Integration with platform-specific threading backends - -.. req:: Debug Infrastructure - :id: REQ_FUNC_032 - :status: implemented - - The interpreter shall provide comprehensive debugging capabilities including: - - DWARF debug information parsing and processing - - WIT-aware debugging with source mapping - - Runtime breakpoint management - - Stack trace generation with source information - - Memory inspection and variable examination - - Step-by-step execution control - -.. req:: Fuzzing Infrastructure - :id: REQ_QA_010 - :status: implemented - - The interpreter shall include comprehensive fuzzing infrastructure covering: - - Bounded collections fuzzing (stack, vec, queue) - - Memory adapter and safe memory fuzzing - - Component model parser fuzzing - - Type bounds and canonical options fuzzing - - WIT parser fuzzing - - Continuous fuzzing integration - -.. req:: Multiple Runtime Modes - :id: REQ_FUNC_033 - :status: implemented - - The interpreter shall support multiple runtime deployment modes through the kilnd daemon: - - Standard mode (kilnd-std) with full standard library support - - Allocation mode (kilnd-alloc) for embedded systems with heap - - No-std mode (kilnd-nostd) for pure bare-metal deployment - - Each mode with appropriate resource limits and safety constraints - -.. req:: Hardware Optimization Support - :id: REQ_PERF_010 - :status: implemented - - The interpreter shall support platform-specific hardware optimizations including: - - SIMD acceleration for supported architectures (x86_64, aarch64) - - ARM Memory Tagging Extension (MTE) for spatial memory safety - - Intel Control-flow Enforcement Technology (CET) integration - - Hardware-accelerated atomic operations - - CPU-specific instruction scheduling optimizations - -.. req:: Formal Verification Support - :id: REQ_VERIFY_010 - :status: implemented - - The interpreter shall include support for formal verification through: - - Kani proof harness integration - - Model checking annotations - - Invariant specifications - - Bounded verification for critical paths - - Integration with verification registry - -Implementation Status ---------------------- - -.. needtable:: - :columns: id;title;status - :filter: type == 'req' - -Requirement Relationships -------------------------- - -.. needflow:: - :filter: id in ['REQ_PLATFORM_001', 'REQ_HELPER_ABI_001', 'REQ_FUNC_001', 'REQ_FUNC_002', 'REQ_FUNC_003', 'REQ_FUNC_004', 'REQ_LFUNC_005', 'REQ_LFUNC_006', 'REQ_LFUNC_007', 'REQ_LFUNC_008', 'REQ_DEP_009', 'REQ_DEP_010', 'REQ_DEP_011', 'REQ_OBS_012', 'REQ_OBS_013', 'REQ_FUNC_014', 'REQ_FUNC_015', 'REQ_FUNC_016', 'REQ_LFUNC_018', 'REQ_LFUNC_019', 'REQ_CMP_020', 'REQ_FUNC_021', 'REQ_FUNC_022', 'REQ_LFUNC_023', 'REQ_LFUNC_024', 'REQ_LFUNC_025', 'REQ_LFUNC_026'] - -Component Model Requirements ----------------------------- - -.. req:: Component Resource Lifecycle Management - :id: REQ_CMP_020 - :status: active - - The WebAssembly component model implementation shall provide comprehensive lifecycle management for resource types, ensuring proper creation, tracking, and disposal of resources. \ No newline at end of file diff --git a/docs/source/requirements/asil_a_requirements.rst b/docs/source/requirements/asil_a_requirements.rst deleted file mode 100644 index e8c7d3d90..000000000 --- a/docs/source/requirements/asil_a_requirements.rst +++ /dev/null @@ -1,237 +0,0 @@ -======================= -ASIL-A Requirements -======================= - -This document defines the specific requirements for achieving ASIL-A compliance per ISO 26262. - -.. contents:: On this page - :local: - :depth: 2 - -ASIL-A Overview ---------------- - -ASIL-A is the lowest safety integrity level in ISO 26262, suitable for functions where failure poses minimal risk to vehicle occupants. The Kiln project targets ASIL-A as the initial safety certification level. - -**Key ASIL-A Requirements:** -- Basic hazard analysis and risk assessment -- Systematic development process -- Basic verification and validation -- Fault detection capability -- Quality management system - -Memory Safety Requirements (ASIL-A) ------------------------------------- - -REQ_ASIL_A_MEM_001: Memory Allocation Safety -~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ -**ID:** REQ_ASIL_A_MEM_001 -**Title:** Capability-Based Memory Allocation -**Priority:** High -**Status:** Implemented - -**Requirement:** -The Kiln runtime SHALL use capability-based memory allocation to prevent unauthorized memory access and ensure deterministic memory usage patterns. - -**Implementation:** -- Located in: `/kiln-foundation/src/capabilities/` -- Verified by: KANI harness `kani_verify_memory_budget_never_exceeded` -- Test coverage: Memory allocation tests in `kiln-foundation/tests/` - -**Rationale:** -Capability-based allocation provides the deterministic memory management required for ASIL-A certification while preventing common memory safety issues. - -REQ_ASIL_A_MEM_002: Memory Budget Enforcement -~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ -**ID:** REQ_ASIL_A_MEM_002 -**Title:** Compile-Time Memory Budget Verification -**Priority:** High -**Status:** Implemented - -**Requirement:** -The Kiln runtime SHALL enforce memory budgets at compile-time to prevent memory exhaustion during runtime execution. - -**Implementation:** -- Located in: `/kiln-foundation/src/budget_verification.rs` -- Macros: `safe_managed_alloc!` with budget checking -- Configuration: `CRATE_BUDGETS` constant arrays - -**Verification:** -- KANI harness: `kani_verify_hierarchical_budget_consistency` -- Build-time verification through `cargo-kiln` tool - -REQ_ASIL_A_MEM_003: No Dynamic Memory Allocation -~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ -**ID:** REQ_ASIL_A_MEM_003 -**Title:** Static Memory Layout Enforcement -**Priority:** High -**Status:** Partially Implemented - -**Requirement:** -The Kiln runtime SHALL NOT perform dynamic memory allocation during execution in safety-critical contexts. - -**Implementation:** -- `NoStdProvider` using fixed-size arrays -- Bounded collections with compile-time capacity limits -- `#![no_std]` compilation for safety-critical targets - -**Gap Analysis:** -- Global capability context still uses `HashMap` in std mode -- Needs static array replacement for full compliance - -Error Handling Requirements (ASIL-A) -------------------------------------- - -REQ_ASIL_A_ERR_001: Systematic Error Classification -~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ -**ID:** REQ_ASIL_A_ERR_001 -**Title:** ASIL-Level Error Classification -**Priority:** Medium -**Status:** Implemented - -**Requirement:** -The Kiln runtime SHALL classify all errors according to their ASIL level and handle them appropriately. - -**Implementation:** -- Located in: `/kiln-error/src/asil.rs` -- Enum: `AsilLevel` with QM through ASIL-D levels -- Error classification in `Error` struct - -**Verification:** -- Tests in: `/kiln-error/tests/asil_tests.rs` -- ASIL-tagged test framework - -REQ_ASIL_A_ERR_002: Fault Detection Coverage -~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ -**ID:** REQ_ASIL_A_ERR_002 -**Title:** Basic Fault Detection Mechanisms -**Priority:** Medium -**Status:** In Progress - -**Requirement:** -The Kiln runtime SHALL detect and respond to basic fault conditions including memory violations and resource exhaustion. - -**Implementation Plan:** -- Memory bounds checking in all allocations -- Resource limit monitoring -- Graceful degradation on fault detection - -Verification Requirements (ASIL-A) ------------------------------------ - -REQ_ASIL_A_VER_001: Formal Verification Coverage -~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ -**ID:** REQ_ASIL_A_VER_001 -**Title:** KANI Formal Verification for Critical Paths -**Priority:** High -**Status:** Implemented - -**Requirement:** -The Kiln runtime SHALL use formal verification (KANI) to prove correctness of safety-critical memory operations. - -**Implementation:** -- KANI configuration: `/kiln-tests/integration/Kani.toml` -- Verification profiles for each ASIL level -- 7+ existing KANI harnesses for memory operations - -**Target Coverage:** -- Memory allocation and deallocation -- Capability verification logic -- Budget enforcement mechanisms -- Atomic operations and synchronization - -REQ_ASIL_A_VER_002: Test Coverage Requirements -~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ -**ID:** REQ_ASIL_A_VER_002 -**Title:** Systematic Test Coverage for ASIL-A Components -**Priority:** Medium -**Status:** In Progress - -**Requirement:** -The Kiln runtime SHALL achieve comprehensive test coverage for all ASIL-A classified components with systematic boundary testing. - -**Target Metrics:** -- Line coverage: ≥95% for safety-critical paths -- Branch coverage: ≥90% for decision points -- MC/DC coverage: ≥85% for complex Boolean expressions - -Process Requirements (ASIL-A) ------------------------------- - -REQ_ASIL_A_PROC_001: Safety Development Lifecycle -~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ -**ID:** REQ_ASIL_A_PROC_001 -**Title:** ISO 26262 Compliant Development Process -**Priority:** High -**Status:** In Progress - -**Requirement:** -The Kiln runtime development SHALL follow ISO 26262 safety development lifecycle processes. - -**Implementation Plan:** -- Safety requirements specification (this document) -- Hazard analysis and risk assessment -- Safety case development -- Verification and validation procedures - -REQ_ASIL_A_PROC_002: Change Control Process -~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ -**ID:** REQ_ASIL_A_PROC_002 -**Title:** Safety-Critical Code Change Management -**Priority:** Medium -**Status:** Planned - -**Requirement:** -All changes to safety-critical Kiln components SHALL be subject to controlled change management with safety impact assessment. - -**Implementation Plan:** -- Git-based change tracking -- Safety review process for critical components -- Regression testing requirements - -Gap Analysis for ASIL-A Compliance ------------------------------------ - -**Critical Gaps (Must Fix):** - -1. **Dynamic Memory in std Mode** - - Issue: Global capability context uses `HashMap` - - Fix: Replace with static arrays - - Timeline: Week 4-5 - -2. **Incomplete Fault Detection** - - Issue: Limited fault detection mechanisms - - Fix: Implement systematic fault detection - - Timeline: Week 5-6 - -**Minor Gaps (Should Fix):** - -1. **Documentation Completeness** - - Issue: Some safety requirements lack detailed implementation links - - Fix: Complete traceability matrix - - Timeline: Week 7-8 - -2. **Process Documentation** - - Issue: Safety development process needs formalization - - Fix: Create process documentation - - Timeline: Week 6-8 - -Compliance Status Summary -------------------------- - -**Ready for ASIL-A:** -- ✅ Capability-based memory system -- ✅ Formal verification infrastructure (KANI) -- ✅ Error classification system -- ✅ Budget enforcement mechanisms - -**Needs Work for ASIL-A:** -- 🔄 Complete elimination of dynamic allocation -- 🔄 Systematic fault detection implementation -- 🔄 Process documentation completion -- 🔄 Full test coverage achievement - -**Timeline to ASIL-A Readiness:** -- **Week 4-6:** Technical gap resolution -- **Week 7-8:** Process and documentation completion -- **Week 9-10:** Independent review and assessment diff --git a/docs/source/requirements/functional.rst b/docs/source/requirements/functional.rst deleted file mode 100644 index 4773aff58..000000000 --- a/docs/source/requirements/functional.rst +++ /dev/null @@ -1,95 +0,0 @@ -======================= -Functional Requirements -======================= - -.. image:: ../_static/icons/functional.svg - :width: 64px - :align: right - :alt: Functional Requirements Icon - -This document defines the functional requirements for PulseEngine (Kiln Edition). These requirements specify what the system should do to accomplish its mission. - -.. contents:: On this page - :local: - :depth: 2 - -Functional Requirements Status ------------------------------- - -.. - Pie chart temporarily removed due to syntax issues - - .. needpie:: - :labels: Active, Implemented, Not Started - :status: id =~ "REQ_[^S].*" and status != "removed" and id !~ "REQ_SAFETY_.*|REQ_MEM_SAFETY_.*|REQ_VERIFY_.*|REQ_RESOURCE_.*" - -WebAssembly Core Requirements ------------------------------ - -.. commenting out needfilters until they can be fixed -.. -.. .. needfilter:: -.. :filter: id =~ "REQ_CORE_.*" -.. :style: table -.. :columns: id, title, status - -Platform Requirements ---------------------- - -Component Model Requirements ----------------------------- - -.. commenting out needfilters until they can be fixed -.. -.. .. needfilter:: -.. :filter: id =~ "REQ_COMP_.*" -.. :style: table -.. :columns: id, title, status - -Performance Requirements ------------------------- - -.. commenting out needfilters until they can be fixed -.. -.. .. needfilter:: -.. :filter: id =~ "REQ_PERF_.*" -.. :style: table -.. :columns: id, title, status - -Error Handling Requirements ---------------------------- - -.. commenting out needfilters until they can be fixed -.. -.. .. needfilter:: -.. :filter: id =~ "REQ_ERROR_.*" -.. :style: table -.. :columns: id, title, status - -API Requirements ----------------- - -.. commenting out needfilters until they can be fixed -.. -.. .. needfilter:: -.. :filter: id =~ "REQ_API_.*" -.. :style: table -.. :columns: id, title, status - -Quality Assurance Requirements ------------------------------- - -.. commenting out needfilters until they can be fixed -.. -.. .. needfilter:: -.. :filter: id =~ "REQ_QA_.*" -.. :style: table -.. :columns: id, title, status - -Implementation Details ----------------------- - -For information on how these functional requirements are implemented, see: - -* :doc:`../architecture` - System architecture -* :doc:`../api/index` - API documentation \ No newline at end of file diff --git a/docs/source/requirements/index.rst b/docs/source/requirements/index.rst deleted file mode 100644 index 4c2aa0031..000000000 --- a/docs/source/requirements/index.rst +++ /dev/null @@ -1,74 +0,0 @@ -====================== -Requirements Dashboard -====================== - -.. image:: ../_static/icons/requirements.svg - :width: 64px - :align: right - :alt: Requirements Icon - -This section provides a consolidated view of all system requirements and their status. Use this dashboard to track implementation progress and relationships between different requirement types. - -.. contents:: On this page - :local: - :depth: 2 - -Requirements Overview ---------------------- - -The following charts provide an overview of requirements status by category: - -Functional Requirements -~~~~~~~~~~~~~~~~~~~~~~~ - -.. commenting out needpie directives until they can be fixed -.. -.. .. needpie:: -.. :labels: Implemented, Partial, Not Started -.. :filter: id =~ "REQ_[^S].*" and status != "removed" - -Safety Requirements -~~~~~~~~~~~~~~~~~~~ - -.. commenting out needpie directives until they can be fixed -.. -.. .. needpie:: -.. :labels: Implemented, Partial, Not Started -.. :filter: id =~ "REQ_SAFETY.*|REQ_MEM_SAFETY.*|REQ_VERIFY.*|REQ_RESOURCE.*" and status != "removed" - -Qualification Requirements -~~~~~~~~~~~~~~~~~~~~~~~~~~ - -.. commenting out needpie directives until they can be fixed -.. -.. .. needpie:: -.. :labels: Implemented, Partial, Not Started -.. :filter: id =~ "QUAL_.*" and status != "removed" - -Implementation Status ---------------------- - -This table shows the implementation status of all requirements: - -.. needtable:: - :columns: id;title;status;implementation_status - :filter: id.startswith("REQ_") or id.startswith("QUAL_") - :style: table - -Traceability Matrix -------------------- - -The following matrix shows the relationships between requirements, specifications, implementations, and tests: - -.. needflow:: - :filter: id.startswith("REQ_") or id.startswith("SPEC_") or id.startswith("IMPL_") or id.startswith("T_") - :show_legend: - -Key Requirements ----------------- - -The following are the key requirements driving the PulseEngine design: - -.. needtable:: - :columns: id;title;status - :filter: id in ['REQ_SAFETY_001', 'REQ_SAFETY_002', 'REQ_MEM_SAFETY_001', 'REQ_RESOURCE_001', 'REQ_WASM_001', 'REQ_CODE_QUALITY_001'] \ No newline at end of file diff --git a/docs/source/requirements/qualification.rst b/docs/source/requirements/qualification.rst deleted file mode 100644 index e14304881..000000000 --- a/docs/source/requirements/qualification.rst +++ /dev/null @@ -1,73 +0,0 @@ -========================== -Qualification Requirements -========================== - -.. image:: ../_static/icons/qualification.svg - :width: 64px - :align: right - :alt: Qualification Requirements Icon - -This document defines the qualification requirements for PulseEngine (Kiln Edition). These requirements specify how the system must be qualified for use in safety-critical applications. - -.. contents:: On this page - :local: - :depth: 2 - -Status Overview ---------------- - -.. commenting out needpie directives until they can be fixed -.. -.. .. needpie:: -.. :labels: Active, Implemented, Not Started -.. :filter: id =~ "QUAL_.*" and status != "removed" - -Documentation Requirements --------------------------- - -.. commenting out needfilter directives until they can be fixed -.. -.. .. needfilter:: -.. :filter: id =~ "QUAL_DOCS_.*" -.. :style: table -.. :columns: id, title, status - -Testing Requirements --------------------- - -.. commenting out needfilter directives until they can be fixed -.. -.. .. needfilter:: -.. :filter: id =~ "QUAL_TEST_.*" -.. :style: table -.. :columns: id, title, status - -Safety Verification Requirements --------------------------------- - -.. commenting out needfilter directives until they can be fixed -.. -.. .. needfilter:: -.. :filter: id =~ "QUAL_SAFETY_.*" -.. :style: table -.. :columns: id, title, status - -Panic Documentation -------------------- - -The following table shows all documented panic points in the system: - -.. needtable:: - :columns: id;title;item_status;safety_impact - :filter: id.startswith("KILNQ-") - :style: table - -Qualification Documentation ---------------------------- - -For more information on qualification materials, see: - -* :doc:`../qualification/index` - Qualification overview -* :doc:`../qualification/plan` - Qualification plan -* :doc:`../qualification/safety_analysis` - Safety analysis report -* :doc:`../qualification/panic_registry` - Panic registry \ No newline at end of file diff --git a/docs/source/requirements/safety.rst b/docs/source/requirements/safety.rst deleted file mode 100644 index f609a35bc..000000000 --- a/docs/source/requirements/safety.rst +++ /dev/null @@ -1,103 +0,0 @@ -=================== -Safety Requirements -=================== - -.. image:: ../_static/icons/safety_features.svg - :width: 64px - :align: right - :alt: Safety Features Icon - -This document defines the safety, resource management, and verification requirements for the Kiln runtime. It consolidates all safety-related requirements in one place for easier tracking and management. - -.. contents:: On this page - :local: - :depth: 2 - -Status Overview ---------------- - -.. commenting out needpie directives until they can be fixed -.. -.. .. needpie:: -.. :labels: Active, Implemented, Not Started -.. :filter: id =~ "REQ_SAFETY_.*" and status != "removed" - -Safety Core Requirements ------------------------- - -.. commenting out needfilter directives until they can be fixed -.. -.. .. needfilter:: -.. :filter: id =~ "REQ_SAFETY_.*" -.. :style: table -.. :columns: id, title, status - -Memory Safety Requirements --------------------------- - -.. commenting out needfilter directives until they can be fixed -.. -.. .. needfilter:: -.. :filter: id =~ "REQ_MEM_SAFETY_.*" -.. :style: table -.. :columns: id, title, status - -Resource Management -------------------- - -.. commenting out needfilter directives until they can be fixed -.. -.. .. needfilter:: -.. :filter: id =~ "REQ_RESOURCE_.*" -.. :style: table -.. :columns: id, title, status - -Verification Requirements -------------------------- - -.. commenting out needfilter directives until they can be fixed -.. -.. .. needfilter:: -.. :filter: id =~ "REQ_VERIFY_.*" -.. :style: table -.. :columns: id, title, status - -WebAssembly Safety Requirements -------------------------------- - -.. commenting out needfilter directives until they can be fixed -.. -.. .. needfilter:: -.. :filter: id =~ "REQ_WASM_.*" -.. :style: table -.. :columns: id, title, status - -Code Quality Requirements -------------------------- - -.. commenting out needfilter directives until they can be fixed -.. -.. .. needfilter:: -.. :filter: id =~ "REQ_CODE_QUALITY_.*" -.. :style: table -.. :columns: id, title, status - -Build and Environment Requirements ----------------------------------- - -.. commenting out needfilter directives until they can be fixed -.. -.. .. needfilter:: -.. :filter: id =~ "REQ_BUILD_.*|REQ_ENV_.*|REQ_INSTALL_.*" -.. :style: table -.. :columns: id, title, status - -Related Documentation ---------------------- - -For more information on how these safety requirements are implemented and verified, see: - -* :doc:`../safety/index` - Safety documentation overview -* :doc:`../safety/mechanisms` - Safety mechanism implementations -* :doc:`../safety/test_cases` - Safety test cases -* :doc:`../safety/constraints` - Safety constraints \ No newline at end of file diff --git a/docs/source/safety_manual/mechanisms.rst b/docs/source/safety_manual/mechanisms.rst deleted file mode 100644 index 14eeb33b4..000000000 --- a/docs/source/safety_manual/mechanisms.rst +++ /dev/null @@ -1,519 +0,0 @@ -================== -Safety Mechanisms -================== - -.. image:: ../_static/icons/safety_features.svg - :width: 64px - :align: right - :alt: Safety Mechanisms Icon - -This document consolidates all safety mechanisms implemented in PulseEngine (Kiln Edition) to satisfy safety requirements and protect against systematic and random faults. - -.. warning:: - **Implementation Note**: Safety mechanisms must be configured according to the - target ASIL level. See :doc:`configuration` for ASIL-specific configuration guidance. - -.. contents:: On this page - :local: - :depth: 2 - -Overview -======== - -Mechanism Categories --------------------- - -Safety mechanisms are organized by the fault types they address: - -1. **Memory Safety Mechanisms** - Prevent memory corruption and access violations -2. **Control Flow Integrity** - Protect execution flow from hijacking -3. **Resource Protection** - Prevent resource exhaustion and starvation -4. **Temporal Safety** - Ensure timing constraints and prevent lockups -5. **Data Integrity** - Protect data from corruption and tampering -6. **Fault Detection** - Identify and report fault conditions -7. **Error Recovery** - Restore safe operation after faults - -Mechanism Attributes --------------------- - -Each mechanism includes: - -- **ID**: Unique identifier (SAFETY_CATEGORY_NNN) -- **Detection**: Fault detection capability and coverage -- **Reaction**: Response to detected faults -- **ASIL**: Required for ASIL levels (A, B, C, D) -- **Diagnostic Coverage**: Percentage of faults detected - -Memory Safety Mechanisms -======================== - -.. safety:: Memory Bounds Checking - :id: SAFETY_MEM_001 - :detection: 100% of out-of-bounds accesses - :reaction: Reject access, return error - :asil: A, B, C, D - :diagnostic_coverage: 99% - - **Description**: The runtime validates all memory accesses against allocation boundaries before - execution. The system checks both base address and offset+length. - - **Implementation**: - - SafeSlice wrapper enforces bounds on all slice operations - - Integer overflow detection in offset calculations - - Dual-check strategy: pre-access and in-access validation - - Zero-cost abstraction in release builds with bounds elision - - **Configuration**: - - Always enabled in safety-critical mode - - Performance mode allows selective bounds elision - - Configurable trap vs. error return behavior - -.. safety:: Memory Isolation Barriers - :id: SAFETY_MEM_002 - :detection: 100% of cross-module access attempts - :reaction: Block access, signal violation - :asil: C, D - :diagnostic_coverage: 99% - - **Description**: The runtime isolates WebAssembly modules in separate memory spaces with no - shared mutable state except through validated interfaces. - - **Implementation**: - - Separate linear memory per module instance - - No direct memory sharing between modules - - Explicit import/export validation - - Hardware memory protection when available (Memory Protection Unit/Memory Management Unit) - - **Integration Requirements**: - - Platform must provide memory protection unit - - Minimum 4KB page granularity required - -.. safety:: Stack Overflow Protection - :id: SAFETY_MEM_003 - :detection: 95% of stack overflows before corruption - :reaction: Terminate execution, report error - :asil: B, C, D - :diagnostic_coverage: 90% - - **Description**: The runtime monitors and limits stack usage to prevent overflow into - adjacent memory regions. - - **Implementation**: - - Stack depth counter with configurable limit - - Guard pages when platform supports - - Stack canary values for corruption detection - - Pre-allocation of maximum stack space - - **Limitations**: - - Cannot detect all forms of stack corruption - - Guard pages require platform support - -.. safety:: Memory Initialization Enforcement - :id: SAFETY_MEM_004 - :detection: 100% of uninitialized access attempts - :reaction: Initialize to safe default or trap - :asil: A, B, C, D - :diagnostic_coverage: 100% - - **Description**: All memory is initialized before use to prevent information leakage - and undefined behavior. - - **Implementation**: - - Zero-initialization of linear memory on allocation - - Explicit initialization tracking for tables - - Trap on access to uninitialized table elements - - Safe default values for all types - -Control Flow Integrity Mechanisms -================================= - -.. safety:: Indirect Call Validation - :id: SAFETY_CFI_001 - :detection: 100% of invalid indirect calls - :reaction: Trap execution, report violation - :asil: C, D - :diagnostic_coverage: 100% - - **Description**: All indirect calls are validated against the function table before - execution to prevent control flow hijacking. - - **Implementation**: - - Type signature validation on every indirect call - - Function index bounds checking - - Table element initialization tracking - - No function pointer arithmetic allowed - - **Performance Impact**: - - ~5-10% overhead on indirect call heavy workloads - - Can be optimized with caching in performance mode - -.. safety:: Control Stack Integrity - :id: SAFETY_CFI_002 - :detection: >90% of control stack corruptions - :reaction: Terminate execution, safe state transition - :asil: D - :diagnostic_coverage: >85% - - **Description**: The control stack is protected against corruption through redundancy - and validation checks. - - **Implementation**: - - Shadow control stack with validation - - Return address encryption when supported - - Stack frame validation on unwind - - Structured control flow enforcement - - **Platform Requirements**: - - Hardware CET support provides additional protection - - Software-only mode available with reduced coverage - -Resource Protection Mechanisms -============================== - -.. safety:: Memory Quota Enforcement - :id: SAFETY_RESOURCE_001 - :detection: 100% of quota violations - :reaction: Deny allocation, return error - :asil: A, B, C, D - :diagnostic_coverage: 100% - - **Description**: Memory usage is limited per module with strict enforcement to prevent - resource exhaustion. - - **Implementation**: - - Per-module memory quotas (default 1MB, configurable) - - Allocation tracking with O(1) quota checks - - Hierarchical quotas for module groups - - No dynamic allocation after initialization in ASIL-D - - **Configuration**: - ```rust - const MAX_MEMORY_PAGES: u32 = 16; // 1MB with 64KB pages - const MEMORY_GROWTH_ENABLED: bool = false; // For ASIL-D - ``` - -.. safety:: Execution Fuel Limiting - :id: SAFETY_RESOURCE_002 - :detection: 100% of fuel exhaustion - :reaction: Controlled termination - :asil: B, C, D - :diagnostic_coverage: 100% - - **Description**: Execution is limited through a fuel mechanism to prevent infinite - loops and ensure bounded execution time. - - **Implementation**: - - Fuel consumption per instruction (configurable costs) - - Fuel checks at loop headers and function entries - - Interruptible execution for external timeout - - Deterministic fuel consumption for WCET analysis - - **Fuel Costs** (example): - - Basic arithmetic: 1 fuel - - Memory access: 2 fuel - - Function call: 10 fuel - - Indirect call: 15 fuel - -.. safety:: Table Size Limits - :id: SAFETY_RESOURCE_003 - :detection: 100% of limit violations - :reaction: Deny growth, return error - :asil: A, B, C, D - :diagnostic_coverage: 100% - - **Description**: Function and element tables are size-limited to prevent resource - exhaustion attacks. - - **Implementation**: - - Configurable maximum table size (default 10K elements) - - Pre-allocation in safety-critical mode - - Growth tracking and validation - - No dynamic table growth in ASIL-D - -Temporal Safety Mechanisms -========================== - -.. safety:: Watchdog Integration - :id: SAFETY_TEMPORAL_001 - :detection: 100% of deadline violations - :reaction: External watchdog reset - :asil: C, D - :diagnostic_coverage: 100% - - **Description**: Integration with external watchdog timer for detecting execution - lockups and deadline violations. - - **Implementation**: - - Periodic watchdog feeding during execution - - Configurable feeding intervals - - Execution checkpoint markers - - Clean shutdown on watchdog timeout warning - - **Integration Requirements**: - - System must provide watchdog with warning period - - Minimum 1ms warning before reset - -.. safety:: Bounded Loop Detection - :id: SAFETY_TEMPORAL_002 - :detection: >80% of potentially infinite loops - :reaction: Fuel-based termination - :asil: B, C, D - :diagnostic_coverage: >75% - - **Description**: Loops are monitored for bounded execution through static analysis - and runtime checks. - - **Implementation**: - - Loop fuel consumption tracking - - Loop iteration counting for simple loops - - Static analysis for loop bound inference - - Runtime validation of loop variants - -Data Integrity Mechanisms -========================= - -.. safety:: Type Safety Enforcement - :id: SAFETY_DATA_001 - :detection: 100% of type violations - :reaction: Trap execution - :asil: A, B, C, D - :diagnostic_coverage: 100% - - **Description**: WebAssembly type system is strictly enforced preventing type - confusion vulnerabilities. - - **Implementation**: - - Static type checking during validation - - Runtime type checks for indirect calls - - No type casts or unions allowed - - Memory is typed only as bytes - - **Guarantees**: - - No undefined behavior from type errors - - Predictable trap on type mismatch - -.. safety:: Data Flow Tracking - :id: SAFETY_DATA_002 - :detection: >90% of unauthorized data flows - :reaction: Block data transfer - :asil: C, D - :diagnostic_coverage: >85% - - **Description**: Information flow control prevents data leakage between different - criticality levels. - - **Implementation**: - - Taint tracking for high-criticality data - - Interface validation for data exports - - No implicit data sharing between modules - - Audit logging of data transfers - -Fault Detection Mechanisms -========================== - -.. safety:: Built-In Self Test (BIST) - :id: SAFETY_DETECT_001 - :detection: >95% of permanent faults - :reaction: Prevent operation, report failure - :asil: C, D - :diagnostic_coverage: 90% - - **Description**: Power-on and periodic self-tests verify correct operation of safety - mechanisms. - - **Implementation**: - - Memory pattern tests (walking 1s/0s) - - Arithmetic unit verification - - Control flow test patterns - - Safety mechanism verification - - **Test Schedule**: - - Power-on: Full test suite (~100ms) - - Periodic: Quick tests (~1ms every 100ms) - - On-demand: Full test via API - -.. safety:: Runtime Assertion Checking - :id: SAFETY_DETECT_002 - :detection: 100% of assertion violations - :reaction: Trap and diagnostic dump - :asil: A, B, C, D - :diagnostic_coverage: 100% - - **Description**: Critical invariants are continuously verified during execution with - immediate detection of violations. - - **Implementation**: - - Precondition checks on safety-critical functions - - Postcondition verification - - Invariant checks at key points - - Diagnostic information collection - - **Performance Mode**: - - Can be selectively disabled for QM components - - Always enabled for ASIL components - -Error Recovery Mechanisms -========================= - -.. safety:: Checkpoint and Rollback - :id: SAFETY_RECOVERY_001 - :detection: N/A (recovery mechanism) - :reaction: Restore last known good state - :asil: C, D - :diagnostic_coverage: N/A - - **Description**: Execution state can be checkpointed and restored to recover from - transient faults. - - **Implementation**: - - Lightweight state snapshots - - Copy-on-write optimization - - Configurable checkpoint intervals - - Automatic rollback on fault detection - - **Limitations**: - - I/O operations cannot be rolled back - - External side effects must be managed by system - -.. safety:: Graceful Degradation - :id: SAFETY_RECOVERY_002 - :detection: N/A (recovery mechanism) - :reaction: Reduced functionality mode - :asil: B, C, D - :diagnostic_coverage: N/A - - **Description**: System can operate in degraded mode with reduced functionality when - non-critical components fail. - - **Implementation**: - - Component criticality classification - - Degraded mode configuration - - Feature disabling on fault - - Performance reduction for safety - - **Degradation Levels**: - 1. Full operation (all features) - 2. Safe mode (critical features only) - 3. Limp mode (minimum functionality) - 4. Shutdown (safe state only) - -Configuration Guidelines -======================== - -ASIL-Specific Configuration ---------------------------- - -.. list-table:: Mechanism Configuration by ASIL Level - :widths: 30 15 15 15 15 - :header-rows: 1 - - * - Safety Mechanism - - ASIL-A - - ASIL-B - - ASIL-C - - ASIL-D - * - Memory Bounds Checking - - Enabled - - Enabled - - Enabled - - Enabled - * - Memory Isolation - - Optional - - Recommended - - Required - - Required - * - Stack Protection - - Basic - - Enhanced - - Full - - Full+HW - * - CFI Protection - - Optional - - Recommended - - Required - - Required - * - Execution Fuel - - Optional - - Required - - Required - - Required - * - Watchdog Integration - - Optional - - Optional - - Required - - Required - * - BIST - - Startup - - Startup - - Periodic - - Continuous - * - Checkpointing - - No - - Optional - - Recommended - - Required - -Performance Impact ------------------- - -.. list-table:: Mechanism Performance Overhead - :widths: 40 20 40 - :header-rows: 1 - - * - Safety Mechanism - - Overhead - - Mitigation Strategy - * - Memory Bounds Checking - - 5-15% - - Bounds elision optimization - * - CFI Protection - - 5-10% - - Type caching, hw support - * - Execution Fuel - - 10-20% - - Coarse-grained fuel checks - * - Runtime Assertions - - 5-30% - - Selective deployment - * - Checkpointing - - 1-5% - - Copy-on-write, intervals - -Integration Checklist -===================== - -Platform Requirements ---------------------- - -□ Memory protection unit (MPU) or MMU available -□ Hardware atomic operations support -□ Reliable timer/clock source -□ Watchdog timer with warning period -□ Sufficient memory for safety mechanisms -□ Hardware CFI support (optional but recommended) - -Configuration Steps -------------------- - -1. Select target ASIL level -2. Configure mechanisms per ASIL table above -3. Set resource limits based on application -4. Configure watchdog integration -5. Enable appropriate diagnostic coverage -6. Verify configuration with built-in tests - -Validation Requirements ------------------------ - -- Fault injection testing for each mechanism -- Performance profiling with mechanisms enabled -- Diagnostic coverage measurement -- Integration testing with system-level safety - -See Also -======== - -- :doc:`requirements` - Safety requirements addressed by these mechanisms -- :doc:`implementations` - Detailed implementation descriptions -- :doc:`verification` - Test procedures for mechanisms -- :doc:`configuration` - Configuration procedures \ No newline at end of file diff --git a/docs/source/safety_manual/requirements.rst b/docs/source/safety_manual/requirements.rst deleted file mode 100644 index 9e3cde740..000000000 --- a/docs/source/safety_manual/requirements.rst +++ /dev/null @@ -1,455 +0,0 @@ -====================== -Safety Requirements -====================== - -.. image:: ../_static/icons/requirements.svg - :width: 64px - :align: right - :alt: Safety Requirements Icon - -This document consolidates all safety requirements for PulseEngine (Kiln Edition) as a Safety Element out of Context (SEooC). These requirements form the basis for safety mechanisms and verification activities. - -.. warning:: - **Integration Note**: These requirements must be verified in the context of the - specific system where PulseEngine is integrated. See :doc:`assumptions` for - integration prerequisites. - -.. contents:: On this page - :local: - :depth: 2 - -Overview -======== - -Requirement Categories ----------------------- - -Safety requirements are organized into the following categories: - -1. **General Safety Requirements** - Overall safety properties -2. **Memory Safety Requirements** - Memory isolation and protection -3. **Resource Management Requirements** - Bounded resource usage -4. **Error Handling Requirements** - Fault detection and recovery -5. **Verification Requirements** - Runtime checks and validation -6. **Temporal Safety Requirements** - Timing and execution bounds -7. **Data Flow Safety Requirements** - Information flow control -8. **Configuration Safety Requirements** - Safe configuration management - -Requirement Attributes ----------------------- - -Each requirement includes: - -- **ID**: Unique identifier (REQ_CATEGORY_NNN) -- **ASIL**: Applicable ASIL level (QM, A, B, C, D) -- **Verification**: Method of verification (Test, Analysis, Review, Inspection) -- **Status**: Implementation status (Implemented, Partial, Planned) -- **Traces To**: Reference to ISO 26262 or IEC 61508 clause - -General Safety Requirements -=========================== - -.. req:: Safety-Critical Operation Mode - :id: REQ_SAFETY_001 - :asil: D - :verification: Test, Analysis - :status: Implemented - :traces_to: ISO 26262-6:7.4.2 - - The runtime SHALL provide a safety-critical operation mode with deterministic behavior, - disabled dynamic features, and comprehensive error detection. - -.. req:: Safety Manual Compliance - :id: REQ_SAFETY_002 - :asil: D - :verification: Review - :status: Implemented - :traces_to: ISO 26262-10:9.4 - - System integrators SHALL follow all procedures defined in this safety manual when - deploying PulseEngine in safety-critical applications. - -.. req:: Fail-Safe Behavior - :id: REQ_SAFETY_003 - :asil: D - :verification: Test, Analysis - :status: Implemented - :traces_to: ISO 26262-6:7.4.3 - - Upon detection of any safety-critical fault, the runtime SHALL transition to a - fail-safe state and notify the system-level error handler. - -.. req:: Safety Mechanism Independence - :id: REQ_SAFETY_004 - :asil: D - :verification: Analysis - :status: Implemented - :traces_to: ISO 26262-6:7.4.10 - - Safety mechanisms SHALL be independent from the functionality they protect to - avoid common cause failures. - -Memory Safety Requirements -========================== - -.. req:: Memory Bounds Validation - :id: REQ_MEM_SAFETY_001 - :asil: D - :verification: Test - :status: Implemented - :traces_to: ISO 26262-6:7.4.14 - - All memory accesses SHALL be validated against allocated boundaries before execution. - Out-of-bounds access attempts SHALL be detected and safely rejected. - -.. req:: Memory Isolation - :id: REQ_MEM_SAFETY_002 - :asil: D - :verification: Test, Analysis - :status: Implemented - :traces_to: ISO 26262-6:7.4.13 - - WebAssembly module instances SHALL be isolated from each other with no shared - mutable state except through explicit, validated interfaces. - -.. req:: Stack Overflow Protection - :id: REQ_MEM_SAFETY_003 - :asil: D - :verification: Test - :status: Implemented - :traces_to: ISO 26262-6:7.4.14 - - Stack usage SHALL be monitored and limited. Stack overflow conditions SHALL be - detected before memory corruption occurs. - -.. req:: Memory Initialization - :id: REQ_MEM_SAFETY_004 - :asil: C - :verification: Test, Inspection - :status: Implemented - :traces_to: ISO 26262-6:8.4.4 - - All allocated memory SHALL be initialized to a known safe state before use. - Uninitialized memory access SHALL be prevented. - -.. req:: Memory Lifetime Management - :id: REQ_MEM_SAFETY_005 - :asil: C - :verification: Analysis, Test - :status: Implemented - :traces_to: ISO 26262-6:7.4.13 - - Memory lifetime SHALL be explicitly managed. Use-after-free and double-free - conditions SHALL be prevented through static lifetime analysis. - -Resource Management Requirements -================================ - -.. req:: Static Resource Allocation - :id: REQ_RESOURCE_001 - :asil: D - :verification: Analysis, Review - :status: Implemented - :traces_to: ISO 26262-6:7.4.4 - - In safety-critical mode, all resources SHALL be allocated statically during - initialization. Dynamic allocation SHALL be disabled during runtime operation. - -.. req:: Resource Limits Enforcement - :id: REQ_RESOURCE_002 - :asil: D - :verification: Test - :status: Implemented - :traces_to: ISO 26262-6:7.4.3 - - Explicit limits SHALL be enforced for: - - Memory usage per module (configurable, default 1MB) - - Stack depth (configurable, default 1000 frames) - - Table size (configurable, default 10000 elements) - - Number of module instances (configurable, default 10) - -.. req:: Resource Exhaustion Handling - :id: REQ_RESOURCE_003 - :asil: C - :verification: Test - :status: Implemented - :traces_to: ISO 26262-6:7.4.3 - - Resource exhaustion SHALL be detected before system destabilization. Graceful - degradation strategies SHALL be implemented for non-critical resources. - -.. req:: Resource Usage Monitoring - :id: REQ_RESOURCE_004 - :asil: B - :verification: Test, Inspection - :status: Implemented - :traces_to: ISO 26262-6:8.4.8 - - Resource usage SHALL be continuously monitored and reported. High watermarks - SHALL be tracked for capacity planning. - -Error Handling Requirements -=========================== - -.. req:: Comprehensive Error Detection - :id: REQ_ERROR_001 - :asil: D - :verification: Test, Analysis - :status: Implemented - :traces_to: ISO 26262-6:7.4.6 - - All detectable error conditions SHALL be explicitly checked. Error detection - coverage SHALL be measured and documented. - -.. req:: Error Propagation Control - :id: REQ_ERROR_002 - :asil: D - :verification: Test, Analysis - :status: Implemented - :traces_to: ISO 26262-6:7.4.7 - - Errors SHALL be propagated through explicit return values or status codes. - Exception-based error handling SHALL NOT be used in safety-critical paths. - -.. req:: Error Recovery Actions - :id: REQ_ERROR_003 - :asil: C - :verification: Test - :status: Implemented - :traces_to: ISO 26262-6:7.4.3 - - For each error category, specific recovery actions SHALL be defined: - - Transient errors: Retry with backoff - - Resource errors: Graceful degradation - - Logic errors: Fail-safe shutdown - - Hardware errors: System notification - -.. req:: Error Logging and Reporting - :id: REQ_ERROR_004 - :asil: B - :verification: Test, Inspection - :status: Implemented - :traces_to: ISO 26262-6:8.4.8 - - All safety-relevant errors SHALL be logged with sufficient context for diagnosis. - Error logs SHALL be protected from overflow and corruption. - -Verification Requirements -========================= - -.. req:: Module Validation - :id: REQ_VERIFY_001 - :asil: D - :verification: Test - :status: Implemented - :traces_to: ISO 26262-6:9.4.2 - - WebAssembly modules SHALL be fully validated according to the WebAssembly - specification before instantiation. Invalid modules SHALL be rejected. - -.. req:: Runtime Integrity Checks - :id: REQ_VERIFY_002 - :asil: D - :verification: Test - :status: Implemented - :traces_to: ISO 26262-6:7.4.8 - - Critical data structures SHALL include integrity checks (checksums, magic values, - redundancy) to detect corruption. - -.. req:: Built-In Test - :id: REQ_VERIFY_003 - :asil: C - :verification: Test - :status: Implemented - :traces_to: ISO 26262-6:8.4.6 - - Power-on self-test (POST) SHALL verify correct operation of safety mechanisms - before entering operational mode. - -.. req:: Continuous Monitoring - :id: REQ_VERIFY_004 - :asil: C - :verification: Test, Analysis - :status: Implemented - :traces_to: ISO 26262-6:7.4.8 - - Safety-critical invariants SHALL be continuously monitored during operation. - Violations SHALL trigger immediate safety actions. - -Temporal Safety Requirements -============================ - -.. req:: Bounded Execution Time - :id: REQ_TEMPORAL_001 - :asil: D - :verification: Test, Analysis - :status: Implemented - :traces_to: ISO 26262-6:7.4.5 - - All operations SHALL complete within bounded time. Worst-case execution time - (WCET) SHALL be determinable through static analysis. - -.. req:: Execution Fuel Limiting - :id: REQ_TEMPORAL_002 - :asil: C - :verification: Test - :status: Implemented - :traces_to: ISO 26262-6:7.4.5 - - Execution SHALL be limited through a fuel mechanism. Fuel exhaustion SHALL - cause controlled termination without resource leaks. - -.. req:: Deadline Monitoring - :id: REQ_TEMPORAL_003 - :asil: C - :verification: Test - :status: Partial - :traces_to: ISO 26262-6:7.4.5 - - Time-critical operations SHALL be monitored for deadline compliance. Deadline - misses SHALL be reported to the system scheduler. - -.. req:: Interrupt Latency Bounds - :id: REQ_TEMPORAL_004 - :asil: B - :verification: Test, Measurement - :status: Implemented - :traces_to: ISO 26262-6:7.4.5 - - Maximum interrupt disable time SHALL be bounded and documented. Critical - sections SHALL be minimized. - -Data Flow Safety Requirements -============================= - -.. req:: Type Safety Enforcement - :id: REQ_DATAFLOW_001 - :asil: D - :verification: Test, Analysis - :status: Implemented - :traces_to: ISO 26262-6:7.4.14 - - Type safety SHALL be enforced at module boundaries. Type confusion SHALL be - prevented through static and dynamic checks. - -.. req:: Information Flow Control - :id: REQ_DATAFLOW_002 - :asil: C - :verification: Analysis - :status: Partial - :traces_to: ISO 26262-6:7.4.13 - - Information flow between different criticality levels SHALL be controlled and - validated. High-criticality data SHALL NOT flow to low-criticality domains. - -.. req:: Data Validation - :id: REQ_DATAFLOW_003 - :asil: C - :verification: Test - :status: Implemented - :traces_to: ISO 26262-6:8.4.4 - - All external inputs SHALL be validated before use. Range checks, format checks, - and consistency checks SHALL be applied. - -Configuration Safety Requirements -================================= - -.. req:: Configuration Validation - :id: REQ_CONFIG_001 - :asil: D - :verification: Test, Analysis - :status: Implemented - :traces_to: ISO 26262-6:9.4.4 - - Configuration parameters SHALL be validated against safety constraints before - activation. Invalid configurations SHALL be rejected. - -.. req:: Configuration Integrity - :id: REQ_CONFIG_002 - :asil: C - :verification: Test, Inspection - :status: Implemented - :traces_to: ISO 26262-6:8.4.7 - - Configuration data SHALL be protected against corruption through checksums or - redundancy. Configuration changes SHALL be atomic. - -.. req:: Safe Defaults - :id: REQ_CONFIG_003 - :asil: B - :verification: Review, Test - :status: Implemented - :traces_to: ISO 26262-6:7.4.2 - - All configuration parameters SHALL have safe default values. The system SHALL - operate safely with default configuration. - -Traceability -============ - -Requirements Allocation ------------------------ - -.. list-table:: Requirements to Component Allocation - :widths: 30 70 - :header-rows: 1 - - * - Component - - Allocated Requirements - * - kiln-runtime - - REQ_SAFETY_*, REQ_MEM_SAFETY_*, REQ_TEMPORAL_* - * - kiln-foundation - - REQ_MEM_SAFETY_*, REQ_RESOURCE_*, REQ_ERROR_* - * - kiln-decoder - - REQ_VERIFY_001, REQ_DATAFLOW_* - * - kiln-instructions - - REQ_TEMPORAL_001, REQ_DATAFLOW_001 - * - kiln-component - - REQ_CONFIG_*, REQ_DATAFLOW_002 - -Standards Traceability ----------------------- - -See :doc:`compliance/traceability` for detailed mapping to: -- ISO 26262:2018 requirements -- IEC 61508:2010 requirements -- IEC 62304:2006 requirements - -Verification Cross-Reference ----------------------------- - -See :doc:`verification` for: -- Test cases covering each requirement -- Analysis reports for non-testable requirements -- Verification completion status - -Updates and Maintenance -======================= - -Requirement Changes -------------------- - -Changes to safety requirements require: - -1. Impact analysis on safety case -2. Verification plan update -3. Traceability matrix update -4. Review and approval by safety assessor - -Version History ---------------- - -Safety requirements are version controlled with the source code. See the git history -for detailed change tracking. - -Next Steps -========== - -After reviewing requirements: - -1. Review :doc:`mechanisms` for implementation approach -2. Check :doc:`implementations` for detailed realization -3. Verify with :doc:`verification` procedures -4. Ensure :doc:`assumptions` are met in your system \ No newline at end of file diff --git a/rivet.yaml b/rivet.yaml new file mode 100644 index 000000000..d47dc2db2 --- /dev/null +++ b/rivet.yaml @@ -0,0 +1,61 @@ +project: + name: kiln + version: "0.1.0" + description: > + WebAssembly runtime for safety-critical systems. Implements the + WebAssembly Core Spec 3.0, Component Model, and WASI Preview 2 + with ASIL-D through QM safety level support. + schemas: + - common + - stpa + - dev + +sources: + - path: safety/stpa + format: stpa-yaml + - path: safety/requirements + format: generic-yaml + +docs: + - docs + +commits: + format: trailers + trailers: + Trace: traces-to + Implements: implements + Fixes: fixes + Verifies: verifies + exempt-types: + - chore + - style + - ci + - docs + - build + traced-paths: + - kiln-runtime/ + - kiln-decoder/ + - kiln-foundation/ + - kiln-component/ + - kiln-platform/ + - kiln-error/ + - kiln-instructions/ + - kiln-sync/ + - kiln-host/ + - kiln-intercept/ + - kiln-wasi/ + - kilnd/ + - safety/ + +externals: + meld: + git: https://github.com/pulseengine/meld.git + path: /Volumes/Home/git/pulseengine/meld + ref: main + prefix: meld + + synth: + git: https://github.com/pulseengine/synth.git + path: /Volumes/Home/git/pulseengine/synth + ref: main + prefix: synth diff --git a/safety/requirements/architecture-components.yaml b/safety/requirements/architecture-components.yaml new file mode 100644 index 000000000..956af05be --- /dev/null +++ b/safety/requirements/architecture-components.yaml @@ -0,0 +1,344 @@ +# Architecture Components — Migrated from sphinx-needs +# +# System: Kiln — WebAssembly runtime for safety-critical systems +# +# Migrated from: +# docs/source/architecture/01_architectural_design/components.rst +# docs/source/architecture/01_architectural_design/patterns.rst +# +# These are architectural components (feature type) that satisfy +# functional and safety requirements by providing actual capabilities. +# +# Interface catalog (ARCH_IF_*) and specification items (SPEC_*, IMPL_*) +# are NOT migrated — they describe internal structure better captured in +# code documentation than in traceability artifacts. +# +# Format: rivet generic-yaml + +artifacts: + # ========================================================================= + # Core Components (crate-level) + # ========================================================================= + - id: AC-RUNTIME + type: feature + title: Runtime core execution engine + description: > + Stackless WebAssembly instruction execution engine with resumable + operation, fuel-based bounded execution, and multi-instance support. + Crate: kiln-runtime. + status: partial + tags: [component, runtime, core] + links: + - type: satisfies + target: REQ_FUNC_001 + - type: satisfies + target: REQ_LFUNC_005 + - type: satisfies + target: REQ_LFUNC_018 + fields: + previous-id: ARCH_COMP_001 + implementation: kiln-runtime/src/stackless/engine.rs + note: "Infrastructure implemented; ~1,500 WAST assertion failures remain (Issue 149)" + + - id: AC-MEMORY + type: feature + title: Memory manager with safe memory provider + description: > + Safe memory operations with bounds checking, integrity verification, + and capability-based allocation via safe_managed_alloc! macro. + Supports std, no_std+alloc, and no_alloc environments. + Crate: kiln-foundation. + status: implemented + tags: [component, memory, safety] + links: + - type: satisfies + target: REQ_MEM_SAFETY_005 + - type: satisfies + target: REQ_MEM_SAFETY_002 + fields: + previous-id: ARCH_COMP_002 + implementation: kiln-foundation/src/safe_memory.rs, kiln-foundation/src/capabilities/ + + - id: AC-COMPONENT + type: feature + title: Component Model runtime + description: > + WebAssembly Component Model Preview 2 implementation including + component instantiation, canonical ABI lifting/lowering, resource + lifecycle management, and interface types. + Crate: kiln-component. + status: partial + tags: [component, component-model] + links: + - type: satisfies + target: REQ_FUNC_014 + - type: satisfies + target: REQ_FUNC_021 + - type: satisfies + target: REQ_CMP_020 + fields: + previous-id: ARCH_COMP_003 + implementation: kiln-component/src/ + + - id: AC-DECODER + type: feature + title: WebAssembly binary decoder + description: > + Streaming WebAssembly binary format parser with validation. + Parses modules and components into internal representation. + Crate: kiln-decoder. + status: implemented + tags: [component, decoder] + links: + - type: satisfies + target: REQ_LFUNC_018 + fields: + previous-id: ARCH_COMP_004 + implementation: kiln-decoder/src/streaming_decoder.rs + + - id: AC-PLATFORM + type: feature + title: Platform abstraction layer + description: > + OS-specific operations abstracted behind common traits (PageAllocator, + FutexLike). Backends for macOS, Linux, QNX, Zephyr, and bare-metal. + Crate: kiln-platform. + status: implemented + tags: [component, platform] + links: + - type: satisfies + target: REQ_PLATFORM_001 + fields: + previous-id: ARCH_COMP_005 + implementation: kiln-platform/src/ + + # ========================================================================= + # Supporting Components + # ========================================================================= + - id: AC-ERROR + type: feature + title: Unified error management system + description: > + ASIL-compliant error categorization with factory methods, error + propagation through Result types, and no_std compatibility. + Crate: kiln-error. + status: implemented + tags: [component, error-handling] + links: + - type: satisfies + target: REQ_ERROR_001 + fields: + previous-id: ARCH_COMP_010 + implementation: kiln-error/src/ + + - id: AC-INSTRUCTIONS + type: feature + title: WebAssembly instruction set implementation + description: > + Instruction execution for arithmetic, control flow, memory operations, + variable access, type conversions, table operations, and SIMD. + Crate: kiln-instructions. + status: implemented + tags: [component, instructions] + links: + - type: satisfies + target: REQ_LFUNC_018 + fields: + previous-id: ARCH_COMP_011 + implementation: kiln-instructions/src/ + + - id: AC-BOUNDED + type: feature + title: Bounded collections for no_alloc environments + description: > + BoundedVec, BoundedString, and other bounded collections that replace + standard collections in no_alloc environments with compile-time + capacity limits. + Crate: kiln-foundation. + status: implemented + tags: [component, bounded, no-std] + links: + - type: satisfies + target: REQ_FUNC_002 + - type: satisfies + target: REQ_LFUNC_006 + fields: + previous-id: ARCH_COMP_012 + implementation: kiln-foundation/src/bounded.rs + + # ========================================================================= + # Runtime Features (not separate crate-level components in sphinx-needs, + # but real implemented capabilities that satisfy requirements) + # ========================================================================= + - id: AC-WASI + type: feature + title: WASI Preview 2 dispatcher + description: > + WASI logging support with all log levels (Error, Warn, Info, Debug, + Trace), context-based logging, stderr integration, and thread-safe + operations. Crate: kiln-wasi. + status: implemented + tags: [component, wasi] + links: + - type: satisfies + target: REQ_FUNC_015 + fields: + implementation: kiln-wasi/src/dispatcher.rs + + - id: AC-ASYNC + type: feature + title: Async/await runtime for Component Model + description: > + Async canonical lifting/lowering, async execution engine with + future-based task management, and context preservation across async + boundaries. Crate: kiln-runtime. + status: implemented + tags: [component, async, runtime] + links: + - type: satisfies + target: REQ_FUNC_030 + fields: + implementation: kiln-runtime/src/async_runtime.rs + + - id: AC-DEBUG + type: feature + title: Debug infrastructure + description: > + DWARF debug information parsing, WIT-aware debugging with source + mapping, runtime breakpoint management, and stack trace generation. + Crate: kiln-runtime. + status: implemented + tags: [component, debugging, tooling] + links: + - type: satisfies + target: REQ_FUNC_032 + fields: + implementation: kiln-runtime/src/debug/ + + - id: AC-WAST + type: feature + title: WAST test suite runner + description: > + Integration with the official WebAssembly specification (WAST) test + suite for conformance and correctness testing. Test runner with + result tracking and memory statistics. + status: partial + tags: [testing, conformance] + links: + - type: satisfies + target: REQ_FUNC_022 + fields: + implementation: kiln-build-core/src/wast_execution.rs + note: "Test runner exists; ~1,600 assertion failures across Issues 146-149" + + - id: AC-FUZZ + type: feature + title: Fuzzing infrastructure + description: > + Fuzzing coverage for bounded collections, memory adapters, component + model parser, type bounds, canonical options, and WIT parser. + status: implemented + tags: [testing, fuzzing, quality] + links: + - type: satisfies + target: REQ_QA_010 + fields: + implementation: fuzz/ + + - id: AC-FORMAL + type: feature + title: Formal verification via Kani + description: > + Kani proof harness integration, model checking annotations, + invariant specifications, and bounded verification for critical paths. + status: implemented + tags: [verification, formal-methods] + links: + - type: satisfies + target: REQ_VERIFY_010 + fields: + implementation: "Kani proofs in kiln-foundation, kiln-runtime" + + - id: AC-KILND + type: feature + title: kilnd daemon with multiple deployment modes + description: > + Runtime daemon supporting standard mode (kilnd-std), allocation mode + (kilnd-alloc), and no-std mode (kilnd-nostd), each with appropriate + resource limits and safety constraints. + status: implemented + tags: [deployment, daemon] + links: + - type: satisfies + target: REQ_FUNC_033 + fields: + implementation: kilnd/src/ + + # ========================================================================= + # Tooling & Monitoring Features + # ========================================================================= + - id: AC-MONITORING + type: feature + title: Resource usage monitoring infrastructure + description: > + Memory monitoring via MEMORY_MONITOR global singleton with + record_allocation/record_deallocation tracking. SafetyMonitor with + AllocationMonitor, CapabilityMonitor, ErrorMonitor, PerformanceMonitor + subsystems. Returns SafetyReport with health_score (0-100). + High watermark tracking for capacity planning. + status: partial + tags: [monitoring, resource-management, tooling] + links: + - type: satisfies + target: REQ_RESOURCE_004 + fields: + previous-id: IMPL_RESOURCE_SAFETY_001 + implementation: kiln-foundation/src/monitoring.rs, kiln-foundation/src/safety_monitor.rs + note: "~1,800 lines of infrastructure exist but not yet wired to allocation paths" + + # ========================================================================= + # NOT MIGRATED (with rationale): + # + # ARCH_COMP_SYSTEM — meta-level "system" component; covered by rivet + # project definition. + # + # ARCH_COMP_PATTERNS_001-008 — architectural pattern descriptions; + # these describe HOW components are built, not WHAT capability they + # provide. Patterns captured in AD-PATTERNS-001 and AD-ENV-001. + # + # ARCH_COMP_TRACE_001, ARCH_COMP_COV_001, ARCH_COMP_SEQ_001, + # ARCH_COMP_STATE_001, ARCH_COMP_CPU_001, ARCH_COMP_RES_001 — + # meta-documentation components describing architecture documents, + # not system capabilities. + # + # ARCH_IF_* (~42 interface items) — internal API specifications; + # captured in Rust trait definitions and code documentation. + # + # SPEC_005 (CLI), SPEC_009 (Safety), SPEC_010 (Testing), + # SPEC_VERIFY_001 (Verification Levels) — architecture-level specs + # covered by: AC-KILND, safety-mechanisms.yaml, AC-WAST/AC-FUZZ/ + # AC-FORMAL, AD-VERIFY-001 respectively. + # + # IMPL_008 (CLI), IMPL_009 (WAST), IMPL_MEMORY_SAFETY_001, + # IMPL_RESOURCE_SAFETY_001, IMPL_ERROR_HANDLING_RECOVERY_001, + # IMPL_VERIFICATION_001, IMPL_CONFIG_001, IMPL_SAFETY_TESTING_001 — + # implementation tracking items covered by corresponding AC-*/SM-*/AD-* + # artifacts at the proper traceability level. + # + # QUAL_100-102 (ASIL-D, SIL-3, Class C targets) — certification + # aspirations, not code properties. Tracked in evaluation_plan.rst. + # + # QUAL_103-108 — process/documentation deliverables (evaluation plan, + # qualification report, traceability matrix, etc.). rivet replaces + # QUAL_105 (traceability matrix) natively. + # + # KILNQ_001-007 — auto-generated panic registry. Operational defects + # tracked as issues, not traceability artifacts. + # + # SAFETY_001-004 (pre-STPA hazards) — superseded by STPA analysis + # (H-1 through H-10 in safety/stpa/hazards.yaml). + # + # FR-001..PER-004 (traceability.rst alternate IDs) — duplicate + # numbering scheme used only in architecture docs. rivet generates + # traceability matrices natively. + # ========================================================================= diff --git a/safety/requirements/architecture-decisions.yaml b/safety/requirements/architecture-decisions.yaml new file mode 100644 index 000000000..77abd80d8 --- /dev/null +++ b/safety/requirements/architecture-decisions.yaml @@ -0,0 +1,187 @@ +# Architecture Decisions — Migrated from sphinx-needs +# +# System: Kiln — WebAssembly runtime for safety-critical systems +# +# Migrated from: +# docs/source/architecture/01_architectural_design/overview.rst +# docs/source/architecture/01_architectural_design/patterns.rst +# +# These are architectural design decisions (design-decision type) that +# satisfy functional and safety requirements. +# +# Architectural constraints (ARCH_CON_001-003) and architectural +# requirements (ARCH_REQ_001-005) are NOT migrated as separate artifacts — +# they are subsumed by the existing functional and safety requirements +# (REQ_PLATFORM_001, REQ_FUNC_002, REQ_LFUNC_006, SR-3, REQ_SAFETY_001, etc.) +# +# Format: rivet generic-yaml + +artifacts: + # ========================================================================= + # Core Architecture Decisions + # ========================================================================= + - id: AD-COMP-001 + type: design-decision + title: Component-based modular architecture + description: > + The system is decomposed into independently testable and certifiable + components (crates), each with a single well-defined responsibility. + Higher layers depend only on lower layers. Platform-specific code is + isolated in the Platform Abstraction Layer. + status: implemented + tags: [architecture, modularity] + links: + - type: satisfies + target: REQ_PLATFORM_001 + - type: satisfies + target: REQ_FUNC_002 + fields: + rationale: > + Modular design enables independent testing, certification, and + platform-specific optimization. Clear separation of concerns allows + selective feature inclusion and minimizes dependencies. + previous-id: ARCH_DEC_COMP_001 + implementation: Cargo workspace with 24 specialized crates + + - id: AD-DEPLOY-001 + type: design-decision + title: Multi-platform deployment strategy + description: > + Different deployment environments (server, embedded Linux, QNX, VxWorks, + Zephyr RTOS, bare-metal) are supported through the platform abstraction + layer with environment-specific memory models, security features, and + resource constraints. + status: partial + tags: [architecture, platform, deployment] + links: + - type: satisfies + target: REQ_PLATFORM_001 + - type: satisfies + target: REQ_FUNC_002 + - type: satisfies + target: REQ_FUNC_033 + fields: + rationale: > + Different deployment environments require different memory models + and security features. Platform abstraction isolates these + differences behind common interfaces. + previous-id: ARCH_DEC_DEPLOY_001 + implementation: kiln-platform/src/ + + - id: AD-CRATE-001 + type: design-decision + title: Fine-grained crate organization + description: > + Implementation organized into fine-grained crates (kiln-error, + kiln-foundation, kiln-format, kiln-decoder, kiln-runtime, + kiln-instructions, kiln-component, kiln-platform, etc.) to enable + selective feature inclusion and minimize dependency footprint. + status: implemented + tags: [architecture, organization] + links: + - type: satisfies + target: REQ_LFUNC_006 + fields: + rationale: > + Fine-grained crates enable selective feature compilation (e.g., + exclude Component Model for embedded), clear dependency boundaries + for safety analysis, and independent testing/verification. + previous-id: ARCH_DEC_CRATE_001 + implementation: Cargo.toml workspace members + + - id: AD-ENV-001 + type: design-decision + title: Multi-environment architecture (std / no_std+alloc / no_std) + description: > + Four environment configurations supported via conditional compilation: + full std, no_std with alloc, no_std without alloc (bounded collections), + and bare-metal. Same interfaces work across all environments with + different backing implementations. + status: implemented + tags: [architecture, no-std, platform] + links: + - type: satisfies + target: REQ_FUNC_002 + - type: satisfies + target: REQ_LFUNC_006 + fields: + rationale: > + Different deployment scenarios require different resource trade-offs. + Conditional compilation with trait-based abstractions provides full + feature parity across environments. + previous-id: ARCH_DEC_ENV_001 + implementation: "#![cfg_attr(not(feature = \"std\"), no_std)] across all crates" + + - id: AD-PATTERNS-001 + type: design-decision + title: Three-tier environment support pattern + description: > + Trait-based abstractions (MemoryProvider, ComponentFactory, etc.) with + environment-specific implementations selected at compile time. BoundedVec, + BoundedString, and other bounded collections replace std collections in + no_alloc environments. + status: implemented + tags: [architecture, patterns, no-std] + links: + - type: satisfies + target: REQ_FUNC_002 + - type: satisfies + target: REQ_LFUNC_006 + fields: + rationale: > + Trait-based abstractions with conditional compilation enable the same + API surface across std, no_std+alloc, and no_std+no_alloc environments + without runtime overhead. + previous-id: ARCH_DEC_PATTERNS_001 + implementation: kiln-foundation/src/safe_memory.rs, kiln-foundation/src/bounded.rs + + # ========================================================================= + # Tooling & Verification Decisions + # ========================================================================= + - id: AD-BUILD-001 + type: design-decision + title: Unified build and verification tooling (cargo-kiln) + description: > + Single CLI entry point (cargo-kiln) for all build, test, verification, + and ASIL compliance operations. Includes: ASIL-level verification + (verify --asil d), build matrix verification (verify-matrix --report), + no-std validation, requirements traceability (requirements verify), + safety feature testing, and diagnostic system with LSP-compatible + JSON output. + status: implemented + tags: [tooling, build-system, verification] + links: + - type: satisfies + target: REQ_CONFIG_001 + - type: satisfies + target: REQ_CONFIG_003 + fields: + rationale: > + Single entry point ensures consistent configuration validation and + safe defaults across all development activities. Build matrix + verification detects ASIL compliance issues before merge. + Replaces fragmented shell scripts and justfile recipes. + previous-id: IMPL_CONFIG_001 + implementation: cargo-kiln/src/, kiln-build-core/src/ + + - id: AD-VERIFY-001 + type: design-decision + title: Configurable verification level system + description: > + Multiple verification levels (Off, Basic, Standard, Full, Sampling, + Redundant) configurable per-component and per-deployment scenario. + Verification operates independently of the functionality it protects — + safety mechanisms can be verified without affecting execution behavior. + status: implemented + tags: [verification, safety-independence, asil-d] + links: + - type: satisfies + target: REQ_SAFETY_004 + fields: + rationale: > + Safety mechanism independence (ISO 26262-6:7.4.10) requires that + verification systems do not share failure modes with the mechanisms + they verify. Configurable levels allow deployment-appropriate + trade-offs between coverage and performance. + previous-id: SPEC_VERIFY_001, IMPL_VERIFICATION_001 + implementation: kiln-foundation/src/verification.rs diff --git a/safety/requirements/functional-requirements.yaml b/safety/requirements/functional-requirements.yaml new file mode 100644 index 000000000..3fa04a6ed --- /dev/null +++ b/safety/requirements/functional-requirements.yaml @@ -0,0 +1,321 @@ +# Functional Requirements — Migrated from sphinx-needs +# +# System: Kiln — WebAssembly runtime for safety-critical systems +# +# Migrated from: docs/source/requirements.rst +# +# Status key: +# implemented — infrastructure exists and works +# partial — partially implemented, gaps remain +# planned — design exists but no implementation +# removed — no longer applicable (with rationale) +# +# Format: rivet generic-yaml + +artifacts: + # ========================================================================= + # Platform & Runtime Architecture + # ========================================================================= + - id: REQ_PLATFORM_001 + type: requirement + title: Platform abstraction layer + description: > + The runtime shall provide a platform abstraction layer (PAL) with + distinct backends for target operating systems (macOS, Linux, QNX, + Zephyr) and bare-metal environments, selectable via compile-time + features. The PAL shall abstract OS-specific APIs for memory + allocation/protection and synchronization primitives. + status: implemented + tags: [platform, architecture] + fields: + implementation: kiln-platform/src/ + + - id: REQ_FUNC_001 + type: requirement + title: Resumable interpreter + description: > + The interpreter shall be resumable, allowing operation with fuel or + other bounded run-time mechanisms that require the interpreter to be + halted and later resumed as if it was not halted. + status: implemented + tags: [runtime, core] + fields: + implementation: kiln-runtime/src/stackless/engine.rs + + - id: REQ_FUNC_002 + type: requirement + title: Baremetal support + description: > + The interpreter shall be executable on bare-metal environments with + no reliance on any specific functionality from the provided execution + environment, ready for embedding to any environment Rust can compile for. + status: implemented + tags: [platform, no-std] + fields: + implementation: "All crates support #![no_std]" + + - id: REQ_FUNC_003 + type: requirement + title: Bounded execution + description: > + The interpreter shall yield back control flow eventually, allowing + users to call the interpreter with a bound and expect a result in + a finite amount of time or bytecode operations. + status: implemented + tags: [runtime, safety] + fields: + implementation: kiln-runtime/src/stackless/engine.rs (fuel mechanism) + + - id: REQ_FUNC_033 + type: requirement + title: Multiple runtime deployment modes + description: > + The interpreter shall support multiple runtime deployment modes + through the kilnd daemon: standard mode (kilnd-std), allocation + mode (kilnd-alloc), and no-std mode (kilnd-nostd), each with + appropriate resource limits and safety constraints. + status: implemented + tags: [runtime, deployment] + fields: + implementation: kilnd/src/ + + # ========================================================================= + # WebAssembly Spec Conformance + # ========================================================================= + - id: REQ_LFUNC_018 + type: requirement + title: WebAssembly Core Spec 3.0 implementation + description: > + The interpreter shall implement the WebAssembly Core Spec 3.0, + including: module validation, value types and reference types, + instructions and control flow, function calls and tables, memory + and data segments, global variables, exception handling (modern + try_table syntax), and SIMD operations. + status: partial + tags: [wasm-core, spec-conformance] + fields: + implementation: kiln-runtime/src/stackless/engine.rs + spec-reference: "WebAssembly Core Spec 3.0 (2025-12-03)" + note: "~1,500 assert_return failures remain (Issue 149)" + + - id: REQ_FUNC_022 + type: requirement + title: WAST test suite compatibility + description: > + The interpreter shall be testable against the official WebAssembly + specification (WAST) test suite to ensure conformance and correctness. + status: partial + tags: [testing, spec-conformance] + fields: + implementation: kiln-build-core/src/wast_execution.rs + note: "Test runner exists; ~1,600 assertion failures across Issues 146-149" + + # ========================================================================= + # Component Model + # ========================================================================= + - id: REQ_FUNC_014 + type: requirement + title: WebAssembly Component Model support + description: > + The interpreter shall implement the WebAssembly Component Model + Preview 2 specification, including: component model validation, + resource type handling, interface types, component instantiation + and linking, resource lifetime management, custom section handling, + and component model binary format parsing. + status: partial + tags: [component-model, spec-conformance] + fields: + implementation: kiln-component/src/ + spec-reference: "Component Model commit deb0b0a (2025-05-19)" + + - id: REQ_FUNC_021 + type: requirement + title: Component Model binary format + description: > + The interpreter shall strictly implement the WebAssembly Component + Model binary format including magic bytes, component sections, + type encoding, import/export handling, core module embedding, + canonical ABI encoding/decoding, and LEB128 encoding. + status: partial + tags: [component-model, decoder] + links: + - type: derives-from + target: REQ_FUNC_014 + fields: + implementation: kiln-decoder/src/streaming_decoder.rs, kiln-component/src/ + + - id: REQ_CMP_020 + type: requirement + title: Component resource lifecycle management + description: > + The component model implementation shall provide comprehensive + lifecycle management for resource types, ensuring proper creation, + tracking, and disposal of resources. + status: partial + tags: [component-model, resources] + links: + - type: derives-from + target: REQ_FUNC_014 + fields: + implementation: kiln-component/src/components/resource_management.rs + note: "Subsumed by STPA requirements SR-12 (no-aliasing) and SR-13 (double-drop)" + + # ========================================================================= + # WASI Support + # ========================================================================= + - id: REQ_FUNC_015 + type: requirement + title: WASI logging support + description: > + The interpreter shall implement WASI logging with support for all + defined log levels (Error, Warn, Info, Debug, Trace), context-based + logging, stderr integration, and thread-safe logging operations. + status: implemented + tags: [wasi, logging] + fields: + implementation: kiln-wasi/src/dispatcher.rs + + # ========================================================================= + # Low-Level Implementation + # ========================================================================= + - id: REQ_LFUNC_005 + type: requirement + title: Stackless implementation + description: > + The interpreter shall be stackless, storing the stack of the + interpreted bytecode in a traditional data structure rather than + using function calls in the host environment. + status: implemented + tags: [runtime, architecture] + links: + - type: derives-from + target: REQ_FUNC_001 + fields: + implementation: kiln-runtime/src/stackless/ + + - id: REQ_LFUNC_006 + type: requirement + title: No standard library dependency + description: > + The interpreter shall be implemented in no_std Rust, only relying + on functionality provided by core/alloc to enable execution on + bare environments where no operating system is available. + status: implemented + tags: [platform, no-std] + links: + - type: derives-from + target: REQ_FUNC_002 + fields: + implementation: "All core crates: #![cfg_attr(not(feature = \"std\"), no_std)]" + note: "kiln-runtime/src/memory.rs has a no_std guard bug (Issue in Stream D)" + + # ========================================================================= + # Advanced Runtime + # ========================================================================= + - id: REQ_FUNC_030 + type: requirement + title: Async/await runtime support + description: > + The interpreter shall provide async/await runtime support for the + Component Model, including async canonical lifting/lowering, async + execution engine with future-based task management, and context + preservation across async boundaries. + status: implemented + tags: [runtime, async] + fields: + implementation: kiln-runtime/src/async_runtime.rs + + - id: REQ_FUNC_032 + type: requirement + title: Debug infrastructure + description: > + The interpreter shall provide debugging capabilities including + DWARF debug information parsing, WIT-aware debugging with source + mapping, runtime breakpoint management, and stack trace generation. + status: implemented + tags: [debugging, tooling] + fields: + implementation: kiln-runtime/src/debug/ + + - id: REQ_QA_010 + type: requirement + title: Fuzzing infrastructure + description: > + The interpreter shall include fuzzing infrastructure covering + bounded collections, memory adapters, component model parser, + type bounds, canonical options, and WIT parser fuzzing. + status: implemented + tags: [testing, quality] + fields: + implementation: fuzz/ + + - id: REQ_VERIFY_010 + type: requirement + title: Formal verification support + description: > + The interpreter shall include support for formal verification + through Kani proof harness integration, model checking annotations, + invariant specifications, and bounded verification for critical paths. + status: implemented + tags: [verification, formal-methods] + fields: + implementation: "Kani proofs in kiln-foundation, kiln-runtime" + + - id: REQ_HELPER_ABI_001 + type: requirement + title: Helper runtime C ABI exports + description: > + The AOT helper runtime (libkiln_helper) shall export a stable C + ABI including functions for Wasm operations not efficiently inlined + by the AOT compiler: kiln_memory_copy, kiln_memory_fill, + kiln_memory_grow, kiln_atomic_wait, kiln_atomic_notify. + status: planned + tags: [aot, synth-integration] + fields: + note: "Related to BA RFC #46 host-wit-bindgen equivalent" + + # ========================================================================= + # REMOVED from sphinx-needs (with rationale): + # + # REQ_FUNC_004 (State Migration) — planned, never started, low priority. + # Re-add when state migration becomes active work. + # + # REQ_FUNC_016 (Platform-Specific Logging) — planned, never started. + # syslog/os_log integration is an embedder concern in SEooC model. + # + # REQ_LFUNC_008 (State Serialization) — planned, never started. Same as + # REQ_FUNC_004. + # + # REQ_LFUNC_023 (Optimized Instruction Dispatch) — optimization goal, + # not a functional requirement. Track as a performance objective. + # + # REQ_LFUNC_024 (Efficient Operand Stack) — same as above. + # + # REQ_LFUNC_025 (Efficient Branch Pre-calculation) — same as above. + # + # REQ_LFUNC_026 (Minimize Code Complexity) — design principle, not a + # requirement. Captured in CLAUDE.md guidelines. + # + # REQ_DEP_009 (Logging crate dependency) — dependency management belongs + # in Cargo.toml, not requirements. + # + # REQ_DEP_010 (libm dependency) — same as above. + # + # REQ_DEP_011 (Rust version 1.76.0) — MSRV belongs in Cargo.toml and + # rust-toolchain.toml. + # + # REQ_OBS_012 (Instrumentation Support) — partially implemented via + # kiln_foundation::tracing; operational concern. + # + # REQ_OBS_013 (Coverage Measurement) — DO-178C coverage is a + # certification process concern, not a code requirement. + # + # REQ_FUNC_031 (Advanced Threading) — partially implemented; re-add + # when threading becomes active work. + # + # REQ_PERF_010 (Hardware Optimization) — SIMD/MTE/CET are platform + # features, not functional requirements. + # + # REQ_LFUNC_019 (Component Model Implementation) — duplicates + # REQ_FUNC_014 at a lower level. + # ========================================================================= diff --git a/safety/requirements/safety-mechanisms.yaml b/safety/requirements/safety-mechanisms.yaml new file mode 100644 index 000000000..6384f2907 --- /dev/null +++ b/safety/requirements/safety-mechanisms.yaml @@ -0,0 +1,292 @@ +# Safety Mechanisms — Migrated from sphinx-needs +# +# System: Kiln — WebAssembly runtime for safety-critical systems +# +# Migrated from: docs/source/safety_manual/mechanisms.rst +# +# These are design decisions describing HOW safety requirements are +# satisfied. Each mechanism links back to the requirement(s) it addresses. +# +# The 4 pre-STPA hazards (SAFETY_001-004 from qualification/safety_analysis.rst) +# are NOT migrated — they are superseded by the comprehensive STPA hazard +# analysis (H-1 through H-10 in safety/stpa/hazards.yaml). +# +# Format: rivet generic-yaml + +artifacts: + # ========================================================================= + # Memory Safety Mechanisms + # ========================================================================= + - id: SM-MEM-001 + type: design-decision + title: Memory bounds checking via SafeSlice + description: > + All memory accesses are validated against allocation boundaries before + execution. Pre-access and in-access dual-check strategy. SafeSlice + wrapper enforces bounds on all slice operations with integer overflow + detection in offset calculations. + status: implemented + tags: [memory-safety, asil-d, mechanism] + links: + - type: satisfies + target: SR-3 + - type: satisfies + target: REQ_MEM_SAFETY_002 + - type: satisfies + target: REQ_MEM_SAFETY_004 + fields: + rationale: > + 99% diagnostic coverage for out-of-bounds accesses. Always enabled in + safety-critical mode. Performance mode allows selective bounds elision. + previous-id: SAFETY_MEM_001, SAFETY_MEM_002, SAFETY_MEM_004 + implementation: kiln-foundation/src/safe_memory.rs + + - id: SM-MEM-002 + type: design-decision + title: Stack overflow protection via depth counter and guard pages + description: > + Stack depth counter with configurable limit, guard pages when platform + supports, stack canary values for corruption detection, and + pre-allocation of maximum stack space. + status: implemented + tags: [memory-safety, asil-d, mechanism] + links: + - type: satisfies + target: SR-5 + fields: + rationale: > + 90% diagnostic coverage. Cannot detect all forms of stack corruption. + Guard pages require platform support. + previous-id: SAFETY_MEM_003 + implementation: kiln-runtime/src/stackless/engine.rs + + # ========================================================================= + # Control Flow Integrity Mechanisms + # ========================================================================= + - id: SM-CFI-001 + type: design-decision + title: Indirect call type signature validation + description: > + All indirect calls validated against function table before execution. + Type signature validation on every indirect call, function index bounds + checking, table element initialization tracking. No function pointer + arithmetic allowed. + status: implemented + tags: [cfi, asil-d, mechanism] + links: + - type: satisfies + target: SR-20 + - type: satisfies + target: SR-21 + fields: + rationale: > + 100% diagnostic coverage for invalid indirect calls. ~5-10% overhead + on indirect-call-heavy workloads. + previous-id: SAFETY_CFI_001 + implementation: kiln-runtime/src/cfi_engine.rs + + - id: SM-CFI-002 + type: design-decision + title: Shadow control stack with return validation + description: > + Shadow control stack protects against control stack corruption through + redundancy and validation checks. Return address validation on unwind. + Structured control flow enforcement. + status: implemented + tags: [cfi, asil-d, mechanism] + links: + - type: satisfies + target: SR-20 + fields: + rationale: > + >85% diagnostic coverage. Hardware CET support provides additional + protection. Software-only mode available with reduced coverage. + previous-id: SAFETY_CFI_002 + implementation: kiln-runtime/src/cfi_engine.rs + + # ========================================================================= + # Resource Protection Mechanisms + # ========================================================================= + - id: SM-RES-001 + type: design-decision + title: Per-module memory quotas via safe_managed_alloc! + description: > + Memory usage limited per module with strict enforcement. Per-module + memory quotas (default 1MB, configurable). Allocation tracking with + O(1) quota checks. Hierarchical quotas for module groups. No dynamic + allocation after initialization in ASIL-D. + status: implemented + tags: [resource-management, asil-d, mechanism] + links: + - type: satisfies + target: SR-22 + - type: satisfies + target: SR-23 + - type: satisfies + target: SR-8 + - type: satisfies + target: REQ_RESOURCE_003 + fields: + rationale: > + 100% diagnostic coverage for quota violations. Uses capability-based + allocation via safe_managed_alloc! macro exclusively. + previous-id: SAFETY_RESOURCE_001 + implementation: kiln-foundation/src/capabilities/memory_factory.rs + + - id: SM-RES-002 + type: design-decision + title: Fuel-based execution limiting + description: > + Execution limited through fuel mechanism. Fuel consumption per + instruction (configurable costs). Fuel checks at loop headers and + function entries. Interruptible execution for external timeout. + Deterministic fuel consumption for WCET analysis. + status: implemented + tags: [resource-management, asil-c, mechanism] + links: + - type: satisfies + target: SR-2 + - type: satisfies + target: REQ_TEMPORAL_001 + - type: satisfies + target: REQ_FUNC_003 + fields: + rationale: > + 100% diagnostic coverage for fuel exhaustion. Basic arithmetic: 1 fuel, + memory access: 2, function call: 10, indirect call: 15. + previous-id: SAFETY_RESOURCE_002 + implementation: kiln-runtime/src/stackless/engine.rs + + # ========================================================================= + # Data Integrity Mechanisms + # ========================================================================= + - id: SM-DATA-001 + type: design-decision + title: Static and runtime type safety enforcement + description: > + WebAssembly type system strictly enforced. Static type checking during + validation. Runtime type checks for indirect calls. No type casts or + unions allowed. Memory typed only as bytes. + status: implemented + tags: [type-safety, asil-d, mechanism] + links: + - type: satisfies + target: SR-1 + - type: satisfies + target: SR-7 + - type: satisfies + target: REQ_DATAFLOW_003 + fields: + rationale: > + 100% diagnostic coverage for type violations. No undefined behavior + from type errors. Predictable trap on type mismatch. + previous-id: SAFETY_DATA_001 + implementation: kiln-decoder/src/streaming_decoder.rs, kiln-runtime/src/stackless/engine.rs + + # ========================================================================= + # Fault Detection Mechanisms + # ========================================================================= + - id: SM-DETECT-001 + type: design-decision + title: Runtime assertion checking with precondition/postcondition verification + description: > + Critical invariants continuously verified during execution with + immediate detection of violations. Precondition checks on + safety-critical functions, postcondition verification, invariant + checks at key points, diagnostic information collection. + status: implemented + tags: [verification, asil-d, mechanism] + links: + - type: satisfies + target: REQ_ERROR_001 + - type: satisfies + target: REQ_VERIFY_002 + - type: satisfies + target: REQ_VERIFY_004 + fields: + rationale: > + 100% diagnostic coverage for assertion violations. Can be selectively + disabled for QM components. Always enabled for ASIL components. + previous-id: SAFETY_DETECT_002 + implementation: kiln-foundation/src/ + + # ========================================================================= + # Error Recovery Mechanisms + # ========================================================================= + - id: SM-RECOVERY-001 + type: design-decision + title: Fail-safe state transition on fault detection + description: > + Upon detection of any safety-critical fault, runtime transitions to + fail-safe state and notifies system-level error handler. Error + propagation through explicit Result types only; no exceptions in + safety-critical paths. + status: implemented + tags: [error-handling, asil-d, mechanism] + links: + - type: satisfies + target: REQ_SAFETY_001 + - type: satisfies + target: REQ_SAFETY_003 + - type: satisfies + target: REQ_ERROR_002 + - type: satisfies + target: REQ_ERROR_003 + fields: + rationale: > + Degradation levels: full operation → safe mode → limp mode → shutdown. + I/O operations cannot be rolled back. + previous-id: SAFETY_RECOVERY_001, SAFETY_RECOVERY_002 + implementation: kiln-error/src/lib.rs + + # ========================================================================= + # Isolation Mechanisms + # ========================================================================= + - id: SM-ISOLATION-001 + type: design-decision + title: Module memory isolation via linear memory sandbox + description: > + Each WebAssembly module instance executes in its own linear memory + sandbox. No shared mutable state between instances except through + explicit, validated import/export interfaces. Memory isolation + enforced by the WebAssembly execution model — modules cannot + address memory outside their linear memory. Combined with per-module + quotas (SM-RES-001) and link-time type checking (SR-15) to provide + criticality-level information flow control. + status: implemented + tags: [isolation, information-flow, asil-c, mechanism] + links: + - type: satisfies + target: REQ_DATAFLOW_002 + fields: + rationale: > + WebAssembly's linear memory model provides hardware-independent + memory isolation. Each module's memory is a contiguous byte array + inaccessible to other modules. Cross-module data flow requires + explicit import/export declarations validated at link time. + implementation: kiln-runtime/src/memory.rs, kiln-runtime/src/module_instance.rs + + # ========================================================================= + # Temporal Safety Mechanisms + # ========================================================================= + - id: SM-TEMPORAL-001 + type: design-decision + title: Bounded critical sections and interrupt latency control + description: > + Critical sections minimized through capability-based locking + (kiln_sync::Mutex). Lock-free algorithms preferred where possible. + Maximum interrupt disable time bounded by design — no unbounded + loops while holding locks. Fuel mechanism (SM-RES-002) provides + additional temporal bounding at instruction level. + status: implemented + tags: [temporal, interrupt-latency, asil-b, mechanism] + links: + - type: satisfies + target: REQ_TEMPORAL_004 + fields: + rationale: > + ISO 26262-6:7.4.5 requires bounded interrupt latency. Critical + sections are bounded by design — fuel checks at loop back-edges + ensure no unbounded computation while resources are held. + kiln_sync::Mutex provides platform-appropriate locking. + implementation: kiln-sync/src/mutex.rs, kiln-runtime/src/stackless/engine.rs diff --git a/safety/requirements/safety-requirements.yaml b/safety/requirements/safety-requirements.yaml new file mode 100644 index 000000000..40a37c55e --- /dev/null +++ b/safety/requirements/safety-requirements.yaml @@ -0,0 +1,774 @@ +# Safety Requirements — Consolidated +# +# System: Kiln — WebAssembly runtime for safety-critical systems +# +# This file merges: +# 1. STPA-derived requirements (SR-1 through SR-24) from hazard analysis +# 2. Sphinx-needs safety requirements (REQ_SAFETY_*, REQ_MEM_SAFETY_*, etc.) +# migrated from docs/source/safety_manual/requirements.rst +# +# Merge strategy: +# - Where sphinx-needs overlaps with STPA: keep SR-* ID, add previous-id +# - Where sphinx-needs has no STPA equivalent: preserve original ID +# - ISO 26262 traceability preserved from sphinx-needs +# +# Format: rivet generic-yaml + +artifacts: + # ========================================================================= + # STPA-derived: Execution correctness (from CC-E-*, LS-E-*) + # ========================================================================= + - id: SR-1 + type: requirement + title: Numeric instruction edge-case correctness + description: > + All numeric instructions shall produce results matching the WebAssembly + reference interpreter for boundary inputs: NaN propagation, saturating + conversions, signed division overflow (INT_MIN / -1), and division by + zero. Rust's "as" cast shall not be used for float-to-int conversion + without explicit boundary handling. + status: draft + tags: [execution, numeric, asil-d, stpa-derived] + links: + - type: derives-from + target: CC-E-1 + - type: derives-from + target: LS-E-1 + fields: + implementation: kiln-runtime/src/stackless/engine.rs + spec-reference: "WebAssembly Core Spec 3.0, Section 4.3.1-4.3.3" + verification-method: test + verification-description: > + WAST test suite (i32.wast, i64.wast, f32.wast, f64.wast, conversions.wast) + with zero assertion failures; property-based tests for all 12 conversion + instructions with boundary values + + - id: SR-2 + type: requirement + title: Fuel metering at all control flow points + description: > + Fuel shall be checked before every instruction dispatch when fuel + metering is enabled. This includes loop back-edges, not just block + and function entry. The fuel counter shall be atomic in multi-threaded + configurations. + status: partial + tags: [execution, resource-containment, asil-c, stpa-derived] + links: + - type: derives-from + target: CC-E-2 + - type: derives-from + target: LS-E-2 + fields: + previous-id: REQ_TEMPORAL_002, REQ_LFUNC_007 + iso-26262: "ISO 26262-6:7.4.5" + implementation: kiln-runtime/src/stackless/engine.rs + verification-method: test + verification-description: > + Infinite loop exhausts fuel within configured limit; code review that + all branch targets include fuel check + note: "Fuel mechanism exists (REQ_LFUNC_007 implemented); loop back-edge check not verified" + + - id: SR-3 + type: requirement + title: Memory bounds check uses current size + description: > + Memory bounds checks shall read the memory's current size at each + access, not a cached value. If caching is used for performance, the + cache shall be invalidated on every memory.grow, memory.copy, and + memory.fill that changes memory size. + status: partial + tags: [execution, memory-safety, asil-d, stpa-derived] + links: + - type: derives-from + target: CC-E-3 + - type: derives-from + target: LS-E-3 + fields: + previous-id: REQ_MEM_SAFETY_001 + iso-26262: "ISO 26262-6:7.4.14" + implementation: kiln-runtime/src/stackless/engine.rs + spec-reference: "WebAssembly Core Spec 3.0, Section 4.4.7" + verification-method: test + verification-description: > + WAST tests memory.wast, memory_grow.wast; regression test for access + at old_size..new_size after grow + note: "Bounds checking infrastructure exists; post-grow cache invalidation not verified" + + - id: SR-4 + type: requirement + title: Unknown opcodes trap unconditionally + description: > + 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 + tags: [execution, correctness, stpa-derived] + links: + - type: derives-from + target: CC-E-4 + - type: derives-from + target: LS-E-4 + fields: + implementation: kiln-runtime/src/stackless/engine.rs + verification-method: test + verification-description: > + All undefined opcodes (0x06-0x09 legacy, reserved ranges) produce + a trap, not a silent no-op + + - id: SR-5 + type: requirement + title: Call stack depth limit enforced for all call types + description: > + 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 + tags: [execution, stack-safety, asil-d, stpa-derived] + links: + - type: derives-from + target: CC-E-5 + - type: derives-from + target: LS-E-5 + fields: + previous-id: REQ_MEM_SAFETY_003 + iso-26262: "ISO 26262-6:7.4.14" + implementation: kiln-runtime/src/stackless/engine.rs + verification-method: test + verification-description: > + WAST tests call.wast; tail-call regression for deep return_call chain + note: "Stack overflow protection exists; tail-call depth tracking not verified" + + - id: SR-6 + type: requirement + title: Multi-memory index validation + description: > + 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 + tags: [execution, memory-safety, stpa-derived] + links: + - type: derives-from + target: CC-E-6 + fields: + implementation: kiln-runtime/src/stackless/engine.rs + spec-reference: "WebAssembly Multi-Memory Proposal" + verification-method: test + verification-description: > + Instruction referencing non-existent memory index traps + + # ========================================================================= + # STPA-derived: Decoder correctness (from CC-D-*, LS-D-*) + # ========================================================================= + - id: SR-7 + type: requirement + title: Reject all malformed modules + description: > + 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 + tags: [decoder, validation, asil-d, stpa-derived] + links: + - type: derives-from + target: CC-D-1 + - type: derives-from + target: LS-D-1 + fields: + previous-id: REQ_VERIFY_001 + iso-26262: "ISO 26262-6:9.4.2" + implementation: kiln-decoder/src/streaming_decoder.rs + spec-reference: "WebAssembly Core Spec 3.0, Binary Format" + verification-method: test + verification-description: > + WAST test suite: all assert_malformed tests pass with zero failures + note: "~35 failures remain (Issue 148)" + + - id: SR-8 + type: requirement + title: Resource limits enforced before allocation + description: > + 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 + tags: [decoder, resource-containment, asil-d, stpa-derived] + links: + - type: derives-from + target: CC-D-2 + - type: derives-from + target: LS-D-2 + fields: + previous-id: REQ_RESOURCE_002 + iso-26262: "ISO 26262-6:7.4.3" + implementation: kiln-decoder/src/streaming_decoder.rs + verification-method: test + verification-description: > + Module with count > limit for each section type is rejected + without allocating the full count + note: "Resource limits exist; pre-allocation check order not verified" + + # ========================================================================= + # STPA-derived: Canonical ABI correctness (from CC-CM-*, LS-CM-*) + # ========================================================================= + - id: SR-9 + type: requirement + title: String transcoding handles all encodings correctly + description: > + Canonical ABI string transcoding shall correctly handle UTF-8 (1-4 byte + 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 + tags: [component-model, canonical-abi, strings, stpa-derived] + links: + - type: derives-from + target: CC-CM-1 + - type: derives-from + target: LS-CM-1 + fields: + implementation: kiln-component/src/canonical_abi/ + spec-reference: "Component Model Canonical ABI, String section" + verification-method: test + verification-description: > + Shared wit-bindgen strings fixture with multi-byte characters; + property-based roundtrip test + + - id: SR-10 + type: requirement + title: Record field alignment matches canonical ABI spec + description: > + 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 + tags: [component-model, canonical-abi, alignment, stpa-derived] + links: + - type: derives-from + target: CC-CM-2 + - type: derives-from + target: LS-CM-2 + fields: + implementation: kiln-component/src/canonical_abi/ + spec-reference: "Component Model Canonical ABI, Record section" + verification-method: test + verification-description: > + Shared wit-bindgen records fixture; unit tests for align_up + + - id: SR-11 + type: requirement + title: List element size matches canonical ABI and Meld + description: > + 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 + tags: [component-model, canonical-abi, cross-toolchain, stpa-derived] + links: + - type: derives-from + target: CC-CM-3 + - type: derives-from + target: LS-CM-3 + - type: derives-from + target: LS-CM-6 + fields: + implementation: kiln-component/src/canonical_abi/ + spec-reference: "Component Model Canonical ABI, List section; XH-1" + verification-method: test + verification-description: > + Shared wit-bindgen fixtures run through Kiln; cross-validation of + element sizes for 50+ type patterns vs Meld output + + - id: SR-12 + type: requirement + title: Resource handle no-aliasing guarantee + description: > + Resource table shall guarantee that no two live handles share the same + index. Generation counters or equivalent mechanism shall prevent aliasing + even after rapid create/drop cycles. + status: draft + tags: [component-model, resources, stpa-derived] + links: + - type: derives-from + target: CC-CM-4 + - type: derives-from + target: LS-CM-4 + fields: + previous-id: REQ_CMP_020 + implementation: kiln-component/src/components/resource_management.rs + verification-method: test + verification-description: > + Create/drop/create cycle verifies no aliasing; 10000-cycle stress test + + - id: SR-13 + type: requirement + title: Double-drop detection and trap + description: > + Dropping a resource handle that has already been dropped shall produce + a trap, not corrupt the resource table. + status: draft + tags: [component-model, resources, stpa-derived] + links: + - type: derives-from + target: CC-CM-5 + fields: + implementation: kiln-component/src/components/resource_management.rs + verification-method: test + verification-description: > + Create, drop, drop again: verify trap on second drop + + # ========================================================================= + # STPA-derived: Cross-component correctness (from CC-L-*, LS-L-*) + # ========================================================================= + - id: SR-14 + type: requirement + title: Import resolution uses fully-qualified versioned names + status: draft + tags: [linker, component-model, stpa-derived] + links: + - type: derives-from + target: CC-L-1 + - type: derives-from + target: LS-L-1 + fields: + implementation: kiln-component/src/components/component_instantiation.rs + + - id: SR-15 + type: requirement + title: Type compatibility verified at link time + status: partial + tags: [linker, type-safety, stpa-derived] + links: + - type: derives-from + target: CC-L-2 + - type: derives-from + target: LS-L-2 + fields: + implementation: kiln-component/src/components/component_instantiation.rs + note: "~235 assert_unlinkable failures remain (Issue 149)" + + - id: SR-16 + type: requirement + title: Instantiation order respects dependency graph + status: draft + tags: [linker, component-model, stpa-derived] + links: + - type: derives-from + target: CC-L-3 + fields: + implementation: kiln-component/src/components/component_instantiation.rs + + # ========================================================================= + # STPA-derived: WASI correctness (from CC-W-*, LS-W-*) + # ========================================================================= + - id: SR-17 + type: requirement + title: Per-component capability isolation + status: draft + tags: [wasi, capability-isolation, asil-d, stpa-derived] + links: + - type: derives-from + target: CC-W-1 + - type: derives-from + target: LS-W-1 + fields: + implementation: kiln-wasi/src/dispatcher.rs + + - id: SR-18 + type: requirement + title: Monotonic clock enforcement + status: draft + tags: [wasi, clocks, stpa-derived] + links: + - type: derives-from + target: CC-W-2 + - type: derives-from + target: LS-W-2 + fields: + implementation: kiln-wasi/src/dispatcher.rs + spec-reference: "WASI v0.2.3, wasi:clocks/monotonic-clock" + + - id: SR-19 + type: requirement + title: Cryptographic random or explicit error + status: draft + tags: [wasi, random, security, stpa-derived] + links: + - type: derives-from + target: CC-W-3 + fields: + implementation: kiln-wasi/src/dispatcher.rs + + # ========================================================================= + # STPA-derived: CFI correctness (from CC-CFI-*, LS-CFI-*) + # ========================================================================= + - id: SR-20 + type: requirement + title: Shadow stack instrumented for all call paths + status: draft + tags: [cfi, control-flow-integrity, stpa-derived] + links: + - type: derives-from + target: CC-CFI-1 + - type: derives-from + target: LS-CFI-1 + fields: + implementation: kiln-runtime/src/cfi_engine.rs + + - id: SR-21 + type: requirement + title: call_indirect validates against instruction type_idx + status: draft + tags: [cfi, type-safety, stpa-derived] + links: + - type: derives-from + target: CC-CFI-2 + - type: derives-from + target: LS-CFI-2 + fields: + previous-id: REQ_DATAFLOW_001 + implementation: kiln-runtime/src/stackless/engine.rs + + # ========================================================================= + # STPA-derived: Allocation correctness (from CC-A-*, LS-A-*) + # ========================================================================= + - id: SR-22 + type: requirement + title: ASIL-D mode rejects dynamic allocation + status: partial + tags: [allocation, asil-d, stpa-derived] + links: + - type: derives-from + target: CC-A-1 + - type: derives-from + target: LS-A-1 + fields: + previous-id: REQ_RESOURCE_001 + iso-26262: "ISO 26262-6:7.4.4" + implementation: kiln-foundation/src/capabilities/memory_factory.rs + note: "safe_managed_alloc! macro in place; transitive dependency analysis not automated" + + - id: SR-23 + type: requirement + title: BoundedVec uses configured capacity, not allocator capacity + status: draft + tags: [allocation, bounded-collections, stpa-derived] + links: + - type: derives-from + target: CC-A-2 + - type: derives-from + target: LS-A-2 + fields: + implementation: kiln-foundation/src/collections/bounded_vec.rs + + # ========================================================================= + # STPA-derived: Cross-toolchain consistency + # ========================================================================= + - id: SR-24 + type: requirement + title: Shared wit-bindgen fixtures pass through Kiln + status: draft + tags: [cross-toolchain, canonical-abi, integration, stpa-derived] + links: + - type: derives-from + target: CC-CM-8 + - type: derives-from + target: LS-CM-6 + fields: + implementation: kiln-component/src/canonical_abi/ + note: "Blocking: kiln-runtime fixture coverage currently empty" + + # ========================================================================= + # Migrated from sphinx-needs: General Safety (no STPA equivalent) + # These are operational/design-level safety properties not directly + # derived from STPA hazard analysis. + # ========================================================================= + - id: REQ_SAFETY_001 + type: requirement + title: Safety-critical operation mode + description: > + The runtime shall provide a safety-critical operation mode with + deterministic behavior, disabled dynamic features, and comprehensive + error detection. + status: implemented + tags: [safety-policy, asil-d, migrated-from-sphinx] + fields: + iso-26262: "ISO 26262-6:7.4.2" + implementation: kiln-runtime (feature flags) + verification-method: test, analysis + + - id: REQ_SAFETY_003 + type: requirement + title: Fail-safe behavior + description: > + Upon detection of any safety-critical fault, the runtime shall + transition to a fail-safe state and notify the system-level error + handler. + status: implemented + tags: [safety-policy, asil-d, migrated-from-sphinx] + fields: + iso-26262: "ISO 26262-6:7.4.3" + verification-method: test, analysis + + - id: REQ_SAFETY_004 + type: requirement + title: Safety mechanism independence + description: > + Safety mechanisms shall be independent from the functionality they + protect to avoid common cause failures. + status: implemented + tags: [safety-policy, asil-d, migrated-from-sphinx] + fields: + iso-26262: "ISO 26262-6:7.4.10" + verification-method: analysis + + # ========================================================================= + # Migrated from sphinx-needs: Memory Safety (supplements STPA SR-3, SR-5) + # ========================================================================= + - id: REQ_MEM_SAFETY_002 + type: requirement + title: Memory isolation between module instances + description: > + WebAssembly module instances shall be isolated from each other with + no shared mutable state except through explicit, validated interfaces. + status: implemented + tags: [memory-safety, asil-d, migrated-from-sphinx] + fields: + iso-26262: "ISO 26262-6:7.4.13" + implementation: kiln-runtime/src/memory.rs + verification-method: test, analysis + + - id: REQ_MEM_SAFETY_004 + type: requirement + title: Memory initialization enforcement + description: > + All allocated memory shall be initialized to a known safe state + before use. Uninitialized memory access shall be prevented. + status: implemented + tags: [memory-safety, asil-c, migrated-from-sphinx] + fields: + iso-26262: "ISO 26262-6:8.4.4" + verification-method: test, inspection + + - id: REQ_MEM_SAFETY_005 + type: requirement + title: Memory lifetime management + description: > + Memory lifetime shall be explicitly managed. Use-after-free and + double-free conditions shall be prevented through RAII and + capability-based allocation (safe_managed_alloc!). + status: implemented + tags: [memory-safety, asil-c, migrated-from-sphinx] + fields: + iso-26262: "ISO 26262-6:7.4.13" + implementation: kiln-foundation/src/capabilities/memory_factory.rs + verification-method: analysis, test + + # ========================================================================= + # Migrated from sphinx-needs: Resource Management (supplements SR-8, SR-22) + # ========================================================================= + - id: REQ_RESOURCE_003 + type: requirement + title: Resource exhaustion handling + description: > + Resource exhaustion shall be detected before system destabilization. + Graceful degradation strategies shall be implemented for non-critical + resources. + status: implemented + tags: [resource-management, asil-c, migrated-from-sphinx] + fields: + iso-26262: "ISO 26262-6:7.4.3" + verification-method: test + + - id: REQ_RESOURCE_004 + type: requirement + title: Resource usage monitoring + description: > + Resource usage shall be continuously monitored and reported. High + watermarks shall be tracked for capacity planning. + status: partial + tags: [resource-management, asil-b, migrated-from-sphinx] + fields: + iso-26262: "ISO 26262-6:8.4.8" + implementation: kiln-foundation/src/monitoring.rs + note: "~1800 lines of monitoring infrastructure exist but not yet wired to allocations" + + # ========================================================================= + # Migrated from sphinx-needs: Error Handling + # ========================================================================= + - id: REQ_ERROR_001 + type: requirement + title: Comprehensive error detection + description: > + All detectable error conditions shall be explicitly checked. Error + detection coverage shall be measured and documented. + status: implemented + tags: [error-handling, asil-d, migrated-from-sphinx] + fields: + iso-26262: "ISO 26262-6:7.4.6" + implementation: kiln-error/src/lib.rs + verification-method: test, analysis + + - id: REQ_ERROR_002 + type: requirement + title: Error propagation control + description: > + Errors shall be propagated through explicit return values (Result types). + Exception-based error handling shall not be used in safety-critical paths. + status: implemented + tags: [error-handling, asil-d, migrated-from-sphinx] + fields: + iso-26262: "ISO 26262-6:7.4.7" + verification-method: analysis + + - id: REQ_ERROR_003 + type: requirement + title: Error recovery actions + description: > + For each error category, specific recovery actions shall be defined. + Transient: retry with backoff. Resource: graceful degradation. + Logic: fail-safe shutdown. Hardware: system notification. + status: implemented + tags: [error-handling, asil-c, migrated-from-sphinx] + fields: + iso-26262: "ISO 26262-6:7.4.3" + verification-method: test + + # ========================================================================= + # Migrated from sphinx-needs: Verification + # ========================================================================= + - id: REQ_VERIFY_002 + type: requirement + title: Runtime integrity checks + description: > + Critical data structures shall include integrity checks (checksums, + magic values, redundancy) to detect corruption. + status: implemented + tags: [verification, asil-d, migrated-from-sphinx] + fields: + iso-26262: "ISO 26262-6:7.4.8" + verification-method: test + + - id: REQ_VERIFY_004 + type: requirement + title: Continuous monitoring + description: > + Safety-critical invariants shall be continuously monitored during + operation. Violations shall trigger immediate safety actions. + status: implemented + tags: [verification, asil-c, migrated-from-sphinx] + fields: + iso-26262: "ISO 26262-6:7.4.8" + verification-method: test, analysis + + # ========================================================================= + # Migrated from sphinx-needs: Temporal Safety + # ========================================================================= + - id: REQ_TEMPORAL_001 + type: requirement + title: Bounded execution time + description: > + All operations shall complete within bounded time. Worst-case + execution time (WCET) shall be determinable through static analysis. + status: implemented + tags: [temporal, asil-d, migrated-from-sphinx] + fields: + iso-26262: "ISO 26262-6:7.4.5" + implementation: kiln-runtime/src/stackless/engine.rs + verification-method: test, analysis + + - id: REQ_TEMPORAL_003 + type: requirement + title: Deadline monitoring + description: > + Time-critical operations shall be monitored for deadline compliance. + Deadline misses shall be reported to the system scheduler. + status: partial + tags: [temporal, asil-c, migrated-from-sphinx] + fields: + iso-26262: "ISO 26262-6:7.4.5" + verification-method: test + + - id: REQ_TEMPORAL_004 + type: requirement + title: Interrupt latency bounds + description: > + Maximum interrupt disable time shall be bounded and documented. + Critical sections shall be minimized. + status: implemented + tags: [temporal, asil-b, migrated-from-sphinx] + fields: + iso-26262: "ISO 26262-6:7.4.5" + verification-method: test, measurement + + # ========================================================================= + # Migrated from sphinx-needs: Data Flow Safety + # ========================================================================= + - id: REQ_DATAFLOW_002 + type: requirement + title: Information flow control + description: > + Information flow between different criticality levels shall be + controlled and validated. High-criticality data shall not flow + to low-criticality domains without explicit authorization. + status: partial + tags: [data-flow, asil-c, migrated-from-sphinx] + fields: + iso-26262: "ISO 26262-6:7.4.13" + verification-method: analysis + + - id: REQ_DATAFLOW_003 + type: requirement + title: Data validation at system boundaries + description: > + All external inputs shall be validated before use. Range checks, + format checks, and consistency checks shall be applied. + status: implemented + tags: [data-flow, asil-c, migrated-from-sphinx] + fields: + iso-26262: "ISO 26262-6:8.4.4" + implementation: kiln-decoder/src/streaming_decoder.rs + verification-method: test + + # ========================================================================= + # Migrated from sphinx-needs: Configuration Safety + # ========================================================================= + - id: REQ_CONFIG_001 + type: requirement + title: Configuration validation + description: > + Configuration parameters shall be validated against safety constraints + before activation. Invalid configurations shall be rejected. + status: implemented + tags: [configuration, asil-d, migrated-from-sphinx] + fields: + iso-26262: "ISO 26262-6:9.4.4" + verification-method: test, analysis + + - id: REQ_CONFIG_003 + type: requirement + title: Safe defaults + description: > + All configuration parameters shall have safe default values. The + system shall operate safely with default configuration. + status: implemented + tags: [configuration, asil-b, migrated-from-sphinx] + fields: + iso-26262: "ISO 26262-6:7.4.2" + verification-method: review, test + + # ========================================================================= + # REMOVED from sphinx-needs (with rationale): + # + # REQ_SAFETY_002 (Safety Manual Compliance) — process requirement, not + # a code property; tracked in qualification documentation + # + # REQ_ERROR_004 (Error Logging and Reporting) — operational; covered by + # kiln_foundation::tracing framework (implemented) + # + # REQ_VERIFY_003 (Built-In Test / POST) — not applicable to a library + # runtime; POST is the embedder's responsibility + # + # REQ_CONFIG_002 (Configuration Integrity) — checksums/redundancy for + # config data is the embedder's responsibility in SEooC model + # ========================================================================= diff --git a/safety/stpa/control-structure-diagram.md b/safety/stpa/control-structure-diagram.md new file mode 100644 index 000000000..c6ba8a5ba --- /dev/null +++ b/safety/stpa/control-structure-diagram.md @@ -0,0 +1,122 @@ +# Kiln Control Structure Diagram + +```mermaid +graph TB + subgraph "Environment (outside system boundary)" + HOST["CTRL-HOST
Host Application / Gale Task"] + MELD["Meld (build-time)"] + SYNTH["Synth (AOT compile)"] + HW["Hardware / Platform"] + end + + subgraph "Kiln System Boundary" + subgraph "Frontend" + DECODER["CTRL-DECODER
Module/Component Decoder
kiln-decoder"] + LINKER["CTRL-LINKER
Component Linker
kiln-component"] + end + + subgraph "Execution Core" + ENGINE["CTRL-ENGINE
Execution Engine
kiln-runtime"] + CFI["CTRL-CFI
CFI Engine
kiln-runtime/cfi"] + CM["CTRL-CM
Component Model
kiln-component"] + end + + subgraph "Host Services" + WASI["CTRL-WASI
WASI Dispatcher
kiln-wasi"] + BLAST["CTRL-BLAST
Blast Zone
kiln-component"] + end + + subgraph "Foundation" + ALLOC["CTRL-ALLOC
Allocation Manager
kiln-foundation"] + end + + subgraph "Controlled Processes" + INST["PROC-INSTRUCTION"] + MEM["PROC-MEMORY"] + STACK["PROC-STACK"] + MOD["PROC-MODULE"] + INSTANCE["PROC-INSTANCE"] + CANON["PROC-CANONICAL"] + RES["PROC-RESOURCE"] + SHADOW["PROC-SHADOW"] + IO["PROC-IO"] + BUDGET["PROC-BUDGET"] + end + end + + %% Host → System + HOST -->|"CA-HOST-1: Create engine"| ENGINE + HOST -->|"CA-HOST-2: Load module"| DECODER + HOST -->|"CA-HOST-3: Define imports"| LINKER + HOST -->|"CA-HOST-4: Call export"| ENGINE + + %% External tools (environment) + MELD -.->|"Fused core module"| HOST + SYNTH -.->|"AOT binary"| HOST + + %% Frontend → Execution + DECODER -->|"CA-DEC-1: Parse"| MOD + DECODER -->|"CA-DEC-3: Detect format"| MOD + LINKER -->|"CA-LINK-1: Resolve"| INSTANCE + LINKER -->|"CA-LINK-2: Instantiate"| INSTANCE + + %% Execution Core + ENGINE -->|"CA-ENG-1: Dispatch"| INST + ENGINE -->|"CA-ENG-2: Load/Store"| MEM + ENGINE -->|"CA-ENG-3: Push/Pop"| STACK + ENGINE -->|"CA-ENG-4: Validate CF"| CFI + ENGINE -->|"CA-ENG-5: Cross-component"| CM + + %% CFI + CFI -->|"CA-CFI-1: Push return"| SHADOW + CFI -->|"CA-CFI-2: Validate return"| SHADOW + + %% Component Model + CM -->|"CA-CM-1: Lift"| CANON + CM -->|"CA-CM-2: Lower"| CANON + CM -->|"CA-CM-3: Resource op"| RES + CM -->|"CA-CM-6: Isolate fault"| BLAST + + %% WASI + WASI -->|"CA-WASI-1: FS op"| IO + WASI -->|"CA-WASI-2: Clock/Random"| IO + + %% Allocation + ALLOC -->|"CA-ALLOC-1: Allocate"| BUDGET + + %% Feedback (dashed) + ENGINE -.->|"Result/Trap"| HOST + INST -.->|"Result"| ENGINE + MEM -.->|"Value/OOB"| ENGINE + SHADOW -.->|"Pass/Fail"| CFI + CFI -.->|"Violation"| ENGINE + CANON -.->|"Values/Error"| CM + CM -.->|"Call result"| ENGINE + IO -.->|"Result/Denial"| WASI + BUDGET -.->|"Success/Failure"| ALLOC + + %% Cross-toolchain boundary (XH-1 through XH-5) + CM -.->|"XH-1: Element sizes"| MELD + CM -.->|"XH-3: Element sizes"| SYNTH +``` + +## Controller Summary + +| Controller | Crate | Control Actions | UCAs | Constraints | +|-----------|-------|----------------|------|-------------| +| CTRL-HOST | (external) | 5 | - | - | +| CTRL-ENGINE | kiln-runtime | 5 | 6 | 6 | +| CTRL-DECODER | kiln-decoder | 3 | 3 | 3 | +| CTRL-LINKER | kiln-component | 3 | 3 | 3 | +| CTRL-CM | kiln-component | 6 | 8 | 8 | +| CTRL-CFI | kiln-runtime | 3 | 3 | 3 | +| CTRL-WASI | kiln-wasi | 3 | 3 | 3 | +| CTRL-BLAST | kiln-component | 2 | 1 | 1 | +| CTRL-ALLOC | kiln-foundation | 2 | 2 | 2 | + +## Cross-Toolchain Boundaries + +The dotted lines from CTRL-CM to Meld and Synth represent cross-toolchain +consistency hazards (XH-1 through XH-5). These are not control actions but +rather constraints that must be satisfied across independent tool +implementations. diff --git a/safety/stpa/control-structure.yaml b/safety/stpa/control-structure.yaml new file mode 100644 index 000000000..9fcd97787 --- /dev/null +++ b/safety/stpa/control-structure.yaml @@ -0,0 +1,317 @@ +# STPA Step 2: Control Structure +# +# System: Kiln — WebAssembly runtime for safety-critical systems +# +# Kiln is a runtime system. Unlike Meld (a build-time tool), Kiln's control +# structure has real-time feedback loops, concurrent execution paths, and +# external I/O. The controllers operate during program execution, not during +# a one-shot transformation. +# +# Relation to BA RFC #46: The RFC's "Host C API for Lowered Components" and +# "Host C API for Embedder Bindings" are implemented by Kiln's controllers. +# The RFC proposes abstract C API functions; Kiln provides concrete Rust +# implementations with safety-level guarantees. + +controllers: + - id: CTRL-HOST + name: Host Application / Gale Task + type: human-and-automated + description: > + The host application (or gale RTOS task) that creates a Kiln engine, + loads modules/components, configures capabilities, and invokes exports. + In embedded systems, this is the main task or an ISR-triggered handler. + In std systems, this is the application binary using kiln as a library. + control-actions: + - ca: CA-HOST-1 + target: CTRL-ENGINE + action: Create engine with configuration (fuel, memory limits, safety level) + - ca: CA-HOST-2 + target: CTRL-ENGINE + action: Load and validate module/component bytes + - ca: CA-HOST-3 + target: CTRL-LINKER + action: Define host functions and WASI capabilities + - ca: CA-HOST-4 + target: CTRL-ENGINE + action: Call exported function with arguments + - ca: CA-HOST-5 + target: CTRL-ENGINE + action: Read/write memory and globals + feedback: + - from: CTRL-ENGINE + info: Execution result (return values, trap, fuel exhausted) + process-model: + - Module/component bytes are valid WebAssembly + - Fuel and memory limits are appropriate for the target platform + - Safety level matches the system's certification target + + - id: CTRL-ENGINE + name: Execution Engine + type: automated + description: > + The core execution engine in kiln-runtime. Interprets or dispatches + WebAssembly instructions, manages the value stack and call stack, + tracks fuel consumption, and enforces resource budgets. Contains + the cfi_engine for control flow integrity. + source-crate: kiln-runtime + control-actions: + - ca: CA-ENG-1 + target: PROC-INSTRUCTION + action: Fetch, decode, and dispatch next instruction + - ca: CA-ENG-2 + target: PROC-MEMORY + action: Execute memory load/store with bounds check + - ca: CA-ENG-3 + target: PROC-STACK + action: Push/pop values, manage call frames + - ca: CA-ENG-4 + target: CTRL-CFI + action: Validate control flow (calls, returns, indirect calls) + - ca: CA-ENG-5 + target: CTRL-CM + action: Dispatch cross-component call + feedback: + - from: PROC-INSTRUCTION + info: Instruction result, trap condition + - from: PROC-MEMORY + info: Loaded value, OOB trap + - from: CTRL-CFI + info: CFI violation detected / clear + - from: CTRL-CM + info: Cross-component call result + process-model: + - Program counter is within valid code range + - Value stack depth matches expected type for current instruction + - Fuel remaining > 0 (if fuel metering enabled) + - Call stack depth < maximum + + - id: CTRL-DECODER + name: Module/Component Decoder + type: automated + description: > + Parses WebAssembly binary format (kiln-decoder, kiln-format). + Validates section ordering, type consistency, and resource limits. + Detects whether input is a core module or component. Enforces + configurable limits (max functions, max memories, max types). + source-crate: kiln-decoder + control-actions: + - ca: CA-DEC-1 + target: PROC-MODULE + action: Parse and validate module sections + - ca: CA-DEC-2 + target: PROC-MODULE + action: Enforce resource limits from configuration + - ca: CA-DEC-3 + target: PROC-MODULE + action: Detect component vs core module format + feedback: + - from: PROC-MODULE + info: Parsed module/component structure, validation errors + + - id: CTRL-LINKER + name: Component Linker + type: automated + description: > + Resolves imports to exports across component instances. Manages + the instance graph. Maps component-level imports to host functions, + WASI implementations, or other component exports. In meld-fused + scenarios, the linker handles the remaining host/WASI imports that + meld could not resolve at fusion time. + source-crate: kiln-component + control-actions: + - ca: CA-LINK-1 + target: PROC-INSTANCE + action: Resolve import to host function or component export + - ca: CA-LINK-2 + target: PROC-INSTANCE + action: Instantiate module with resolved imports + - ca: CA-LINK-3 + target: PROC-INSTANCE + action: Verify type compatibility at link boundary + feedback: + - from: PROC-INSTANCE + info: Instantiated module, unresolved imports, type errors + + - id: CTRL-CM + name: Component Model Executor + type: automated + description: > + Implements the Component Model canonical ABI. Handles lifting + (core→component), lowering (component→core), resource lifecycle, + cross-component communication, async task management, and + virtualization. The largest and most complex controller. + source-crate: kiln-component + control-actions: + - ca: CA-CM-1 + target: PROC-CANONICAL + action: Lift core values to component values + - ca: CA-CM-2 + target: PROC-CANONICAL + action: Lower component values to core values + - ca: CA-CM-3 + target: PROC-RESOURCE + action: Create, transfer, or drop resource handle + - ca: CA-CM-4 + target: PROC-ASYNC + action: Schedule, suspend, or resume async task + - ca: CA-CM-5 + target: PROC-STREAM + action: Read from or write to stream/future + - ca: CA-CM-6 + target: CTRL-BLAST + action: Isolate component fault within blast zone + feedback: + - from: PROC-CANONICAL + info: Lifted/lowered values, encoding errors + - from: PROC-RESOURCE + info: Handle validity, table state + - from: PROC-ASYNC + info: Task state, completion, cancellation + process-model: + - Resource table entries are valid (no dangling handles) + - Async task DAG has no cycles + - Stream/future buffers are exclusively owned by one task + + - id: CTRL-CFI + name: Control Flow Integrity Engine + type: automated + description: > + Shadow stack + indirect call validation. Maintains a parallel stack + of return addresses. On every call, pushes expected return address. + On every return, compares actual vs expected. On indirect calls, + validates the target function's type signature. Configurable violation + policy: trap, log, or continue. + source-crate: kiln-runtime (cfi_engine) + control-actions: + - ca: CA-CFI-1 + target: PROC-SHADOW + action: Push return address on call + - ca: CA-CFI-2 + target: PROC-SHADOW + action: Validate return address on return + - ca: CA-CFI-3 + target: PROC-SHADOW + action: Validate indirect call target type + feedback: + - from: PROC-SHADOW + info: Validation pass/fail, violation details + + - id: CTRL-WASI + name: WASI Host Implementation + type: automated + description: > + Implements WASI Preview 2 interfaces: filesystem, CLI, clocks, I/O, + random, sockets. Enforces capability-based security model. Each + component instance has its own WasiCapabilities set. The dispatcher + routes WASI calls to the appropriate implementation. + source-crate: kiln-wasi + control-actions: + - ca: CA-WASI-1 + target: PROC-IO + action: Execute filesystem operation with capability check + - ca: CA-WASI-2 + target: PROC-IO + action: Execute clock/random operation + - ca: CA-WASI-3 + target: PROC-IO + action: Execute socket operation with capability check + feedback: + - from: PROC-IO + info: Operation result, capability denial, I/O error + + - id: CTRL-BLAST + name: Blast Zone Fault Isolation + type: automated + description: > + Containment mechanism for component faults. When a component traps, + the blast zone prevents the fault from propagating to other components + or the runtime. Configurable containment policies. + source-crate: kiln-component (blast_zone) + control-actions: + - ca: CA-BLAST-1 + target: PROC-INSTANCE + action: Isolate faulting component + - ca: CA-BLAST-2 + target: PROC-INSTANCE + action: Report fault to host with diagnostic info + + - id: CTRL-ALLOC + name: Safety-Level Allocation Manager + type: automated + description: > + Enforces the four-layer memory management strategy. Routes allocation + requests through safe_managed_alloc! macro. Tracks per-crate budgets. + In ASIL-D mode, rejects dynamic allocation entirely. In bounded mode, + enforces capacity limits on all collections. + source-crate: kiln-foundation + control-actions: + - ca: CA-ALLOC-1 + target: PROC-BUDGET + action: Allocate memory within per-crate budget + - ca: CA-ALLOC-2 + target: PROC-BUDGET + action: Reject allocation that exceeds budget or safety level + feedback: + - from: PROC-BUDGET + info: Allocation success/failure, remaining budget + +controlled-processes: + - id: PROC-INSTRUCTION + name: Instruction Stream + description: WebAssembly bytecode being decoded and executed + + - id: PROC-MEMORY + name: Linear Memory + description: > + WebAssembly linear memory instances (one per memory in multi-memory + mode). Protected by bounds checks and optionally MPU regions. + + - id: PROC-STACK + name: Value and Call Stack + description: > + The operand value stack and call frame stack. Bounded by maximum + depth configuration. + + - id: PROC-MODULE + name: Module/Component Binary + description: Raw WebAssembly bytes being parsed and validated + + - id: PROC-INSTANCE + name: Module/Component Instance + description: > + Instantiated module with resolved imports, allocated memories, + initialized tables, and executed start function. + + - id: PROC-CANONICAL + name: Canonical ABI Values + description: > + Values being lifted (core→component) or lowered (component→core) + through the Component Model canonical ABI. + + - id: PROC-RESOURCE + name: Resource Handle Table + description: > + Table mapping resource handle indices to resource values. Tracks + ownership, borrowing, and lifecycle state. + + - id: PROC-ASYNC + name: Async Task Queue + description: > + Queue of async tasks (streams, futures, waitables) managed by the + Component Model executor. + + - id: PROC-STREAM + name: Stream/Future Buffers + description: Buffers for inter-component async data transfer + + - id: PROC-SHADOW + name: CFI Shadow Stack + description: Parallel stack of expected return addresses for CFI validation + + - id: PROC-IO + name: Host I/O Operations + description: WASI filesystem, clock, random, and socket operations + + - id: PROC-BUDGET + name: Allocation Budget + description: Per-crate memory budget tracked by the allocation manager diff --git a/safety/stpa/controller-constraints.yaml b/safety/stpa/controller-constraints.yaml new file mode 100644 index 000000000..937e1e0d0 --- /dev/null +++ b/safety/stpa/controller-constraints.yaml @@ -0,0 +1,303 @@ +# STPA Step 3b: Controller Constraints +# +# System: Kiln — WebAssembly runtime for safety-critical systems +# +# Each controller constraint is derived from one or more UCAs. It specifies +# the required behavior of a controller to prevent the unsafe control action. + +controller-constraints: + # ========================================================================= + # Execution Engine constraints + # ========================================================================= + - id: CC-E-1 + controller: CTRL-ENGINE + constraint: > + Engine shall implement all numeric instructions with correct edge-case + semantics, including NaN propagation (canonical NaN vs arithmetic NaN), + saturating conversions (clamp, not trap), and division (truncation toward + zero for signed, trap on div-by-zero and INT_MIN/-1 overflow). + ucas: [UCA-E-1] + hazards: [H-1] + + - id: CC-E-2 + controller: CTRL-ENGINE + constraint: > + Engine shall decrement the fuel counter before each instruction dispatch + and trap immediately when fuel reaches zero. No instruction shall execute + with fuel <= 0. + ucas: [UCA-E-2] + hazards: [H-3] + + - id: CC-E-3 + controller: CTRL-ENGINE + constraint: > + Every memory access shall check offset + size <= memory.size * PAGE_SIZE. + After memory.grow, the bounds check shall use the updated size. The check + shall handle u32 overflow (offset + size wrapping). + ucas: [UCA-E-3] + hazards: [H-2] + + - id: CC-E-4 + controller: CTRL-ENGINE + constraint: > + Opcode dispatch shall use the exact byte sequence from the instruction + stream. Multi-byte opcodes (0xFC, 0xFD, 0xFE prefixes) shall decode the + full opcode before dispatch. Unknown opcodes shall trap, not fall through. + ucas: [UCA-E-4] + hazards: [H-1] + + - id: CC-E-5 + controller: CTRL-ENGINE + constraint: > + Call stack depth shall be checked before every call instruction. When the + maximum depth is reached, the engine shall trap with stack overflow. The + maximum depth shall be configurable and default to a safe value. + ucas: [UCA-E-5] + hazards: [H-2, H-3] + + - id: CC-E-6 + controller: CTRL-ENGINE + constraint: > + In multi-memory mode, the memory index operand of every memory instruction + shall be validated against the module's declared memory count. The engine + shall not default to memory 0 when an invalid index is provided. + ucas: [UCA-E-6] + hazards: [H-2] + + # ========================================================================= + # Decoder constraints + # ========================================================================= + - id: CC-D-1 + controller: CTRL-DECODER + constraint: > + Decoder shall reject all modules and components that fail any validation + check defined in the WebAssembly spec. Section ordering, type consistency, + function body validation, and all custom section constraints shall be + enforced. No invalid bytecode shall reach the engine. + ucas: [UCA-D-1] + hazards: [H-1, H-2] + + - id: CC-D-2 + controller: CTRL-DECODER + constraint: > + Decoder shall enforce configurable resource limits (max functions, max + memories, max types, max globals, max tables, max elements) and reject + modules that exceed any limit. Default limits shall be safe for the + target platform's memory budget. + ucas: [UCA-D-2] + hazards: [H-3] + + - id: CC-D-3 + controller: CTRL-DECODER + constraint: > + Decoder shall correctly distinguish core modules (magic + version 1) from + components (magic + version 0x0d00) and route to the appropriate + instantiation path. Ambiguous or unknown version bytes shall be rejected. + ucas: [UCA-D-3] + hazards: [H-4, H-5] + + # ========================================================================= + # Component Model constraints + # ========================================================================= + - id: CC-CM-1 + controller: CTRL-CM + constraint: > + String transcoding shall correctly handle all UTF-8 encodings including + multi-byte characters (2, 3, 4 bytes), surrogate pairs in UTF-16, and + the full Unicode range. Code unit counts shall match the encoded length. + ucas: [UCA-CM-1] + hazards: [H-4] + + - id: CC-CM-2 + controller: CTRL-CM + constraint: > + Record field offsets shall be computed using the canonical ABI's align_up + function: offset = align_up(current_offset, field_alignment). The + implementation shall match the spec's pseudocode exactly. + ucas: [UCA-CM-2] + hazards: [H-4] + + - id: CC-CM-3 + controller: CTRL-CM + constraint: > + List element size shall be computed as align_up(sum_of_field_sizes, + max_alignment) for composite elements. This shall be tested against + Meld's canonical_abi_element_size() for all type families. + ucas: [UCA-CM-3] + hazards: [H-4] + + - id: CC-CM-4 + controller: CTRL-CM + constraint: > + Resource handle allocation shall never reuse an index that is still live. + The resource table shall use generation counters or a free list that + guarantees no aliasing between create and the previous drop. + ucas: [UCA-CM-4] + hazards: [H-6] + + - id: CC-CM-5 + controller: CTRL-CM + constraint: > + Resource drop shall validate the handle is live before dropping. A + second drop of the same handle shall trap, not corrupt the table. + The table shall track which handles are live vs dropped. + ucas: [UCA-CM-5] + hazards: [H-6] + + - id: CC-CM-6 + controller: CTRL-CM + constraint: > + Async task state machine shall track task lifecycle (created, running, + suspended, completed, cancelled). A cancelled task shall never transition + to running. The state machine shall be enforced by the type system or + runtime checks. + ucas: [UCA-CM-6] + hazards: [H-7] + + - id: CC-CM-7 + controller: CTRL-CM + constraint: > + Cross-component call dispatch shall use the linker's resolution table + to map (source_instance, import_index) to (target_instance, export_index). + The dispatch shall not use hardcoded instance indices or fallback logic. + ucas: [UCA-CM-7] + hazards: [H-5] + + - id: CC-CM-8 + controller: CTRL-CM + constraint: > + Canonical ABI element size, field alignment, and string encoding shall + produce results identical to Meld's and Synth's implementations. This + shall be verified by running the shared wit-bindgen fixture suite through + Kiln. Any disagreement is a blocking defect. + ucas: [UCA-CM-8] + hazards: [H-4] + + # ========================================================================= + # Linker constraints + # ========================================================================= + - id: CC-L-1 + controller: CTRL-LINKER + constraint: > + Import resolution shall use fully-qualified names (module:field) and + shall reject ambiguous matches. When multiple exports match, the linker + shall report an error rather than choosing arbitrarily. + ucas: [UCA-L-1] + hazards: [H-5] + + - id: CC-L-2 + controller: CTRL-LINKER + constraint: > + Type compatibility between import and export shall be verified at link + time. Function signatures shall match exactly (parameter types and + result types). Type-mismatched links shall be rejected with a diagnostic. + ucas: [UCA-L-2] + hazards: [H-5] + + - id: CC-L-3 + controller: CTRL-LINKER + constraint: > + Module instantiation order shall respect the dependency graph. The + linker shall topologically sort instances and reject cycles. No module + shall be instantiated before all its imports are resolved. + ucas: [UCA-L-3] + hazards: [H-5] + + # ========================================================================= + # CFI constraints + # ========================================================================= + - id: CC-CFI-1 + controller: CTRL-CFI + constraint: > + Every call instruction (call, call_indirect, call_ref, return_call) + shall push the expected return address to the shadow stack. This + includes host-to-guest calls and cross-component calls. + ucas: [UCA-CFI-1] + hazards: [H-9] + + - id: CC-CFI-2 + controller: CTRL-CFI + constraint: > + call_indirect type validation shall use the type annotation from the + instruction, not the table element's declared type. The comparison + shall account for subtyping if GC types are enabled. + ucas: [UCA-CFI-2] + hazards: [H-9] + + - id: CC-CFI-3 + controller: CTRL-CFI + constraint: > + CFI violation policy shall default to "trap" in all safety-critical + configurations (ASIL-A and above). The "continue" policy shall only + be available in QM/development mode and shall emit a warning at + configuration time. + ucas: [UCA-CFI-3] + hazards: [H-8, H-9] + + # ========================================================================= + # WASI constraints + # ========================================================================= + - id: CC-W-1 + controller: CTRL-WASI + constraint: > + Every WASI operation shall check the calling component's WasiCapabilities + before execution. The capability set shall be resolved from the component + instance ID, not from a global or shared state. In multi-component + scenarios, capability isolation shall be verified. + ucas: [UCA-W-1] + hazards: [H-8] + + - id: CC-W-2 + controller: CTRL-WASI + constraint: > + Clock reads shall be monotonic (each read >= previous read for the same + clock). The implementation shall use platform-specific monotonic clock + sources. If the platform clock is not monotonic, the implementation shall + clamp to the previous value. + ucas: [UCA-W-2] + hazards: [H-5] + + - id: CC-W-3 + controller: CTRL-WASI + constraint: > + Random number generation shall use a cryptographically secure source. + On platforms without hardware entropy, the implementation shall return + an error rather than falling back to a predictable PRNG. + ucas: [UCA-W-3] + hazards: [H-5] + + # ========================================================================= + # Blast Zone constraints + # ========================================================================= + - id: CC-BZ-1 + controller: CTRL-BLAST + constraint: > + Fault isolation shall be atomic: either the faulting component's state + is fully rolled back, or no shared runtime state is modified. The blast + zone shall use a pre-fault snapshot or copy-on-write strategy to prevent + partial state corruption. + ucas: [UCA-BZ-1] + hazards: [H-2, H-5] + + # ========================================================================= + # Allocation Manager constraints + # ========================================================================= + - id: CC-A-1 + controller: CTRL-ALLOC + constraint: > + In ASIL-D mode, all allocation paths shall be statically verified to + use only pre-allocated buffers. The safe_managed_alloc! macro shall + reject calls at compile time (or at runtime initialization) in ASIL-D + configuration. No code path shall bypass the macro. + ucas: [UCA-A-1] + hazards: [H-10] + + - id: CC-A-2 + controller: CTRL-ALLOC + constraint: > + BoundedVec::push, BoundedMap::insert, and all bounded collection + operations shall return Result::Err when at capacity. The caller + shall handle the error. No bounded collection operation shall + silently drop data or corrupt internal state. + ucas: [UCA-A-2] + hazards: [H-3, H-10] diff --git a/safety/stpa/cross-toolchain-consistency.yaml b/safety/stpa/cross-toolchain-consistency.yaml new file mode 100644 index 000000000..2bf265be3 --- /dev/null +++ b/safety/stpa/cross-toolchain-consistency.yaml @@ -0,0 +1,151 @@ +# Cross-Toolchain Canonical ABI Consistency Hazards +# +# System: Kiln — WebAssembly runtime for safety-critical systems +# +# Three independent implementations of the Component Model Canonical ABI +# must agree on layout computations. Disagreement causes silent data +# corruption at tool boundaries. +# +# This analysis mirrors and extends: +# pulseengine/meld/safety/stpa/cross-toolchain-consistency.yaml +# +# Spec baselines (shared across all tools): +# Core: WebAssembly Specification 3.0 (2025-12-03) +# Component Model: commit deb0b0a (2025-05-19) +# WASI: v0.2.3 (2024-12-17) + +cross-toolchain-hazards: + # ========================================================================= + # XH-1: Meld ↔ Kiln element size disagreement + # ========================================================================= + - id: XH-1 + 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. + affected-types: + - "list> with non-trivial padding" + - "record with mixed-size fields (u8, u32, u64)" + - "variant with differently-sized payloads" + impact: > + Silent data corruption: after the first list element, all subsequent + elements are read at wrong offsets. The corruption produces plausible + but incorrect values (no trap, no error). + mitigation: + primary: "Shared wit-bindgen composed-runner fixtures run through both tool paths" + secondary: "Shared Rocq formal spec for canonical_abi_element_size" + tertiary: "Minimal, auditable canonical ABI implementation in both tools" + kiln-implementation: kiln-component/src/canonical_abi/ + meld-implementation: meld-core/src/parser.rs::canonical_abi_element_size() + requirement: SR-11 + + # ========================================================================= + # XH-3: Synth ↔ Kiln element size disagreement + # ========================================================================= + - id: XH-3 + title: Canonical ABI element size disagreement (Synth ↔ Kiln) + tools: [synth, kiln] + 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. + affected-types: + - "Import arguments with composite types" + - "Return values written via retptr" + impact: > + Synth-compiled binary calls Kiln host function with misaligned + arguments. Kiln reads wrong values from the argument buffer. + mitigation: + primary: "End-to-end fixtures: compile with Synth, run on Kiln" + secondary: "Shared Rocq spec for element sizing" + kiln-implementation: kiln-component/src/canonical_abi/ + synth-implementation: synth-abi/src/layout.rs + requirement: SR-24 + + # ========================================================================= + # XH-4: String encoding disagreement + # ========================================================================= + - id: XH-4 + title: String encoding disagreement (Meld, Kiln, Synth) + tools: [meld, kiln, synth] + description: > + Each tool implements string transcoding (UTF-8, UTF-16, Latin-1) + independently. If encoding boundaries are handled differently + (surrogate pairs, BOM, NUL termination), strings corrupt at tool + boundaries. + affected-types: + - "string (all encodings)" + - "list as string representation" + impact: > + String data corrupted when crossing tool boundaries. Particularly + dangerous for non-ASCII content (multi-byte characters, emoji, CJK). + mitigation: + primary: "Shared wit-bindgen strings fixture with non-BMP characters" + secondary: "Shared Rocq spec for string transcoding" + kiln-implementation: kiln-component/src/canonical_abi/ + kiln-status: "UTF-8 only; no UTF-16 or Latin-1 tests" + requirement: SR-9 + + # ========================================================================= + # XH-5: Record field alignment disagreement + # ========================================================================= + - id: XH-5 + title: Record field alignment disagreement (Meld, Kiln, Synth) + tools: [meld, kiln, synth] + description: > + The canonical ABI spec's align_up function must be implemented + identically in all tools. Field offsets computed by Kiln's + canonical ABI must match Meld's field layout calculations. + affected-types: + - "record with mixed-size fields" + - "variant with alignment-sensitive payloads" + impact: > + Fields read at wrong offsets. First field correct, subsequent + fields shifted by alignment padding difference. + mitigation: + primary: "Shared wit-bindgen records fixture" + secondary: "Shared Rocq spec for align_up and field layout" + kiln-implementation: kiln-component/src/canonical_abi/ + requirement: SR-10 + +# ========================================================================= +# Fixture Coverage Matrix +# ========================================================================= +# Status of shared wit-bindgen fixtures across tool paths +# +# Fixtures: numbers, strings, lists, records, variants, options, +# many-arguments, flavorful, resources, results, lists-alias, +# strings-alias, strings-simple, fixed-length-lists + +fixture-coverage: + meld-core: + status: "All 14 passing" + fixtures: [numbers, strings, lists, records, variants, options, + many-arguments, flavorful, resources, results, + lists-alias, strings-alias, strings-simple, fixed-length-lists] + + meld-component: + status: "13 passing, 1 graceful degradation" + fixtures: [numbers, strings, lists, records, variants, options, + many-arguments, flavorful, results, + lists-alias, strings-alias, strings-simple] + degraded: [fixed-length-lists] + + kiln-runtime: + status: "TODO" + fixtures: [] + note: "Blocking gap — no shared fixtures run through Kiln yet" + + synth-aot: + status: "TODO" + fixtures: [] + note: "Pending Synth AOT compilation stabilization" + + synth-kiln-bridge: + status: "TODO" + fixtures: [] + note: "End-to-end: AOT compile → run on Kiln/Gale" diff --git a/safety/stpa/hazards.yaml b/safety/stpa/hazards.yaml new file mode 100644 index 000000000..b8a26d336 --- /dev/null +++ b/safety/stpa/hazards.yaml @@ -0,0 +1,148 @@ +# STPA Step 1b: System-Level Hazards +# +# System: Kiln — WebAssembly runtime for safety-critical systems +# +# Relation to BA RFC #46: Hazards H-4 through H-8 cover the runtime-side +# concerns that the RFC's "Host C API" sections leave as TODOs. These +# are the hazards that any runtime implementing the RFC must address. + +hazards: + - id: H-1 + title: Instruction execution produces wrong result + description: > + A core WebAssembly instruction (arithmetic, comparison, conversion, + memory, table, control flow) produces a result that diverges from + the WebAssembly Core Specification. This includes edge cases in + float-to-int conversion, saturating arithmetic, SIMD lane operations, + and atomic memory ordering. + losses: [L-1] + + - id: H-2 + title: Memory access exceeds linear memory bounds + description: > + A load, store, memory.grow, memory.copy, or memory.fill operation + accesses bytes outside the valid range of the target linear memory. + In multi-memory mode, instructions reference the wrong memory index. + The bounds check mechanism (software CMP, MPU, masking) has gaps. + losses: [L-1, L-2] + + - id: H-3 + title: Resource budget exceeded without detection + description: > + Fuel, memory, table, or stack limits are exceeded but the runtime + does not trap or report the violation. Execution continues in an + unbounded state. The bounded allocation system is bypassed. In + ASIL-D mode, the watchdog is not notified of budget exhaustion. + losses: [L-3, L-7] + + - id: H-4 + title: Canonical ABI lifting/lowering produces wrong values + description: > + The Component Model canonical ABI implementation in kiln-component + produces incorrect values during lift (core→component) or lower + (component→core) operations. String encoding/decoding is wrong, + list element sizing is incorrect, record field alignment is off, + or variant discriminant handling is incorrect. + losses: [L-4] + + - id: H-5 + title: Cross-component call misroutes or type-mismatches + description: > + A call from one component to another is dispatched to the wrong + function, or the caller and callee disagree on the function signature. + The linker resolves an import to the wrong export, or the + cross_component_calls module uses incorrect instance indices. + losses: [L-1, L-4] + + - id: H-6 + title: Resource handle lifecycle violation + description: > + A resource handle is used after being dropped, dropped twice, or + leaked (never dropped). The resource table in kiln-component's + resource_management module becomes inconsistent. Handle indices + wrap around and alias previous handles. + losses: [L-4, L-2] + + - id: H-7 + title: Async task scheduling violates ordering or fairness + description: > + The async executor in kiln-component starves a task, delivers + stream/future values out of order, or resumes a cancelled task. + The fuel-aware waker interferes with deterministic scheduling. + Task cancellation leaves dangling references. + losses: [L-4, L-6] + + - id: H-8 + title: WASI host function violates capability boundary + description: > + A WASI filesystem, socket, or clock operation bypasses the + WasiCapabilities security model. A component accesses a file path + it was not granted access to, or the capability check uses the + wrong component's capability set in a multi-component scenario. + losses: [L-5, L-2] + + - id: H-9 + title: CFI shadow stack desynchronization + description: > + The shadow stack and the real execution stack diverge: a call pushes + to one but not the other, or a return pops from one but not the other. + After desync, all subsequent return address validations produce false + positives or false negatives. The CFI violation policy (trap/log/ + continue) determines whether execution continues in a compromised state. + losses: [L-8] + + - id: H-10 + title: Safety-level allocation violation + description: > + In ASIL-D/static-allocation mode, the runtime performs dynamic + allocation. In bounded-allocation mode, a BoundedVec or BoundedMap + exceeds its capacity without error. The safe_managed_alloc! macro + fails to enforce per-crate budgets. An unsafe block in a + #[forbid(unsafe_code)] crate is missed by the audit. + losses: [L-3, L-7] + +# Sub-hazards for complex areas +sub-hazards: + # Refinements of H-4 (Canonical ABI) + - id: H-4.1 + parent: H-4 + title: String transcoding produces invalid encoding + description: > + 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. + + - id: H-4.2 + parent: H-4 + title: List element size computation disagrees with meld + description: > + Kiln's canonical_abi computes a different element size than Meld's + 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. + + - id: H-4.3 + parent: H-4 + title: Record field alignment padding differs from spec + description: > + Record fields are laid out with incorrect alignment, causing + loads/stores to read from wrong offsets within the record's + linear memory representation. + + # Refinements of H-5 (cross-component) + - id: H-5.1 + parent: H-5 + title: Blast zone containment fails to isolate fault + description: > + The blast_zone fault isolation mechanism fails to contain a trap + in one component, allowing it to corrupt the state of another + component or the runtime itself. + + # Refinements of H-9 (CFI) + - id: H-9.1 + parent: H-9 + title: Indirect call target validation uses wrong type index + description: > + call_indirect checks the function signature against the wrong + type index, either allowing a type-mismatched call or rejecting + a valid one. diff --git a/safety/stpa/loss-scenarios.yaml b/safety/stpa/loss-scenarios.yaml new file mode 100644 index 000000000..65f1a48cf --- /dev/null +++ b/safety/stpa/loss-scenarios.yaml @@ -0,0 +1,345 @@ +# STPA Step 4: Loss Scenarios +# +# System: Kiln — WebAssembly runtime for safety-critical systems +# +# Each scenario explains WHY a specific UCA might occur. Scenarios identify +# causal factors that can be addressed through design, testing, or verification. + +loss-scenarios: + # ========================================================================= + # Engine scenarios + # ========================================================================= + - id: LS-E-1 + title: Float-to-int saturating conversion uses wrong rounding + uca: UCA-E-1 + hazards: [H-1] + type: inadequate-control-algorithm + scenario: > + The engine's i32.trunc_sat_f64_s implementation rounds toward negative + infinity instead of toward zero for negative values near the boundary. + Input -2147483648.5 should produce -2147483648 but instead produces + -2147483649 (overflow). The saturating variant should clamp to INT_MIN + but the implementation wraps. + causal-factors: + - Rust's "as" cast uses different rounding than WebAssembly spec + - Saturating conversion boundary conditions not tested exhaustively + + - id: LS-E-2 + title: Fuel counter not checked on loop back-edge + uca: UCA-E-2 + hazards: [H-3] + type: inadequate-control-algorithm + scenario: > + The fuel check is performed at function entry and block entry but + not at loop back-edges (br to loop header). An infinite loop within + a single block body consumes unbounded fuel. The watchdog eventually + fires but the response time exceeds the safety budget. + causal-factors: + - Loop back-edges treated as branch instructions, not fuel checkpoints + - Fuel check only at block/function boundaries, not at all branches + + - id: LS-E-3 + title: Bounds check uses stale memory size after grow + uca: UCA-E-3 + hazards: [H-2] + type: inadequate-process-model + scenario: > + The engine caches the memory size at function entry for performance. + A memory.grow in the middle of the function updates the actual memory + but not the cached size. Subsequent loads/stores use the stale cached + size, allowing access to the newly-grown region to be incorrectly + rejected, or failing to reject access to the old boundary. + causal-factors: + - Performance optimization caches memory size + - memory.grow handler does not invalidate the cache + process-model-flaw: > + Engine assumes memory size is constant within a function body + + - id: LS-E-4 + title: Multi-byte opcode prefix consumed but suffix not validated + uca: UCA-E-4 + hazards: [H-1] + type: inadequate-control-algorithm + scenario: > + The 0xFC prefix is consumed, then the suffix byte is read but not + validated against the set of known 0xFC-prefixed opcodes. An unknown + suffix falls through to the default case which does nothing (no-op) + instead of trapping. The instruction appears to succeed silently. + causal-factors: + - Default match arm in opcode dispatch returns Ok(()) instead of Err + - Missing exhaustive opcode validation after prefix decode + + - id: LS-E-5 + title: Stack overflow check uses wrong limit in nested calls + uca: UCA-E-5 + hazards: [H-2, H-3] + type: inadequate-control-algorithm + scenario: > + Maximum call depth is configured as 1000 but the check compares + against frame count, not call depth. Tail-call-optimized functions + don't push frames but do push to the call stack, causing the counts + to diverge. Deep tail-call chains bypass the limit. + causal-factors: + - Frame count != call depth when tail calls are present + - Stack overflow check measures wrong quantity + + # ========================================================================= + # Decoder scenarios + # ========================================================================= + - id: LS-D-1 + title: Decoder accepts module with overlapping sections + uca: UCA-D-1 + hazards: [H-1, H-2] + type: inadequate-control-algorithm + scenario: > + The decoder processes sections sequentially but does not track whether + a section ID has already been seen. A module with two type sections is + accepted; the second silently overwrites the first. Functions referencing + types from the first section now have wrong signatures. + causal-factors: + - Section deduplication check missing + - Stream parser processes sections independently without global state + + - id: LS-D-2 + title: Resource limits not enforced during LEB128 decoding + uca: UCA-D-2 + hazards: [H-3] + type: inadequate-control-algorithm + scenario: > + A module declares 2^32 - 1 function types via a large LEB128 count. + The decoder begins allocating type structures before checking the + configured limit. The allocation exhausts the per-crate budget, + causing an OOM in a safety-critical system before the limit check fires. + causal-factors: + - Limit check occurs after allocation, not before + - LEB128 count is trusted for allocation sizing + + # ========================================================================= + # Component Model scenarios + # ========================================================================= + - id: LS-CM-1 + title: UTF-8 multi-byte character split across buffer boundary + uca: UCA-CM-1 + hazards: [H-4] + type: inadequate-control-algorithm + scenario: > + The canonical lift reads string data from linear memory in chunks. + A 4-byte UTF-8 character straddles two chunks. The first chunk is + decoded as if complete, producing an invalid character. The second + chunk starts mid-character, producing a decoding error. + causal-factors: + - Chunked reading does not handle multi-byte character boundaries + - String transcoding assumes aligned character boundaries + + - id: LS-CM-2 + title: Record alignment uses natural alignment instead of spec alignment + uca: UCA-CM-2 + hazards: [H-4] + type: inadequate-control-algorithm + scenario: > + The canonical ABI spec defines alignment for each type (e.g., i32 is + 4-aligned, i64 is 8-aligned). The implementation uses Rust's natural + alignment (which may differ due to platform conventions or #[repr(C)] + rules). For a record {u8, u32}, the spec says offset 4 for the u32 + but the implementation uses offset 1 (packed) or offset 8 (over-aligned). + causal-factors: + - Using Rust struct layout instead of canonical ABI layout + - align_up implementation differs from spec's definition + + - id: LS-CM-3 + title: List element size disagrees with Meld at fusion time + uca: UCA-CM-3 + hazards: [H-4] + type: inadequate-process-model + scenario: > + Meld computes list> element size as 8 bytes (align_up(5, 4)) + at fusion time. Kiln computes it as 5 bytes (raw sum without alignment). + When a meld-fused module runs on Kiln, the adapter writes 8-byte elements + but Kiln reads 5-byte elements. After the first element, all subsequent + elements are offset by 3 bytes, producing garbage data. + causal-factors: + - Kiln and Meld implement element size computation independently + - No shared test fixtures verify agreement + process-model-flaw: > + Kiln assumes its own element size is correct; does not verify against Meld + + - id: LS-CM-4 + title: Resource table generation counter overflow causes aliasing + uca: UCA-CM-4 + hazards: [H-6] + type: inadequate-control-algorithm + scenario: > + The resource table uses a 32-bit generation counter. After 2^32 + create/drop cycles, the counter wraps to 0. A handle with generation 0 + now matches a new allocation's generation. The old handle (which should + be invalid) passes the generation check and accesses the wrong resource. + causal-factors: + - Generation counter is 32-bit with no overflow detection + - Rapid create/drop cycles in long-running embedded systems + + - id: LS-CM-5 + title: Cross-component dispatch uses wrong instance after component reload + uca: UCA-CM-7 + hazards: [H-5] + type: inadequate-process-model + scenario: > + Component A is unloaded and Component C is loaded in its place. The + linker's resolution table still maps Component B's import to + instance index 0 (which was A, now C). Component B calls what it + thinks is Component A's export but reaches Component C's function + with a different signature. + causal-factors: + - Instance index reuse after unload + - Resolution table not invalidated on component unload + process-model-flaw: > + Linker assumes instance indices are stable across the component lifecycle + + - id: LS-CM-6 + title: Cross-toolchain element size disagreement causes silent corruption + uca: UCA-CM-8 + hazards: [H-4] + type: inadequate-process-model + scenario: > + A wit-bindgen composed-runner fixture using list passes + through Meld (element size = 16 due to alignment), is then executed on + Kiln which computes element size = 9 (sum without alignment). The list + roundtrip corrupts every element after the first. The corruption is + silent because the values are plausible (just wrong). + causal-factors: + - No shared fixture test suite run through Kiln + - Element size computation not derived from shared specification + - Corruption is silent (no trap, no error, just wrong values) + process-model-flaw: > + Each tool implements canonical ABI independently without cross-validation + + # ========================================================================= + # Linker scenarios + # ========================================================================= + - id: LS-L-1 + title: Import resolved to wrong export due to version-insensitive matching + uca: UCA-L-1 + hazards: [H-5] + type: inadequate-control-algorithm + scenario: > + Component A imports "wasi:http/handler@0.2.0". Two components export + "wasi:http/handler" — one at @0.2.0 and one at @0.3.0. The linker + strips version suffixes for matching and picks the first match, which + is @0.3.0. The signatures differ, causing a runtime trap or data + corruption on the first call. + causal-factors: + - Version suffix not included in import resolution matching + - First-match strategy without version comparison + + - id: LS-L-2 + title: Type compatibility check uses structural equality instead of nominal + uca: UCA-L-2 + hazards: [H-5] + type: inadequate-control-algorithm + scenario: > + Two components define structurally identical but nominally different + types: Component A's "Handle" and Component B's "Index" are both u32. + The linker considers them compatible because their structures match. + At runtime, Component B passes an Index where A expects a Handle, + and the semantic mismatch causes incorrect behavior. + causal-factors: + - Structural type comparison instead of nominal + - Component Model requires nominal type matching for resources + + # ========================================================================= + # CFI scenarios + # ========================================================================= + - id: LS-CFI-1 + title: Host-to-guest call skips shadow stack push + uca: UCA-CFI-1 + hazards: [H-9] + type: inadequate-control-algorithm + scenario: > + The host calls a guest export function directly through the engine API. + The call bypasses the normal instruction dispatch path and does not + trigger the shadow stack push. All subsequent returns within the guest + function are off-by-one on the shadow stack, producing false positives. + causal-factors: + - Host call entry point separate from instruction dispatch + - Shadow stack instrumentation only in instruction dispatch path + + - id: LS-CFI-2 + title: call_indirect uses table element type instead of instruction type + uca: UCA-CFI-2 + hazards: [H-9] + type: inadequate-control-algorithm + scenario: > + call_indirect should validate that the function at table[index] has the + type specified by the instruction's type_idx. Instead, the implementation + checks the function's own type against its own declaration (always true). + Any function in the table passes the check regardless of the instruction's + expected type. + causal-factors: + - Type validation compares function against itself, not against expectation + - The instruction's type_idx operand is ignored + + # ========================================================================= + # WASI scenarios + # ========================================================================= + - id: LS-W-1 + title: Capability check uses global state instead of per-component state + uca: UCA-W-1 + hazards: [H-8] + type: inadequate-process-model + scenario: > + The WASI dispatcher stores capabilities in a single WasiCapabilities + struct shared across all component instances. Component A is granted + filesystem access to /data. Component B should have no filesystem access. + Both components use the same dispatcher, so Component B inherits A's + capabilities. + causal-factors: + - Single WasiDispatcher instance shared across components + - Capability set not keyed by component instance ID + process-model-flaw: > + Dispatcher assumes single-component mode; multi-component requires + per-instance capability isolation + + - id: LS-W-2 + title: Platform clock wraps or adjusts backward + uca: UCA-W-2 + hazards: [H-5] + type: sensor-failure + scenario: > + On an embedded platform without RTC, the monotonic clock is implemented + as a 32-bit microsecond counter. After ~71 minutes, the counter wraps + to 0. The WASI implementation returns the raw counter value without + overflow detection. The application observes a time jump backward. + causal-factors: + - 32-bit counter overflow on long-running embedded systems + - No monotonicity enforcement in the WASI implementation + + # ========================================================================= + # Allocation scenarios + # ========================================================================= + - id: LS-A-1 + title: ASIL-D mode bypassed through optional dependency + uca: UCA-A-1 + hazards: [H-10] + type: inadequate-control-algorithm + scenario: > + A crate has an optional dependency that uses dynamic allocation. The + crate is compiled with the optional dependency enabled. The ASIL-D + check looks at the crate's own code but not transitive dependencies. + Dynamic allocation occurs in the dependency, violating ASIL-D. + causal-factors: + - ASIL-D check is crate-local, not transitive + - Feature flags can enable allocation in dependencies + + - id: LS-A-2 + title: BoundedVec capacity silently truncated to power of two + uca: UCA-A-2 + hazards: [H-3, H-10] + type: inadequate-control-algorithm + scenario: > + BoundedVec is initialized with capacity 100 but the underlying + allocator rounds to the next power of two (128). When the vector + reaches 100 elements, the capacity check passes (100 < 128). Elements + 101-128 are accepted, exceeding the intended budget. At 129, the + allocator fails instead of the bounded check. + causal-factors: + - Capacity check uses allocator capacity, not configured capacity + - Allocator over-provisions without notifying the bounded collection diff --git a/safety/stpa/losses.yaml b/safety/stpa/losses.yaml new file mode 100644 index 000000000..ab5881599 --- /dev/null +++ b/safety/stpa/losses.yaml @@ -0,0 +1,98 @@ +# STPA Step 1a: Losses +# +# System: Kiln — WebAssembly runtime for safety-critical systems +# System boundary: Kiln accepts WebAssembly core modules and components, +# instantiates them with WASI and host functions, and executes them on +# gale (RTOS kernel) or std platforms. The system boundary includes +# decoding, validation, instantiation, execution, component model +# operations, and WASI host implementations. It excludes upstream +# build tools (meld, loom, synth), the gale kernel itself, and hardware. +# +# Stakeholders: +# - Developers building safety-critical systems with WebAssembly +# - End-users of systems whose behavior depends on correct execution +# - Certification authorities (ISO 26262, DO-178C, IEC 61508) +# - PulseEngine toolchain (Meld, Loom, Synth, Sigil, Gale) +# +# Relation to BA RFC #46: Kiln implements the runtime-side functionality +# that the RFC splits across "Host C API for Lowered Components" and +# "Host C API for Embedder Bindings". Where the RFC proposes a +# runtime-agnostic C API, Kiln provides a concrete, safety-qualified +# Rust implementation targeting embedded/safety-critical platforms. + +losses: + - id: L-1 + title: Loss of execution correctness + description: > + The runtime executes WebAssembly instructions incorrectly. Functions + return wrong values, control flow diverges from spec, or traps occur + where none should (or vice versa). This includes incorrect numeric + operations, wrong branching, incorrect table/memory access semantics, + and incorrect component model canonical ABI operations. + stakeholders: [developers, end-users, certification-authorities] + + - id: L-2 + title: Loss of memory isolation + description: > + One component or module reads or writes memory belonging to another + component, the host, or the runtime itself. Bounds checks fail to + prevent out-of-bounds access, multi-memory indexing is incorrect, or + the memory protection mechanism (MPU, software bounds) has gaps. + stakeholders: [developers, end-users, certification-authorities] + + - id: L-3 + title: Loss of resource containment + description: > + The runtime fails to bound execution: unbounded fuel consumption, + unbounded memory growth, unbounded table growth, stack overflow, + or unbounded allocation within the runtime's own data structures. + In embedded/safety-critical systems, this causes watchdog timeout, + memory exhaustion, or interference with other tasks. + stakeholders: [developers, end-users, certification-authorities] + + - id: L-4 + title: Loss of component model fidelity + description: > + The Component Model implementation diverges from the spec: canonical + lifting/lowering produces wrong values, resource handle lifecycle is + incorrect, cross-component calls misroute, type checking at component + boundaries is wrong, or async task scheduling violates ordering + guarantees. + stakeholders: [developers, end-users] + + - id: L-5 + title: Loss of WASI contract + description: > + WASI host implementations violate the WASI specification: file I/O + returns wrong data, clock reads are non-monotonic, random number + generation is predictable, or capability checks are bypassed. In + safety-critical systems, WASI violations can cause silent data + corruption in the application. + stakeholders: [developers, end-users] + + - id: L-6 + title: Loss of deterministic behavior + description: > + Identical inputs produce different execution results across runs, + platforms, or configurations. Sources include HashMap iteration order, + non-deterministic scheduling of async tasks, platform-dependent float + semantics, or timing-dependent behavior in the execution engine. + stakeholders: [developers, certification-authorities] + + - id: L-7 + title: Loss of safety-level guarantees + description: > + The runtime claims a safety integrity level (ASIL-D, SIL-4, DAL-A) + but the actual implementation does not meet the standard's requirements. + Unbounded allocation in ASIL-D mode, missing error detection codes, + insufficient diagnostic coverage, or unsafe Rust in forbidden contexts. + stakeholders: [certification-authorities, developers] + + - id: L-8 + title: Loss of control flow integrity + description: > + The CFI mechanism (shadow stack, indirect call validation) fails to + detect or prevent control flow hijacking. An indirect call reaches a + wrong function, a return address is corrupted, or the shadow stack + is desynchronized from the real stack. + stakeholders: [developers, end-users, certification-authorities] diff --git a/safety/stpa/rfc46-comparative-analysis.md b/safety/stpa/rfc46-comparative-analysis.md new file mode 100644 index 000000000..9c7c943cd --- /dev/null +++ b/safety/stpa/rfc46-comparative-analysis.md @@ -0,0 +1,127 @@ +# BA RFC #46 Comparative Analysis + +## Overview + +Bytecode Alliance RFC #46 ("Propose tools and APIs for lowering components +to core modules", Joel Dice, 2026-03-09) proposes a four-part architecture +for running components on any compatible WebAssembly runtime. This analysis +maps the RFC's architecture to Kiln's implementation and identifies gaps +and hazards. + +## Architecture Mapping + +| RFC Component | Purpose | PulseEngine Equivalent | +|---------------|---------|----------------------| +| `lower-component` | Fuse components into core module | **Meld** | +| Host C API for Lowered Components | Fiber management, stack traces | **Gale task primitives** | +| `host-wit-bindgen` | Generate host bindings for target language | **Kiln WASI dispatcher + Synth stubs** | +| Host C API for Embedder Bindings | Runtime-agnostic module management | **Kiln engine API** | + +## Key Architectural Differences + +### 1. Embedded Runtime vs Clean Separation + +| Aspect | RFC | PulseEngine | +|--------|-----|-------------| +| CM runtime code | Embedded in lowered module (Rust-compiled) | **Not embedded** — clean separation | +| Table management | Guest-side (in sandbox) | **Runtime-side** (kiln-component) | +| Stream/future I/O | Guest-side | **Runtime-side** (kiln-component async) | +| Trust boundary | Smaller (more in sandbox) | **Smaller host API** (less runtime code) | +| Memory overhead | 2+ linear memories per component | **1 per component** (standard) | + +The RFC embeds a Rust-compiled CM runtime in every lowered module. This +puts table management and stream I/O in the sandbox (good for security) +but increases code size and memory usage. PulseEngine keeps these in the +runtime, trading a larger runtime for smaller module sizes. + +### 2. Fiber vs Stackless Execution + +| Aspect | RFC | PulseEngine | +|--------|-----|-------------| +| Async model | Fibers (host-provided intrinsics) | **Stackless** (fuel-aware waker) | +| Stack switching | Planned (Wasm stack switching proposal) | **Not required** (interpreter-based) | +| Host intrinsics | create/suspend/resume fiber | **None** (runtime manages async) | + +The RFC requires the host to provide fiber management intrinsics. Kiln's +stackless interpreter naturally supports async without fibers — the +execution state is a data structure that can be suspended and resumed. + +### 3. Multiply-Instantiated Modules + +Both the RFC and Meld identify this as an unsolved problem. The RFC proposes +three options (reject, duplicate, multi-module output). Meld's +weighted-gap-analysis identifies this as GAP-P2-1 (CRITICAL). + +Kiln's position: If the component arrives pre-fused (via Meld), this is +Meld's problem. If the component is loaded directly, Kiln must handle it. +Current status: Kiln supports single-instance-per-module only. + +### 4. Type Checking Boundary + +The RFC asks: who does type checking — `lower-component` or `host-wit-bindgen`? + +PulseEngine's answer: +- **Meld** validates at fusion time (build-time guarantee) +- **Kiln decoder** validates modules at load time +- **Kiln linker** validates import/export type compatibility +- The **dispatcher** does NOT do type checking — it trusts the linker + +## Hazards Introduced by RFC Scope (Not in PulseEngine) + +These hazards exist in the RFC's architecture but not in PulseEngine's +current implementation, because PulseEngine avoids the patterns that +create them: + +| Hazard | Title | Why PulseEngine avoids it | +|--------|-------|--------------------------| +| RL-1 | Loss of async correctness | No embedded CM runtime | +| RL-2 | Loss of fiber isolation | No fiber intrinsics needed | +| RL-3 | Loss of host/guest type safety | No host-wit-bindgen C API | +| RL-4 | Loss of portability | No Host C API divergence | +| RL-5 | Loss of code size efficiency | No function duplication in module | + +## Gaps in PulseEngine vs RFC + +| Gap | PulseEngine Status | Mitigation | +|-----|-------------------|------------| +| MG-1: Async CM | P2-only; no P3 async | Wait for stack-switching ecosystem | +| MG-2: Resource types | Partial (kiln-component) | Track with SR-12, SR-13 | +| MG-3: Multiply-instantiated modules | Not supported | Track with Meld GAP-P2-1 | +| MG-4: Host bindings generation | Manual (dispatcher) | Dispatcher redesign in progress | + +## Gaps in RFC vs PulseEngine + +| Gap | RFC Status | PulseEngine Advantage | +|-----|-----------|----------------------| +| RG-1: Attestation/provenance | Not mentioned | Sigil integration | +| RG-2: Build reproducibility | Not mentioned | Meld deterministic output | +| RG-3: Formal verification | Not mentioned | 286 Rocq proofs (Meld) | +| RG-4: Certification evidence | Not mentioned | Full STPA + traceability | +| RG-5: Cross-toolchain consistency | Not mentioned | XH-1 through XH-5 tracked | +| RG-6: Safety-level guarantees | Not mentioned | ASIL-D through QM support | + +## Implications for Kiln Dispatcher Redesign + +The RFC validates the architectural split between "lowering" (Meld) and +"host bindings" (Kiln dispatcher). Key takeaways for the dispatcher: + +1. **The dispatcher IS the "host-wit-bindgen" equivalent** — it generates + the runtime-side bindings between lowered modules and WASI host functions + +2. **Canonical ABI correctness is the primary safety concern** — both the + RFC and STPA analysis identify this as the highest-risk boundary + +3. **The dispatcher should NOT embed runtime code** — unlike the RFC's + approach of compiling CM runtime into the module, Kiln keeps this + in the runtime. This means the dispatcher must implement lift/lower + correctly, not delegate to embedded guest code. + +4. **Per-component capability isolation** is unique to PulseEngine's + safety requirements (SR-17). The RFC does not address this because + it targets general-purpose runtimes, not safety-critical systems. + +## References + +- [BA RFC #46 PR](https://github.com/bytecodealliance/rfcs/pull/46) +- [Meld RFC #46 Analysis](https://github.com/pulseengine/meld/safety/stpa/rfc46-comparative-analysis.md) +- [Meld Cross-Toolchain Consistency](https://github.com/pulseengine/meld/safety/stpa/cross-toolchain-consistency.yaml) diff --git a/safety/stpa/system-constraints.yaml b/safety/stpa/system-constraints.yaml new file mode 100644 index 000000000..be0d9d487 --- /dev/null +++ b/safety/stpa/system-constraints.yaml @@ -0,0 +1,124 @@ +# STPA Step 1c: System-Level Constraints +# +# System: Kiln — WebAssembly runtime for safety-critical systems +# +# Each constraint is the inversion of a hazard: it specifies the condition +# that must be enforced to prevent the hazard. +# +# Spec baselines: +# Core: WebAssembly Specification 3.0 (2025-12-03) +# Component Model: commit deb0b0a (2025-05-19) +# WASI: v0.2.3 (2024-12-17) + +system-constraints: + - id: SC-1 + title: Instruction execution must match WebAssembly spec + description: > + Every core WebAssembly instruction shall produce a result identical + to the reference interpreter for all inputs, including edge cases + (NaN propagation, saturating conversion, division by zero rounding, + SIMD lane operations, atomic ordering). + hazards: [H-1] + spec-baseline: "WebAssembly Core Specification 3.0" + + - id: SC-2 + title: Memory access must be within linear memory bounds + description: > + All load, store, memory.grow, memory.copy, and memory.fill operations + shall be bounds-checked against the current memory size. In multi-memory + mode, the memory index shall be validated against the module's declared + memories. No access shall read or write bytes outside the target memory. + hazards: [H-2] + spec-baseline: "WebAssembly Core Specification 3.0, Section 4.4.7" + + - id: SC-3 + title: Resource budgets must be enforced with detection + description: > + Fuel, memory, table, and stack limits shall be checked before every + operation that could exceed them. When a limit is reached, the runtime + shall trap or return an error immediately. In ASIL-D mode, budget + violations shall notify the watchdog. No execution shall continue + in an unbounded state. + hazards: [H-3] + spec-baseline: "ISO 26262, kiln-foundation memory budget system" + + - id: SC-4 + title: Canonical ABI lifting/lowering must produce correct values + description: > + The canonical ABI implementation shall produce identical values to the + Component Model spec's canonical definitions for all type families: + integers, floats, strings (all encodings), lists, records, variants, + options, results, flags, enums, and resource handles. Element sizing, + field alignment, and padding must match the spec exactly. + hazards: [H-4] + spec-baseline: "Component Model commit deb0b0a, Canonical ABI" + + - id: SC-5 + title: Cross-component calls must route to correct function with matching type + description: > + The linker shall resolve every import to the correct export. The resolved + function's signature shall be type-compatible with the import declaration. + Instance indices used in cross-component dispatch shall correctly identify + the target component. No call shall be dispatched to the wrong function. + hazards: [H-5] + spec-baseline: "Component Model commit deb0b0a, Instantiation" + + - id: SC-6 + title: Resource handle lifecycle must be correct + description: > + Resource handles shall not alias (same index, different resource), + shall not be used after drop, and shall not be dropped twice. + The resource table shall maintain consistent state across all + create/transfer/drop operations. + hazards: [H-6] + spec-baseline: "Component Model commit deb0b0a, Resources" + + - id: SC-7 + title: Async task scheduling must preserve ordering and fairness + description: > + No async task shall be starved. Stream and future values shall be + delivered in order. Cancelled tasks shall not be resumed. The + fuel-aware waker shall not interfere with deterministic scheduling. + hazards: [H-7] + spec-baseline: "Component Model commit deb0b0a, Async" + + - id: SC-8 + title: WASI operations must respect capability boundaries + description: > + Every WASI filesystem, socket, and clock operation shall check + the calling component's WasiCapabilities before execution. No + component shall access resources (paths, sockets, clocks) outside + its granted capability set. In multi-component scenarios, each + component's capability set shall be isolated. + hazards: [H-8] + spec-baseline: "WASI v0.2.3" + + - id: SC-9 + title: CFI shadow stack must remain synchronized with execution stack + description: > + Every call instruction shall push to the shadow stack. Every return + shall validate against the shadow stack. No execution path (including + host-to-guest calls, cross-component calls, and exception handling) + shall skip a push or pop operation. + hazards: [H-9] + + - id: SC-10 + title: Safety-level allocation constraints must be enforced + description: > + In ASIL-D/static-allocation mode, no dynamic allocation shall occur + after initialization. In bounded-allocation mode, all BoundedVec and + BoundedMap operations shall return errors at capacity rather than + silently failing. The safe_managed_alloc! macro shall enforce per-crate + budgets. No code path shall bypass the allocation manager. + hazards: [H-10] + spec-baseline: "ISO 26262, kiln-foundation allocation system" + + - id: SC-11 + title: Canonical ABI computation must be consistent across toolchain + description: > + Kiln's canonical ABI element size, field alignment, and string encoding + implementations shall produce identical results to Meld's fusion-time + computations and Synth's AOT compilation for every type. This shall be + verified by running shared wit-bindgen test fixtures through all tool paths. + hazards: [H-4] + spec-baseline: "Cross-toolchain consistency (XH-1 through XH-5)" diff --git a/safety/stpa/ucas.yaml b/safety/stpa/ucas.yaml new file mode 100644 index 000000000..ff4f28204 --- /dev/null +++ b/safety/stpa/ucas.yaml @@ -0,0 +1,277 @@ +# STPA Step 3: Unsafe Control Actions +# +# System: Kiln — WebAssembly runtime for safety-critical systems +# +# Format: UCAs grouped by controller, categorized by type: +# not-providing: Action needed but not taken +# providing: Action taken when it shouldn't be +# too-early-too-late: Action timing incorrect +# stopped-too-soon: Action duration too short +# +# Relation to BA RFC #46: Kiln implements the runtime-side functionality +# that the RFC splits across "Host C API for Lowered Components" and +# "Host C API for Embedder Bindings". These UCAs cover the hazards +# that any runtime implementing the RFC must address. + +engine-ucas: + control-action: "Execute WebAssembly instructions" + controller: CTRL-ENGINE + + providing: + - id: UCA-E-1 + description: > + Engine executes arithmetic instruction with incorrect semantics for + edge cases (NaN propagation, saturating conversion, division by zero + rounding). + context: "Numeric instruction with boundary input values" + hazards: [H-1] + + - id: UCA-E-4 + description: > + Engine dispatches to wrong instruction handler due to opcode decoding + error, executing a different instruction than what is encoded. + context: "Multi-byte opcode (SIMD, atomics) decoding" + hazards: [H-1] + + - id: UCA-E-6 + description: > + Engine uses wrong memory index in multi-memory mode, reading from or + writing to the wrong component's linear memory. + context: "Multi-memory module with memory.copy between memories" + hazards: [H-2] + + not-providing: + - id: UCA-E-2 + description: > + Engine does not check fuel budget before executing instruction, + allowing unbounded execution past the configured fuel limit. + context: "Fuel metering enabled, long-running loop" + hazards: [H-3] + + - id: UCA-E-3 + description: > + Engine performs memory access with incorrect bounds check: off-by-one + in the comparison, or check uses wrong memory size after memory.grow. + context: "Memory load/store near page boundary after grow" + hazards: [H-2] + + - id: UCA-E-5 + description: > + Engine does not trap on stack overflow, allowing call stack to exceed + maximum depth and corrupt adjacent memory. + context: "Deeply recursive function call chain" + hazards: [H-2, H-3] + +decoder-ucas: + control-action: "Parse and validate WebAssembly binary" + controller: CTRL-DECODER + + not-providing: + - id: UCA-D-1 + description: > + Decoder accepts a malformed module that should be rejected, allowing + execution of invalid bytecode that causes undefined behavior in the + engine. + context: "Fuzzer-generated or adversarial module input" + hazards: [H-1, H-2] + + - id: UCA-D-2 + description: > + Decoder does not enforce resource limits (max functions, max memories, + max types), allowing a module to exhaust the runtime's allocation budget + during parsing. + context: "Module with millions of type definitions" + hazards: [H-3] + + providing: + - id: UCA-D-3 + description: > + Decoder misidentifies a component as a core module (or vice versa), + causing the wrong instantiation path to be taken. + context: "Component binary with version byte differences" + hazards: [H-4, H-5] + +component-model-ucas: + control-action: "Lift, lower, and dispatch Component Model operations" + controller: CTRL-CM + + providing: + - id: UCA-CM-1 + description: > + Canonical lift produces wrong string value: UTF-8 to UTF-16 conversion + miscounts code units or produces invalid sequences. + context: "String containing multi-byte UTF-8 characters" + hazards: [H-4] + + - id: UCA-CM-2 + description: > + Canonical lower computes wrong byte offset for record field due to + incorrect alignment calculation. + context: "Record with mixed-size fields (u8, u32, u64)" + hazards: [H-4] + + - id: UCA-CM-3 + description: > + Canonical lift/lower for list type uses wrong element size, reading + past the end of the list buffer or leaving uninitialized gaps. + context: "list> where element_size != sum of field sizes" + hazards: [H-4] + + - id: UCA-CM-4 + description: > + Resource handle creation returns a handle index that aliases a + previously-dropped but not-yet-reclaimed handle. + context: "Rapid create/drop cycle filling resource table" + hazards: [H-6] + + - id: UCA-CM-5 + description: > + Resource drop is called twice for the same handle, corrupting the + 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] + + - id: UCA-CM-7 + description: > + Cross-component call dispatches to wrong function due to incorrect + instance index lookup in the linker's resolution table. + context: "Multiple component instances with same export name" + hazards: [H-5] + + - id: UCA-CM-8 + description: > + Canonical ABI element size computation disagrees with Meld's + fusion-time computation for the same type, causing meld-fused + modules to corrupt data at the kiln lift/lower boundary. + context: "Running a meld-fused component through kiln with P2 wrapper" + hazards: [H-4] + rationale: > + This is a cross-tool consistency hazard. Meld computes CopyLayout + at fusion time; Kiln computes canonical ABI layout at runtime. If + they disagree, the data is silently corrupted. This must be tested + with shared test fixtures (wit-bindgen composed-runner components). + + too-early-too-late: + - id: UCA-CM-6 + description: > + Async task is resumed after cancellation, executing with stale or + freed state. + context: "Task cancellation racing with stream data arrival" + hazards: [H-7] + +linker-ucas: + control-action: "Resolve imports to exports across component instances" + controller: CTRL-LINKER + + providing: + - id: UCA-L-1 + description: > + Linker resolves import to wrong export due to name collision between + component instances. + context: "Two components exporting same interface name" + hazards: [H-5] + + not-providing: + - id: UCA-L-2 + description: > + Linker does not verify type compatibility between import and export, + allowing a function with signature (i32)->i32 to be linked to a + function with signature (i32,i32)->i32. + context: "Component upgrade changes function signature" + hazards: [H-5] + + too-early-too-late: + - id: UCA-L-3 + description: > + Linker instantiates module before its dependencies are ready, + causing the start function to observe uninitialized state. + context: "Circular dependency between component instances" + hazards: [H-5] + +cfi-ucas: + control-action: "Validate control flow integrity" + controller: CTRL-CFI + + not-providing: + - id: UCA-CFI-1 + description: > + Shadow stack push is skipped for a call instruction, causing all + subsequent return validations to be off-by-one. + context: "Host-to-guest call that bypasses CFI instrumentation" + hazards: [H-9] + + providing: + - id: UCA-CFI-2 + description: > + Indirect call target validation uses wrong type index (e.g., the + table element's type vs the call_indirect's type annotation), allowing + a type-mismatched indirect call. + context: "call_indirect with subtyping" + hazards: [H-9] + + - id: UCA-CFI-3 + description: > + CFI violation policy is set to "continue" in production, allowing + execution to proceed after a detected control flow violation. + context: "Deployment misconfiguration" + hazards: [H-8, H-9] + +wasi-ucas: + control-action: "Execute WASI host function with capability check" + controller: CTRL-WASI + + providing: + - id: UCA-W-1 + description: > + WASI filesystem operation uses wrong component's capability set, + granting one component access to another component's allowed paths. + context: "Multi-component instance with different filesystem grants" + hazards: [H-8] + + - id: UCA-W-2 + description: > + WASI clock read returns non-monotonic value, causing application + logic that depends on monotonic time to compute negative durations + or infinite loops. + context: "Platform clock with NTP adjustment" + hazards: [H-5] + + - id: UCA-W-3 + description: > + WASI random returns predictable sequence (e.g., seeded PRNG in + no_std mode without hardware RNG), compromising application + cryptographic operations. + context: "Embedded platform without hardware entropy source" + hazards: [H-5] + +blast-zone-ucas: + control-action: "Isolate component fault within containment zone" + controller: CTRL-BLAST + + not-providing: + - id: UCA-BZ-1 + description: > + Blast zone does not contain fault: a trap in one component corrupts + shared runtime state (e.g., the linker's instance table) before the + blast zone handler activates. + context: "Trap during cross-component call with partially-written state" + hazards: [H-2, H-5] + +allocation-ucas: + control-action: "Manage memory allocation within safety-level budgets" + controller: CTRL-ALLOC + + not-providing: + - id: UCA-A-1 + description: > + Allocation succeeds in ASIL-D/static-allocation mode when it should + be rejected, violating the no-dynamic-allocation guarantee. + context: "Runtime code path that bypasses safe_managed_alloc! macro" + hazards: [H-10] + + - id: UCA-A-2 + description: > + BoundedVec exceeds capacity without returning error, silently + dropping the inserted element or corrupting adjacent memory. + context: "BoundedVec at capacity with push operation" + hazards: [H-3, H-10]