diff --git a/safety/stpa/analysis.yaml b/safety/stpa/analysis.yaml index a7267ef..c864b1b 100644 --- a/safety/stpa/analysis.yaml +++ b/safety/stpa/analysis.yaml @@ -53,6 +53,9 @@ artifacts: - id: H-1 type: hazard + links: + - type: leads-to-loss + target: L-1 title: Analysis produces false negative description: > Spar's analysis passes fail to detect a genuine architectural @@ -63,6 +66,11 @@ artifacts: - id: H-2 type: hazard + links: + - type: leads-to-loss + target: L-2 + - type: leads-to-loss + target: L-3 title: Analysis produces false positive description: > Spar reports a defect that does not actually exist in the model, @@ -72,6 +80,11 @@ artifacts: - id: H-3 type: hazard + links: + - type: leads-to-loss + target: L-1 + - type: leads-to-loss + target: L-4 title: Instance model does not match declarative model description: > The instantiated system tree diverges from the declared AADL @@ -82,6 +95,9 @@ artifacts: - id: H-4 type: hazard + links: + - type: leads-to-loss + target: L-4 title: Serialized output does not match internal model description: > JSON, SVG, or text output represents a different model than @@ -91,6 +107,11 @@ artifacts: - id: H-5 type: hazard + links: + - type: leads-to-loss + target: L-1 + - type: leads-to-loss + target: L-3 title: Parser silently drops valid AADL constructs description: > The parser accepts input without error but silently omits valid @@ -101,6 +122,9 @@ artifacts: - id: H-6 type: hazard + links: + - type: leads-to-loss + target: L-1 title: Property values incorrectly evaluated description: > Timing, memory, or deployment properties are parsed or evaluated @@ -111,6 +135,11 @@ artifacts: - id: H-7 type: hazard + links: + - type: leads-to-loss + target: L-1 + - type: leads-to-loss + target: L-4 title: SysML v2 lowering produces semantically incorrect AADL description: > The SysML v2 to AADL lowering transformation produces AADL @@ -124,6 +153,11 @@ artifacts: - id: H-8 type: hazard + links: + - type: leads-to-loss + target: L-1 + - type: leads-to-loss + target: L-3 title: Verification pipeline provides false assurance description: > The Bazel-based verification pipeline (Verus, Lean4, WASM component @@ -139,6 +173,9 @@ artifacts: - id: SC-1 type: system-constraint + links: + - type: prevents + target: H-1 title: No false negatives on safety analyses description: > Spar must detect all genuine architectural defects for which it @@ -148,6 +185,9 @@ artifacts: - id: SC-2 type: system-constraint + links: + - type: prevents + target: H-2 title: Minimize false positives description: > Spar should not report defects that do not exist. When uncertain, @@ -157,6 +197,9 @@ artifacts: - id: SC-3 type: system-constraint + links: + - type: prevents + target: H-3 title: Instance model fidelity description: > The instance model must faithfully represent the declared AADL @@ -166,6 +209,9 @@ artifacts: - id: SC-4 type: system-constraint + links: + - type: prevents + target: H-4 title: Output fidelity description: > All serialized outputs (JSON, SVG, text) must accurately represent @@ -175,6 +221,9 @@ artifacts: - id: SC-5 type: system-constraint + links: + - type: prevents + target: H-5 title: Parser completeness description: > The parser must produce CST nodes for all valid AADL v2.2 constructs. @@ -184,6 +233,9 @@ artifacts: - id: SC-6 type: system-constraint + links: + - type: prevents + target: H-6 title: Property evaluation correctness description: > Property values must be evaluated with correct units, arithmetic, @@ -193,6 +245,9 @@ artifacts: - id: SC-7 type: system-constraint + links: + - type: prevents + target: H-7 title: SysML v2 lowering semantic fidelity description: > The SysML v2 to AADL lowering must faithfully preserve the design @@ -204,6 +259,9 @@ artifacts: - id: SC-8 type: system-constraint + links: + - type: prevents + target: H-8 title: Verification pipeline integrity description: > The Bazel verification pipeline must fail loudly when verification @@ -338,6 +396,11 @@ artifacts: - id: CA-PARSE type: control-action + links: + - type: issued-by + target: CTRL-PARSER + - type: acts-on + target: CP-MODEL title: Parse AADL source action: Transform source text into concrete syntax tree source: CTRL-PARSER @@ -345,6 +408,11 @@ artifacts: - id: CA-LOWER type: control-action + links: + - type: issued-by + target: CTRL-MODEL + - type: acts-on + target: CP-MODEL title: Lower CST to ItemTree action: Convert syntax tree nodes to typed HIR items source: CTRL-MODEL @@ -352,6 +420,11 @@ artifacts: - id: CA-INSTANTIATE type: control-action + links: + - type: issued-by + target: CTRL-INSTANCE + - type: acts-on + target: CP-MODEL title: Instantiate system action: Recursively expand root implementation into instance tree source: CTRL-INSTANCE @@ -359,6 +432,11 @@ artifacts: - id: CA-ANALYZE type: control-action + links: + - type: issued-by + target: CTRL-ANALYSIS + - type: acts-on + target: CP-DIAGNOSTICS title: Run analysis passes action: Execute registered analyses against instance model source: CTRL-ANALYSIS @@ -366,6 +444,11 @@ artifacts: - id: CA-REPORT type: control-action + links: + - type: issued-by + target: CTRL-OUTPUT + - type: acts-on + target: CP-DECISIONS title: Report results action: Format and output analysis diagnostics source: CTRL-OUTPUT @@ -373,6 +456,11 @@ artifacts: - id: CA-REVIEW type: control-action + links: + - type: issued-by + target: CTRL-REVIEWER + - type: acts-on + target: CP-DECISIONS title: Review and approve architecture action: Evaluate analysis output and decide on architecture approval source: CTRL-REVIEWER @@ -380,6 +468,11 @@ artifacts: - id: CA-SYSML2-LOWER type: control-action + links: + - type: issued-by + target: CTRL-SYSML2 + - type: acts-on + target: CP-MODEL title: Lower SysML v2 to AADL action: Transform SysML v2 CST into AADL ItemTree using SEI mapping rules source: CTRL-SYSML2 @@ -387,6 +480,11 @@ artifacts: - id: CA-CODEGEN type: control-action + links: + - type: issued-by + target: CTRL-CODEGEN + - type: acts-on + target: CP-DECISIONS title: Generate code and verification pipeline action: > Generate Rust crate skeletons, WIT interfaces, and Bazel BUILD files @@ -402,6 +500,11 @@ artifacts: - id: UCA-1 type: uca + links: + - type: issued-by + target: CTRL-PARSER + - type: leads-to-hazard + target: H-5 title: Parser silently drops construct uca-type: not-providing context: > @@ -416,6 +519,13 @@ artifacts: - id: UCA-2 type: uca + links: + - type: issued-by + target: CTRL-PARSER + - type: leads-to-hazard + target: H-1 + - type: leads-to-hazard + target: H-5 title: Parser accepts invalid AADL without error uca-type: providing context: > @@ -431,6 +541,13 @@ artifacts: - id: UCA-3 type: uca + links: + - type: issued-by + target: CTRL-MODEL + - type: leads-to-hazard + target: H-1 + - type: leads-to-hazard + target: H-3 title: Lowering omits CST node uca-type: not-providing context: > @@ -445,6 +562,11 @@ artifacts: - id: UCA-4 type: uca + links: + - type: issued-by + target: CTRL-MODEL + - type: leads-to-hazard + target: H-6 title: Lowering assigns wrong property value uca-type: providing context: > @@ -458,6 +580,11 @@ artifacts: - id: UCA-5 type: uca + links: + - type: issued-by + target: CTRL-MODEL + - type: leads-to-hazard + target: H-3 title: Name resolution returns wrong classifier uca-type: providing context: > @@ -473,6 +600,11 @@ artifacts: - id: UCA-6 type: uca + links: + - type: issued-by + target: CTRL-INSTANCE + - type: leads-to-hazard + target: H-3 title: Instance expansion misses subcomponent uca-type: not-providing context: > @@ -487,6 +619,13 @@ artifacts: - id: UCA-7 type: uca + links: + - type: issued-by + target: CTRL-INSTANCE + - type: leads-to-hazard + target: H-3 + - type: leads-to-hazard + target: H-1 title: Array expansion produces wrong count uca-type: providing context: > @@ -500,6 +639,13 @@ artifacts: - id: UCA-8 type: uca + links: + - type: issued-by + target: CTRL-INSTANCE + - type: leads-to-hazard + target: H-3 + - type: leads-to-hazard + target: H-1 title: Connection tracing produces wrong endpoint uca-type: providing context: > @@ -514,6 +660,11 @@ artifacts: - id: UCA-9 type: uca + links: + - type: issued-by + target: CTRL-INSTANCE + - type: leads-to-hazard + target: H-3 title: Instance builder enters infinite recursion uca-type: stopped-too-soon context: > @@ -530,6 +681,11 @@ artifacts: - id: UCA-10 type: uca + links: + - type: issued-by + target: CTRL-ANALYSIS + - type: leads-to-hazard + target: H-1 title: Analysis not registered uca-type: not-providing context: > @@ -544,6 +700,13 @@ artifacts: - id: UCA-11 type: uca + links: + - type: issued-by + target: CTRL-ANALYSIS + - type: leads-to-hazard + target: H-1 + - type: leads-to-hazard + target: H-6 title: Analysis uses wrong property value uca-type: providing context: > @@ -557,6 +720,11 @@ artifacts: - id: UCA-12 type: uca + links: + - type: issued-by + target: CTRL-ANALYSIS + - type: leads-to-hazard + target: H-1 title: Analysis emits wrong severity uca-type: providing context: > @@ -570,6 +738,11 @@ artifacts: - id: UCA-13 type: uca + links: + - type: issued-by + target: CTRL-ANALYSIS + - type: leads-to-hazard + target: H-2 title: Analysis produces false positive uca-type: providing context: > @@ -585,6 +758,11 @@ artifacts: - id: UCA-14 type: uca + links: + - type: issued-by + target: CTRL-OUTPUT + - type: leads-to-hazard + target: H-4 title: JSON serialization drops field uca-type: not-providing context: > @@ -599,6 +777,11 @@ artifacts: - id: UCA-15 type: uca + links: + - type: issued-by + target: CTRL-OUTPUT + - type: leads-to-hazard + target: H-4 title: SVG rendering misrepresents topology uca-type: providing context: > @@ -612,6 +795,11 @@ artifacts: - id: UCA-16 type: uca + links: + - type: issued-by + target: CTRL-OUTPUT + - type: leads-to-hazard + target: H-1 title: Diagnostic output suppresses errors uca-type: not-providing context: > @@ -626,6 +814,11 @@ artifacts: - id: UCA-17 type: uca + links: + - type: issued-by + target: CTRL-SYSML2 + - type: leads-to-hazard + target: H-7 title: SysML v2 lowering silently drops construct uca-type: not-providing context: > @@ -643,6 +836,13 @@ artifacts: - id: UCA-18 type: uca + links: + - type: issued-by + target: CTRL-SYSML2 + - type: leads-to-hazard + target: H-7 + - type: leads-to-hazard + target: H-1 title: SysML v2 lowering assigns wrong component category uca-type: providing context: > @@ -660,6 +860,13 @@ artifacts: - id: UCA-19 type: uca + links: + - type: issued-by + target: CTRL-SYSML2 + - type: leads-to-hazard + target: H-7 + - type: leads-to-hazard + target: H-6 title: SysML v2 property semantics lost in lowering uca-type: providing context: > @@ -676,6 +883,13 @@ artifacts: - id: UCA-20 type: uca + links: + - type: issued-by + target: CTRL-SYSML2 + - type: leads-to-hazard + target: H-7 + - type: leads-to-hazard + target: H-3 title: Subcomponent category hardcoded to System uca-type: providing context: > @@ -694,6 +908,11 @@ artifacts: - id: UCA-21 type: uca + links: + - type: issued-by + target: CTRL-CODEGEN + - type: leads-to-hazard + target: H-8 title: Verification rule silently passes when tool missing uca-type: not-providing context: > @@ -710,6 +929,11 @@ artifacts: - id: UCA-22 type: uca + links: + - type: issued-by + target: CTRL-CODEGEN + - type: leads-to-hazard + target: H-8 title: Generated BUILD.bazel omits verification targets uca-type: not-providing context: > @@ -729,6 +953,15 @@ artifacts: - id: CC-1 type: controller-constraint + links: + - type: constrains-controller + target: CTRL-PARSER + - type: inverts-uca + target: UCA-1 + - type: inverts-uca + target: UCA-2 + - type: prevents + target: H-5 title: Parser must emit diagnostic for unrecognized constructs constraint: > The parser must produce an error diagnostic for any token sequence @@ -740,6 +973,13 @@ artifacts: - id: CC-2 type: controller-constraint + links: + - type: constrains-controller + target: CTRL-MODEL + - type: inverts-uca + target: UCA-3 + - type: prevents + target: H-3 title: Lowering must handle all SyntaxKind variants constraint: > The CST-to-ItemTree lowering must have a match arm for every @@ -751,6 +991,13 @@ artifacts: - id: CC-3 type: controller-constraint + links: + - type: constrains-controller + target: CTRL-MODEL + - type: inverts-uca + target: UCA-4 + - type: prevents + target: H-6 title: Property evaluation must use standard unit factors constraint: > Unit conversion factors must match AS5506 Appendix A. @@ -761,6 +1008,13 @@ artifacts: - id: CC-4 type: controller-constraint + links: + - type: constrains-controller + target: CTRL-MODEL + - type: inverts-uca + target: UCA-5 + - type: prevents + target: H-3 title: Resolver must handle ambiguous names deterministically constraint: > When multiple classifiers match a reference, the resolver must @@ -772,6 +1026,13 @@ artifacts: - id: CC-5 type: controller-constraint + links: + - type: constrains-controller + target: CTRL-INSTANCE + - type: inverts-uca + target: UCA-6 + - type: prevents + target: H-3 title: Instance builder must include all non-modal subcomponents constraint: > Subcomponents without in_modes filtering must always be instantiated. @@ -783,6 +1044,13 @@ artifacts: - id: CC-6 type: controller-constraint + links: + - type: constrains-controller + target: CTRL-INSTANCE + - type: inverts-uca + target: UCA-7 + - type: prevents + target: H-3 title: Array dimensions must be validated positive constraint: > Array dimension expressions must evaluate to positive integers. @@ -793,6 +1061,13 @@ artifacts: - id: CC-7 type: controller-constraint + links: + - type: constrains-controller + target: CTRL-INSTANCE + - type: inverts-uca + target: UCA-8 + - type: prevents + target: H-3 title: Connection tracing must verify endpoints constraint: > After multi-level connection tracing, both endpoints must resolve @@ -804,6 +1079,13 @@ artifacts: - id: CC-8 type: controller-constraint + links: + - type: constrains-controller + target: CTRL-INSTANCE + - type: inverts-uca + target: UCA-9 + - type: prevents + target: H-3 title: Instance builder must detect circular containment constraint: > Before recursive expansion, check for cycles in the classifier @@ -815,6 +1097,13 @@ artifacts: - id: CC-9 type: controller-constraint + links: + - type: constrains-controller + target: CTRL-ANALYSIS + - type: inverts-uca + target: UCA-10 + - type: prevents + target: H-1 title: All safety analyses must be registered by default constraint: > The AnalysisRunner must register all implemented analysis passes @@ -826,6 +1115,15 @@ artifacts: - id: CC-10 type: controller-constraint + links: + - type: constrains-controller + target: CTRL-ANALYSIS + - type: inverts-uca + target: UCA-11 + - type: prevents + target: H-1 + - type: prevents + target: H-6 title: Analyses must read properties through validated accessors constraint: > Analysis passes must not directly interpret raw property strings. @@ -837,6 +1135,13 @@ artifacts: - id: CC-11 type: controller-constraint + links: + - type: constrains-controller + target: CTRL-ANALYSIS + - type: inverts-uca + target: UCA-12 + - type: prevents + target: H-1 title: Severity assignment must follow documented criteria constraint: > Error = confirmed standard violation or guaranteed runtime failure. @@ -848,6 +1153,13 @@ artifacts: - id: CC-12 type: controller-constraint + links: + - type: constrains-controller + target: CTRL-ANALYSIS + - type: inverts-uca + target: UCA-13 + - type: prevents + target: H-2 title: Analyses must account for modes and property overrides constraint: > Before reporting a defect, analyses must check whether the condition @@ -859,6 +1171,13 @@ artifacts: - id: CC-13 type: controller-constraint + links: + - type: constrains-controller + target: CTRL-OUTPUT + - type: inverts-uca + target: UCA-14 + - type: prevents + target: H-4 title: Serialization must include all public fields constraint: > Serde derives must be present on all public types. New fields @@ -870,6 +1189,13 @@ artifacts: - id: CC-14 type: controller-constraint + links: + - type: constrains-controller + target: CTRL-OUTPUT + - type: inverts-uca + target: UCA-16 + - type: prevents + target: H-1 title: Output must not filter error diagnostics constraint: > The output formatter must transmit all diagnostics regardless @@ -881,6 +1207,13 @@ artifacts: - id: CC-15 type: controller-constraint + links: + - type: constrains-controller + target: CTRL-SYSML2 + - type: inverts-uca + target: UCA-17 + - type: prevents + target: H-7 title: SysML v2 lowering must emit diagnostic for unhandled constructs constraint: > The lower_node function must not have a silent wildcard arm. Every @@ -893,6 +1226,15 @@ artifacts: - id: CC-16 type: controller-constraint + links: + - type: constrains-controller + target: CTRL-SYSML2 + - type: inverts-uca + target: UCA-18 + - type: inverts-uca + target: UCA-20 + - type: prevents + target: H-7 title: Category inference must be validated against type definition constraint: > After lowering, the inferred category of a part def should be @@ -906,6 +1248,15 @@ artifacts: - id: CC-17 type: controller-constraint + links: + - type: constrains-controller + target: CTRL-SYSML2 + - type: inverts-uca + target: UCA-19 + - type: prevents + target: H-7 + - type: prevents + target: H-6 title: SysML v2 constraint values must produce typed PropertyExpr constraint: > When lowering SysML v2 attribute or constraint usages that carry @@ -919,6 +1270,13 @@ artifacts: - id: CC-18 type: controller-constraint + links: + - type: constrains-controller + target: CTRL-CODEGEN + - type: inverts-uca + target: UCA-21 + - type: prevents + target: H-8 title: Verification rules must fail on missing tools constraint: > Bazel verification rules (verus_verify, lean_verify) must explicitly @@ -931,6 +1289,13 @@ artifacts: - id: CC-19 type: controller-constraint + links: + - type: constrains-controller + target: CTRL-CODEGEN + - type: inverts-uca + target: UCA-22 + - type: prevents + target: H-8 title: Generated crates must include verification targets constraint: > The code generator must produce verus_verify and/or lean_verify @@ -947,6 +1312,13 @@ artifacts: - id: LS-1 type: loss-scenario + links: + - type: caused-by-uca + target: UCA-1 + - type: leads-to-hazard + target: H-5 + - type: leads-to-hazard + target: H-1 title: Annex subclause silently dropped scenario-type: inadequate-control-algorithm description: > @@ -965,6 +1337,15 @@ artifacts: - id: LS-2 type: loss-scenario + links: + - type: caused-by-uca + target: UCA-4 + - type: caused-by-uca + target: UCA-11 + - type: leads-to-hazard + target: H-6 + - type: leads-to-hazard + target: H-1 title: Unit conversion factor wrong for time property scenario-type: inadequate-process-model description: > @@ -982,6 +1363,11 @@ artifacts: - id: LS-3 type: loss-scenario + links: + - type: caused-by-uca + target: UCA-9 + - type: leads-to-hazard + target: H-3 title: Recursive instantiation overflow scenario-type: controller-failure description: > @@ -999,6 +1385,13 @@ artifacts: - id: LS-4 type: loss-scenario + links: + - type: caused-by-uca + target: UCA-8 + - type: leads-to-hazard + target: H-3 + - type: leads-to-hazard + target: H-1 title: Connection tracing follows wrong feature group member scenario-type: inadequate-control-algorithm description: > @@ -1018,6 +1411,11 @@ artifacts: - id: LS-5 type: loss-scenario + links: + - type: caused-by-uca + target: UCA-10 + - type: leads-to-hazard + target: H-1 title: Analysis pass not registered after code addition scenario-type: inadequate-control-algorithm description: > @@ -1035,6 +1433,11 @@ artifacts: - id: LS-6 type: loss-scenario + links: + - type: caused-by-uca + target: UCA-14 + - type: leads-to-hazard + target: H-4 title: JSON drops new InstanceNode field scenario-type: inadequate-feedback description: > @@ -1052,6 +1455,11 @@ artifacts: - id: LS-7 type: loss-scenario + links: + - type: caused-by-uca + target: UCA-11 + - type: leads-to-hazard + target: H-1 title: Modal property override not considered in analysis scenario-type: inadequate-process-model description: > @@ -1069,6 +1477,13 @@ artifacts: - id: LS-8 type: loss-scenario + links: + - type: caused-by-uca + target: UCA-13 + - type: leads-to-hazard + target: H-2 + - type: leads-to-hazard + target: H-1 title: Engineer dismisses analysis due to repeated false positives scenario-type: inadequate-feedback description: > @@ -1086,6 +1501,13 @@ artifacts: - id: LS-9 type: loss-scenario + links: + - type: caused-by-uca + target: UCA-17 + - type: leads-to-hazard + target: H-7 + - type: leads-to-hazard + target: H-1 title: SysML v2 flow definition silently dropped during lowering scenario-type: inadequate-control-algorithm description: > @@ -1106,6 +1528,15 @@ artifacts: - id: LS-10 type: loss-scenario + links: + - type: caused-by-uca + target: UCA-18 + - type: caused-by-uca + target: UCA-20 + - type: leads-to-hazard + target: H-7 + - type: leads-to-hazard + target: H-1 title: Part def misclassified as system instead of process scenario-type: inadequate-process-model description: > @@ -1126,6 +1557,13 @@ artifacts: - id: LS-11 type: loss-scenario + links: + - type: caused-by-uca + target: UCA-19 + - type: leads-to-hazard + target: H-7 + - type: leads-to-hazard + target: H-6 title: SysML v2 timing constraint lowered as Opaque property scenario-type: inadequate-control-algorithm description: > @@ -1146,6 +1584,11 @@ artifacts: - id: LS-12 type: loss-scenario + links: + - type: caused-by-uca + target: UCA-21 + - type: leads-to-hazard + target: H-8 title: Verus not installed but BUILD succeeds from cache scenario-type: inadequate-feedback description: > @@ -1166,6 +1609,11 @@ artifacts: - id: LS-13 type: loss-scenario + links: + - type: caused-by-uca + target: UCA-22 + - type: leads-to-hazard + target: H-8 title: Generated crate has no verification targets scenario-type: inadequate-control-algorithm description: > diff --git a/safety/stpa/rendering-analysis.yaml b/safety/stpa/rendering-analysis.yaml index 08b7e09..f6ccfcf 100644 --- a/safety/stpa/rendering-analysis.yaml +++ b/safety/stpa/rendering-analysis.yaml @@ -53,6 +53,11 @@ artifacts: - id: H-R1 type: hazard + links: + - type: leads-to-loss + target: L-R1 + - type: leads-to-loss + target: L-R3 title: Edge spaghetti obscures connection topology description: > Connections between components are rendered as overlapping, @@ -64,6 +69,11 @@ artifacts: - id: H-R2 type: hazard + links: + - type: leads-to-loss + target: L-R3 + - type: leads-to-loss + target: L-R4 title: No port visibility description: > Ports are not rendered or are rendered without directional @@ -75,6 +85,9 @@ artifacts: - id: H-R3 type: hazard + links: + - type: leads-to-loss + target: L-R2 title: Cannot navigate large models description: > No zoom, pan, search, or filtering capability exists, so @@ -85,6 +98,11 @@ artifacts: - id: H-R4 type: hazard + links: + - type: leads-to-loss + target: L-R1 + - type: leads-to-loss + target: L-R2 title: Layout instability description: > A small change to the AADL model (adding one port, renaming a @@ -96,6 +114,11 @@ artifacts: - id: H-R5 type: hazard + links: + - type: leads-to-loss + target: L-R2 + - type: leads-to-loss + target: L-R4 title: No selection or highlighting description: > There is no way to select a component or connection and see its @@ -109,7 +132,7 @@ artifacts: # ══════════════════════════════════════════════════════════════════════ - id: RENDER-REQ-001 - type: safety-requirement + type: requirement title: Orthogonal edge routing status: implemented description: > @@ -121,7 +144,7 @@ artifacts: verified-by: [VAL-R2] - id: RENDER-REQ-002 - type: safety-requirement + type: requirement title: Visible ports with directional indicators status: implemented description: > @@ -134,7 +157,7 @@ artifacts: verified-by: [VAL-R3] - id: RENDER-REQ-003 - type: safety-requirement + type: requirement title: Interactive HTML with zoom/pan/minimap/search status: partial description: > @@ -147,7 +170,7 @@ artifacts: verified-by: [VAL-R4] - id: RENDER-REQ-004 - type: safety-requirement + type: requirement title: Deterministic layout status: implemented description: > @@ -159,7 +182,7 @@ artifacts: verified-by: [VAL-R1] - id: RENDER-REQ-005 - type: safety-requirement + type: requirement title: Selection and group highlighting status: implemented description: > @@ -171,7 +194,7 @@ artifacts: verified-by: [VAL-R4] - id: RENDER-REQ-006 - type: safety-requirement + type: requirement title: Semantic zoom status: implemented description: > diff --git a/safety/stpa/security.yaml b/safety/stpa/security.yaml index 0460331..1fa5443 100644 --- a/safety/stpa/security.yaml +++ b/safety/stpa/security.yaml @@ -78,6 +78,11 @@ artifacts: - id: H-SEC-1 type: hazard + links: + - type: leads-to-loss + target: L-SEC-1 + - type: leads-to-loss + target: L-SEC-2 title: Unsanitized model names in generated source code description: > Component, port, package, and feature names from the AADL/SysML v2 @@ -92,6 +97,11 @@ artifacts: - id: H-SEC-2 type: hazard + links: + - type: leads-to-loss + target: L-SEC-1 + - type: leads-to-loss + target: L-SEC-2 title: Property values injected into generated code without validation description: > Property values from the AADL model (timing values, dispatch @@ -104,6 +114,9 @@ artifacts: - id: H-SEC-3 type: hazard + links: + - type: leads-to-loss + target: L-SEC-3 title: SysML v2 lowering silently alters component semantics description: > The SysML v2 lowering uses heuristics (infer_category) to decide @@ -117,6 +130,9 @@ artifacts: - id: H-SEC-4 type: hazard + links: + - type: leads-to-loss + target: L-SEC-4 title: Generated workspace pulls untrusted dependencies description: > workspace_gen generates Cargo.toml with hardcoded dependency @@ -130,6 +146,9 @@ artifacts: - id: H-SEC-5 type: hazard + links: + - type: leads-to-loss + target: L-SEC-2 title: Verification artifacts do not cover runtime behavior description: > Generated Lean4 proofs only verify scheduling properties (RTA). @@ -143,6 +162,11 @@ artifacts: - id: H-SEC-6 type: hazard + links: + - type: leads-to-loss + target: L-SEC-1 + - type: leads-to-loss + target: L-SEC-4 title: Codegen writes to arbitrary filesystem paths description: > The codegen CLI writes generated files to --output directory @@ -155,6 +179,9 @@ artifacts: - id: H-SEC-7 type: hazard + links: + - type: leads-to-loss + target: L-SEC-5 title: Model complexity causes resource exhaustion description: > The codegen pipeline iterates over all_components() multiple @@ -171,6 +198,11 @@ artifacts: - id: SC-SEC-1 type: system-constraint + links: + - type: prevents + target: H-SEC-1 + - type: prevents + target: H-SEC-2 title: No code injection through model-derived identifiers description: > Names and values extracted from input models must be sanitized @@ -181,6 +213,9 @@ artifacts: - id: SC-SEC-2 type: system-constraint + links: + - type: prevents + target: H-SEC-6 title: Generated file paths must be confined to output directory description: > All generated file paths must be validated to resolve within the @@ -190,6 +225,9 @@ artifacts: - id: SC-SEC-3 type: system-constraint + links: + - type: prevents + target: H-SEC-5 title: Verification must cover safety-critical properties description: > Generated verification artifacts must cover the same safety @@ -200,6 +238,9 @@ artifacts: - id: SC-SEC-4 type: system-constraint + links: + - type: prevents + target: H-SEC-3 title: SysML v2 lowering must not silently drop constructs description: > Unrecognized SysML v2 syntax kinds must produce diagnostics. @@ -209,6 +250,9 @@ artifacts: - id: SC-SEC-5 type: system-constraint + links: + - type: prevents + target: H-SEC-4 title: Generated build configurations must use pinned dependencies description: > Generated Cargo.toml and BUILD.bazel must use exact version pins, @@ -218,6 +262,9 @@ artifacts: - id: SC-SEC-6 type: system-constraint + links: + - type: prevents + target: H-SEC-7 title: Resource bounds on code generation description: > Code generation must enforce limits on the number of generated @@ -312,6 +359,11 @@ artifacts: - id: CA-SEC-LOWER type: control-action + links: + - type: issued-by + target: CTRL-SEC-SYSML2 + - type: acts-on + target: CP-SEC-MODEL-INPUT title: Lower SysML v2 to AADL action: Transform SysML v2 CST into AADL ItemTree source: CTRL-SEC-SYSML2 @@ -319,6 +371,11 @@ artifacts: - id: CA-SEC-GENERATE type: control-action + links: + - type: issued-by + target: CTRL-SEC-CODEGEN + - type: acts-on + target: CP-SEC-GENERATED-CODE title: Generate code from AADL model action: Produce Rust, WIT, config, proof, and build files from instance model source: CTRL-SEC-CODEGEN @@ -326,6 +383,11 @@ artifacts: - id: CA-SEC-GENPROOF type: control-action + links: + - type: issued-by + target: CTRL-SEC-PROOFGEN + - type: acts-on + target: CP-SEC-GENERATED-CODE title: Generate verification artifacts action: Produce Lean4 proofs and Kani harnesses from timing properties source: CTRL-SEC-PROOFGEN @@ -333,6 +395,11 @@ artifacts: - id: CA-SEC-GENBUILD type: control-action + links: + - type: issued-by + target: CTRL-SEC-BUILDGEN + - type: acts-on + target: CP-SEC-GENERATED-CODE title: Generate build configuration action: Produce Cargo.toml and BUILD.bazel workspace files source: CTRL-SEC-BUILDGEN @@ -340,6 +407,11 @@ artifacts: - id: CA-SEC-VERIFY type: control-action + links: + - type: issued-by + target: CTRL-SEC-VERUS + - type: acts-on + target: CP-SEC-VERIFIED-ARTIFACTS title: Run formal verification action: Execute Verus/Lean4/Kani on generated artifacts source: CTRL-SEC-VERUS @@ -353,6 +425,11 @@ artifacts: - id: UCA-SEC-1 type: uca + links: + - type: issued-by + target: CTRL-SEC-SYSML2 + - type: leads-to-hazard + target: H-SEC-3 title: Lowering silently drops security-relevant constructs uca-type: not-providing context: > @@ -370,6 +447,11 @@ artifacts: - id: UCA-SEC-2 type: uca + links: + - type: issued-by + target: CTRL-SEC-SYSML2 + - type: leads-to-hazard + target: H-SEC-3 title: Category heuristic misclassifies security-critical component uca-type: providing context: > @@ -389,6 +471,11 @@ artifacts: - id: UCA-SEC-3 type: uca + links: + - type: issued-by + target: CTRL-SEC-CODEGEN + - type: leads-to-hazard + target: H-SEC-1 title: Codegen interpolates unsanitized name into Rust source uca-type: providing context: > @@ -407,6 +494,11 @@ artifacts: - id: UCA-SEC-4 type: uca + links: + - type: issued-by + target: CTRL-SEC-CODEGEN + - type: leads-to-hazard + target: H-SEC-2 title: Codegen embeds property value in Rust constant without bounds uca-type: providing context: > @@ -423,6 +515,11 @@ artifacts: - id: UCA-SEC-5 type: uca + links: + - type: issued-by + target: CTRL-SEC-CODEGEN + - type: leads-to-hazard + target: H-SEC-6 title: Codegen writes file outside output directory uca-type: providing context: > @@ -441,6 +538,11 @@ artifacts: - id: UCA-SEC-6 type: uca + links: + - type: issued-by + target: CTRL-SEC-CODEGEN + - type: leads-to-hazard + target: H-SEC-1 title: Codegen produces WIT with type confusion uca-type: providing context: > @@ -462,6 +564,11 @@ artifacts: - id: UCA-SEC-7 type: uca + links: + - type: issued-by + target: CTRL-SEC-PROOFGEN + - type: leads-to-hazard + target: H-SEC-5 title: Proof generator substitutes default timing values uca-type: providing context: > @@ -479,6 +586,11 @@ artifacts: - id: UCA-SEC-8 type: uca + links: + - type: issued-by + target: CTRL-SEC-PROOFGEN + - type: leads-to-hazard + target: H-SEC-5 title: Kani harness verifies only base case without interference uca-type: stopped-too-soon context: > @@ -498,6 +610,11 @@ artifacts: - id: UCA-SEC-9 type: uca + links: + - type: issued-by + target: CTRL-SEC-BUILDGEN + - type: leads-to-hazard + target: H-SEC-4 title: Generated Cargo.toml uses unpinned dependency versions uca-type: providing context: > @@ -514,6 +631,11 @@ artifacts: - id: UCA-SEC-10 type: uca + links: + - type: issued-by + target: CTRL-SEC-BUILDGEN + - type: leads-to-hazard + target: H-SEC-4 title: Generated crate names may collide with public registry uca-type: providing context: > @@ -532,6 +654,13 @@ artifacts: - id: UCA-SEC-11 type: uca + links: + - type: issued-by + target: CTRL-SEC-VERUS + - type: leads-to-hazard + target: H-SEC-1 + - type: leads-to-hazard + target: H-SEC-4 title: Verus rule passes shell-injectable paths uca-type: providing context: > @@ -548,6 +677,13 @@ artifacts: - id: UCA-SEC-12 type: uca + links: + - type: issued-by + target: CTRL-SEC-VERUS + - type: leads-to-hazard + target: H-SEC-1 + - type: leads-to-hazard + target: H-SEC-2 title: wasm-tools component new accepts unverified core module uca-type: not-providing context: > @@ -570,6 +706,15 @@ artifacts: - id: CC-SEC-1 type: controller-constraint + links: + - type: constrains-controller + target: CTRL-SEC-CODEGEN + - type: inverts-uca + target: UCA-SEC-3 + - type: inverts-uca + target: UCA-SEC-6 + - type: prevents + target: H-SEC-1 title: Language-specific sanitization for all generated code constraint: > Every model-derived string interpolated into generated source @@ -583,6 +728,15 @@ artifacts: - id: CC-SEC-2 type: controller-constraint + links: + - type: constrains-controller + target: CTRL-SEC-CODEGEN + - type: inverts-uca + target: UCA-SEC-4 + - type: inverts-uca + target: UCA-SEC-7 + - type: prevents + target: H-SEC-2 title: Timing property bounds validation before code generation constraint: > Before generating code or proofs, timing properties must be @@ -595,6 +749,13 @@ artifacts: - id: CC-SEC-3 type: controller-constraint + links: + - type: constrains-controller + target: CTRL-SEC-CODEGEN + - type: inverts-uca + target: UCA-SEC-5 + - type: prevents + target: H-SEC-6 title: Output path confinement constraint: > All generated file paths must be canonicalized and verified @@ -607,6 +768,15 @@ artifacts: - id: CC-SEC-4 type: controller-constraint + links: + - type: constrains-controller + target: CTRL-SEC-SYSML2 + - type: inverts-uca + target: UCA-SEC-1 + - type: inverts-uca + target: UCA-SEC-2 + - type: prevents + target: H-SEC-3 title: SysML v2 lowering must diagnose unhandled constructs constraint: > The wildcard match arm in lower_node must emit a diagnostic @@ -619,6 +789,15 @@ artifacts: - id: CC-SEC-5 type: controller-constraint + links: + - type: constrains-controller + target: CTRL-SEC-BUILDGEN + - type: inverts-uca + target: UCA-SEC-9 + - type: inverts-uca + target: UCA-SEC-10 + - type: prevents + target: H-SEC-4 title: Generated dependencies must use exact version pins with checksums constraint: > Generated Cargo.toml must use exact version pins (= prefix) @@ -631,6 +810,15 @@ artifacts: - id: CC-SEC-6 type: controller-constraint + links: + - type: constrains-controller + target: CTRL-SEC-PROOFGEN + - type: inverts-uca + target: UCA-SEC-7 + - type: inverts-uca + target: UCA-SEC-8 + - type: prevents + target: H-SEC-5 title: Verification harnesses must document coverage scope constraint: > Generated Kani harnesses and Lean4 proofs must include @@ -643,6 +831,13 @@ artifacts: - id: CC-SEC-7 type: controller-constraint + links: + - type: constrains-controller + target: CTRL-SEC-VERUS + - type: inverts-uca + target: UCA-SEC-11 + - type: prevents + target: H-SEC-1 title: Bazel rules must not construct shell commands from paths constraint: > Verus and wasm-tools Bazel rules must use ctx.actions.run @@ -654,6 +849,15 @@ artifacts: - id: CC-SEC-8 type: controller-constraint + links: + - type: constrains-controller + target: CTRL-SEC-VERUS + - type: inverts-uca + target: UCA-SEC-12 + - type: prevents + target: H-SEC-1 + - type: prevents + target: H-SEC-2 title: WASM component must verify provenance of core module constraint: > The wasm_component rule must verify that the core WASM module @@ -670,6 +874,15 @@ artifacts: - id: LS-SEC-1 type: loss-scenario + links: + - type: caused-by-uca + target: UCA-SEC-3 + - type: caused-by-uca + target: UCA-SEC-4 + - type: leads-to-hazard + target: H-SEC-1 + - type: leads-to-hazard + target: H-SEC-2 title: "Attack path: model-driven code injection via component name" scenario-type: inadequate-control-algorithm description: > @@ -694,6 +907,17 @@ artifacts: - id: LS-SEC-2 type: loss-scenario + links: + - type: caused-by-uca + target: UCA-SEC-4 + - type: caused-by-uca + target: UCA-SEC-7 + - type: caused-by-uca + target: UCA-SEC-8 + - type: leads-to-hazard + target: H-SEC-2 + - type: leads-to-hazard + target: H-SEC-5 title: "Attack path: timing property manipulation for proof bypass" scenario-type: inadequate-process-model description: > @@ -716,6 +940,11 @@ artifacts: - id: LS-SEC-3 type: loss-scenario + links: + - type: caused-by-uca + target: UCA-SEC-2 + - type: leads-to-hazard + target: H-SEC-3 title: "Attack path: SysML v2 category confusion for partition bypass" scenario-type: inadequate-control-algorithm description: > @@ -739,6 +968,11 @@ artifacts: - id: LS-SEC-4 type: loss-scenario + links: + - type: caused-by-uca + target: UCA-SEC-10 + - type: leads-to-hazard + target: H-SEC-4 title: "Attack path: dependency confusion via generated workspace" scenario-type: inadequate-control-algorithm description: > @@ -764,6 +998,13 @@ artifacts: - id: LS-SEC-5 type: loss-scenario + links: + - type: caused-by-uca + target: UCA-SEC-11 + - type: leads-to-hazard + target: H-SEC-1 + - type: leads-to-hazard + target: H-SEC-4 title: "Attack path: shell injection via Verus verification rule" scenario-type: inadequate-control-algorithm description: > @@ -787,6 +1028,13 @@ artifacts: - id: LS-SEC-6 type: loss-scenario + links: + - type: caused-by-uca + target: UCA-SEC-12 + - type: leads-to-hazard + target: H-SEC-1 + - type: leads-to-hazard + target: H-SEC-2 title: "Attack path: WASM component substitution via build cache" scenario-type: inadequate-feedback description: > @@ -808,6 +1056,11 @@ artifacts: - id: LS-SEC-7 type: loss-scenario + links: + - type: caused-by-uca + target: UCA-SEC-7 + - type: leads-to-hazard + target: H-SEC-7 title: "Attack path: resource exhaustion via model complexity bomb" scenario-type: inadequate-control-algorithm description: > @@ -828,6 +1081,11 @@ artifacts: - id: LS-SEC-8 type: loss-scenario + links: + - type: caused-by-uca + target: UCA-SEC-1 + - type: leads-to-hazard + target: H-SEC-3 title: "Attack path: SysML v2 wildcard drops security annotations" scenario-type: inadequate-control-algorithm description: > diff --git a/safety/stpa/solver-analysis.yaml b/safety/stpa/solver-analysis.yaml index 0cb9fd1..44f8e9c 100644 --- a/safety/stpa/solver-analysis.yaml +++ b/safety/stpa/solver-analysis.yaml @@ -97,6 +97,15 @@ artifacts: - id: H-S1 type: hazard + links: + - type: leads-to-loss + target: L-S1 + - type: leads-to-loss + target: L-S2 + - type: leads-to-loss + target: L-S3 + - type: leads-to-loss + target: L-S6 title: Solver marks infeasible binding as feasible description: > The solver produces a binding configuration that violates one or @@ -108,6 +117,9 @@ artifacts: - id: H-S2 type: hazard + links: + - type: leads-to-loss + target: L-S1 title: Solver misses timing constraint description: > The solver's schedulability check (RTA at Layer 0) uses incorrect @@ -118,6 +130,9 @@ artifacts: - id: H-S3 type: hazard + links: + - type: leads-to-loss + target: L-S2 title: Solver allows mixed-criticality without fault containment description: > The solver co-locates components of different ASIL/DAL/SIL levels @@ -129,6 +144,9 @@ artifacts: - id: H-S4 type: hazard + links: + - type: leads-to-loss + target: L-S3 title: Solver selects protocol with insufficient properties description: > The solver selects a virtual bus (communication protocol) for a @@ -141,6 +159,9 @@ artifacts: - id: H-S5 type: hazard + links: + - type: leads-to-loss + target: L-S4 title: Source rewrite corrupts AADL model description: > The solver's rowan CST editing inserts a property association in @@ -151,6 +172,9 @@ artifacts: - id: H-S6 type: hazard + links: + - type: leads-to-loss + target: L-S5 title: Optimality certificate is invalid description: > The solver's optimality proof (e.g., dual bound from LP relaxation, @@ -163,6 +187,11 @@ artifacts: - id: H-S7 type: hazard + links: + - type: leads-to-loss + target: L-S5 + - type: leads-to-loss + target: L-S1 title: Solver produces non-deterministic results description: > Given the same input model and constraints, the solver produces @@ -174,6 +203,11 @@ artifacts: - id: H-S8 type: hazard + links: + - type: leads-to-loss + target: L-S1 + - type: leads-to-loss + target: L-S4 title: Stale analysis after source rewrite description: > The solver rewrites AADL source properties but the salsa @@ -185,6 +219,11 @@ artifacts: - id: H-S9 type: hazard + links: + - type: leads-to-loss + target: L-S1 + - type: leads-to-loss + target: L-S3 title: Hierarchical composition violates global constraint description: > Each solver layer produces a locally optimal solution, but the @@ -197,6 +236,9 @@ artifacts: - id: H-S10 type: hazard + links: + - type: leads-to-loss + target: L-S6 title: Resource accounting error description: > The solver's resource budget tracking (memory, weight, power) @@ -207,6 +249,13 @@ artifacts: - id: H-S11 type: hazard + links: + - type: leads-to-loss + target: L-S1 + - type: leads-to-loss + target: L-S3 + - type: leads-to-loss + target: L-S6 title: Incomplete model input causes unsound solution description: > The AADL model is missing properties that the solver needs @@ -219,6 +268,9 @@ artifacts: - id: H-S12 type: hazard + links: + - type: leads-to-loss + target: L-S1 title: Floating-point precision causes incorrect schedulability description: > The solver's RTA computation uses floating-point arithmetic @@ -235,6 +287,9 @@ artifacts: - id: SC-S1 type: system-constraint + links: + - type: prevents + target: H-S1 title: Solver must not produce infeasible bindings marked feasible description: > Every binding configuration reported as feasible must satisfy all @@ -244,6 +299,11 @@ artifacts: - id: SC-S2 type: system-constraint + links: + - type: prevents + target: H-S2 + - type: prevents + target: H-S12 title: Timing analysis must be conservative description: > The solver's schedulability analysis must be pessimistic — it must @@ -253,6 +313,9 @@ artifacts: - id: SC-S3 type: system-constraint + links: + - type: prevents + target: H-S3 title: Safety level separation must be enforced description: > The solver must not co-locate components of different safety levels @@ -262,6 +325,9 @@ artifacts: - id: SC-S4 type: system-constraint + links: + - type: prevents + target: H-S4 title: Protocol selection must use worst-case properties description: > Protocol matching must use worst-case (not nominal) property values. @@ -271,6 +337,9 @@ artifacts: - id: SC-S5 type: system-constraint + links: + - type: prevents + target: H-S5 title: Source rewrites must preserve model validity description: > After source rewriting, the modified AADL files must parse without @@ -280,6 +349,9 @@ artifacts: - id: SC-S6 type: system-constraint + links: + - type: prevents + target: H-S6 title: Optimality certificates must be independently verifiable description: > Optimality certificates must contain sufficient information for @@ -289,6 +361,9 @@ artifacts: - id: SC-S7 type: system-constraint + links: + - type: prevents + target: H-S7 title: Solver results must be deterministic description: > The solver must produce identical results given identical inputs. @@ -297,6 +372,9 @@ artifacts: - id: SC-S8 type: system-constraint + links: + - type: prevents + target: H-S8 title: Cache must be invalidated after source rewrite description: > After source rewriting, the solver must either invalidate all @@ -306,6 +384,9 @@ artifacts: - id: SC-S9 type: system-constraint + links: + - type: prevents + target: H-S9 title: Global constraints must be verified after hierarchical composition description: > After all solver layers complete, a global validation pass must @@ -315,6 +396,9 @@ artifacts: - id: SC-S10 type: system-constraint + links: + - type: prevents + target: H-S11 title: Missing model properties must produce diagnostics description: > When the solver encounters a component without required properties @@ -436,6 +520,11 @@ artifacts: - id: CA-SOLVE type: control-action + links: + - type: issued-by + target: CTRL-SOLVER + - type: acts-on + target: CP-BINDING title: Solve deployment configuration action: > Compute software-to-hardware binding by running Layer 0-3 solvers @@ -445,6 +534,11 @@ artifacts: - id: CA-SCHEDULE type: control-action + links: + - type: issued-by + target: CTRL-LAYER0 + - type: acts-on + target: CP-BINDING title: Check thread schedulability (Layer 0) action: > Perform response-time analysis for threads assigned to a processor. @@ -455,6 +549,11 @@ artifacts: - id: CA-ALLOCATE type: control-action + links: + - type: issued-by + target: CTRL-LAYER1 + - type: acts-on + target: CP-BINDING title: Allocate processes to processors (Layer 1) action: > Assign processes to processors using bin-packing with schedulability @@ -464,6 +563,11 @@ artifacts: - id: CA-BIND-BUS type: control-action + links: + - type: issued-by + target: CTRL-LAYER2 + - type: acts-on + target: CP-BINDING title: Bind connections to buses and select protocols (Layer 2) action: > Select communication protocols from the virtual bus library for @@ -473,6 +577,11 @@ artifacts: - id: CA-OPTIMIZE type: control-action + links: + - type: issued-by + target: CTRL-LAYER3 + - type: acts-on + target: CP-BINDING title: Global optimization (Layer 3) action: > Optimize end-to-end latency, verify safety decomposition, and @@ -482,6 +591,11 @@ artifacts: - id: CA-REWRITE type: control-action + links: + - type: issued-by + target: CTRL-REWRITER + - type: acts-on + target: CP-AADL-SOURCE title: Rewrite AADL source with binding properties action: > Apply computed binding configuration as AADL property associations @@ -491,6 +605,11 @@ artifacts: - id: CA-CERTIFY type: control-action + links: + - type: issued-by + target: CTRL-CERTIFIER + - type: acts-on + target: CP-CERTIFICATE title: Generate optimality certificate action: > Produce a mathematical certificate proving the solution quality @@ -500,6 +619,11 @@ artifacts: - id: CA-VALIDATE type: control-action + links: + - type: issued-by + target: CTRL-SOLVER + - type: acts-on + target: CP-BINDING title: Post-solve validation action: > Re-run analysis passes on the rewritten model to verify all @@ -515,6 +639,13 @@ artifacts: - id: UCA-S1 type: uca + links: + - type: issued-by + target: CTRL-LAYER0 + - type: leads-to-hazard + target: H-S2 + - type: leads-to-hazard + target: H-S12 title: RTA accepts unschedulable task set uca-type: providing context: > @@ -531,6 +662,13 @@ artifacts: - id: UCA-S2 type: uca + links: + - type: issued-by + target: CTRL-LAYER0 + - type: leads-to-hazard + target: H-S1 + - type: leads-to-hazard + target: H-S2 title: RTA not performed for a processor uca-type: not-providing context: > @@ -547,6 +685,11 @@ artifacts: - id: UCA-S3 type: uca + links: + - type: issued-by + target: CTRL-LAYER0 + - type: leads-to-hazard + target: H-S2 title: RTA uses wrong execution time value uca-type: providing context: > @@ -563,6 +706,13 @@ artifacts: - id: UCA-S4 type: uca + links: + - type: issued-by + target: CTRL-LAYER1 + - type: leads-to-hazard + target: H-S1 + - type: leads-to-hazard + target: H-S10 title: Allocator exceeds processor capacity uca-type: providing context: > @@ -578,6 +728,13 @@ artifacts: - id: UCA-S5 type: uca + links: + - type: issued-by + target: CTRL-LAYER1 + - type: leads-to-hazard + target: H-S1 + - type: leads-to-hazard + target: H-S3 title: Allocator ignores affinity constraints uca-type: not-providing context: > @@ -593,6 +750,13 @@ artifacts: - id: UCA-S6 type: uca + links: + - type: issued-by + target: CTRL-LAYER1 + - type: leads-to-hazard + target: H-S2 + - type: leads-to-hazard + target: H-S9 title: Allocator does not invoke Layer 0 for new assignment uca-type: not-providing context: > @@ -610,6 +774,11 @@ artifacts: - id: UCA-S7 type: uca + links: + - type: issued-by + target: CTRL-LAYER2 + - type: leads-to-hazard + target: H-S4 title: Protocol selected with insufficient bandwidth uca-type: providing context: > @@ -626,6 +795,11 @@ artifacts: - id: UCA-S8 type: uca + links: + - type: issued-by + target: CTRL-LAYER2 + - type: leads-to-hazard + target: H-S4 title: Protocol selected without matching security level uca-type: providing context: > @@ -641,6 +815,13 @@ artifacts: - id: UCA-S9 type: uca + links: + - type: issued-by + target: CTRL-LAYER2 + - type: leads-to-hazard + target: H-S3 + - type: leads-to-hazard + target: H-S4 title: Bus binding not performed for cross-processor connection uca-type: not-providing context: > @@ -658,6 +839,13 @@ artifacts: - id: UCA-S10 type: uca + links: + - type: issued-by + target: CTRL-LAYER3 + - type: leads-to-hazard + target: H-S1 + - type: leads-to-hazard + target: H-S9 title: E2E latency check uses incomplete path uca-type: providing context: > @@ -673,6 +861,11 @@ artifacts: - id: UCA-S11 type: uca + links: + - type: issued-by + target: CTRL-LAYER3 + - type: leads-to-hazard + target: H-S3 title: Safety decomposition allows inadequate containment uca-type: providing context: > @@ -688,6 +881,11 @@ artifacts: - id: UCA-S12 type: uca + links: + - type: issued-by + target: CTRL-LAYER3 + - type: leads-to-hazard + target: H-S9 title: Global validation not performed after layer composition uca-type: not-providing context: > @@ -705,6 +903,11 @@ artifacts: - id: UCA-S13 type: uca + links: + - type: issued-by + target: CTRL-REWRITER + - type: leads-to-hazard + target: H-S5 title: Property inserted in wrong component scope uca-type: providing context: > @@ -722,6 +925,11 @@ artifacts: - id: UCA-S14 type: uca + links: + - type: issued-by + target: CTRL-REWRITER + - type: leads-to-hazard + target: H-S5 title: Rewriter deletes existing property uca-type: providing context: > @@ -737,6 +945,11 @@ artifacts: - id: UCA-S15 type: uca + links: + - type: issued-by + target: CTRL-REWRITER + - type: leads-to-hazard + target: H-S5 title: Rewriter produces invalid AADL syntax uca-type: providing context: > @@ -751,6 +964,13 @@ artifacts: - id: UCA-S16 type: uca + links: + - type: issued-by + target: CTRL-REWRITER + - type: leads-to-hazard + target: H-S5 + - type: leads-to-hazard + target: H-S8 title: Rewriter does not update all files uca-type: not-providing context: > @@ -768,6 +988,11 @@ artifacts: - id: UCA-S17 type: uca + links: + - type: issued-by + target: CTRL-CERTIFIER + - type: leads-to-hazard + target: H-S6 title: Certificate claims optimal when solution is suboptimal uca-type: providing context: > @@ -783,6 +1008,11 @@ artifacts: - id: UCA-S18 type: uca + links: + - type: issued-by + target: CTRL-CERTIFIER + - type: leads-to-hazard + target: H-S6 title: Certificate claims infeasible when solution exists uca-type: providing context: > @@ -799,6 +1029,11 @@ artifacts: - id: UCA-S19 type: uca + links: + - type: issued-by + target: CTRL-CERTIFIER + - type: leads-to-hazard + target: H-S6 title: Certificate not generated uca-type: not-providing context: > @@ -816,6 +1051,13 @@ artifacts: - id: UCA-S20 type: uca + links: + - type: issued-by + target: CTRL-SOLVER + - type: leads-to-hazard + target: H-S1 + - type: leads-to-hazard + target: H-S8 title: Post-solve validation not performed uca-type: not-providing context: > @@ -832,6 +1074,11 @@ artifacts: - id: UCA-S21 type: uca + links: + - type: issued-by + target: CTRL-SOLVER + - type: leads-to-hazard + target: H-S8 title: Post-solve validation uses stale cache uca-type: providing context: > @@ -849,6 +1096,11 @@ artifacts: - id: UCA-S22 type: uca + links: + - type: issued-by + target: CTRL-SOLVER + - type: leads-to-hazard + target: H-S11 title: Solver uses default for missing property uca-type: providing context: > @@ -866,6 +1118,11 @@ artifacts: - id: UCA-S23 type: uca + links: + - type: issued-by + target: CTRL-LAYER2 + - type: leads-to-hazard + target: H-S4 title: Virtual bus library properties do not match reality uca-type: providing context: > @@ -885,6 +1142,15 @@ artifacts: - id: CC-S1 type: controller-constraint + links: + - type: constrains-controller + target: CTRL-LAYER0 + - type: inverts-uca + target: UCA-S1 + - type: inverts-uca + target: UCA-S3 + - type: prevents + target: H-S2 title: RTA must use worst-case parameters constraint: > Response-time analysis must use worst-case execution time (maximum @@ -898,6 +1164,15 @@ artifacts: - id: CC-S2 type: controller-constraint + links: + - type: constrains-controller + target: CTRL-LAYER0 + - type: inverts-uca + target: UCA-S2 + - type: inverts-uca + target: UCA-S6 + - type: prevents + target: H-S2 title: Schedulability must be checked for every populated processor constraint: > After Layer 1 allocation completes, Layer 0 RTA must be re-run for @@ -909,6 +1184,13 @@ artifacts: - id: CC-S3 type: controller-constraint + links: + - type: constrains-controller + target: CTRL-LAYER1 + - type: inverts-uca + target: UCA-S4 + - type: prevents + target: H-S10 title: Resource accounting must include all bound components constraint: > Memory, CPU, weight, and power budgets must account for every @@ -920,6 +1202,13 @@ artifacts: - id: CC-S4 type: controller-constraint + links: + - type: constrains-controller + target: CTRL-LAYER1 + - type: inverts-uca + target: UCA-S5 + - type: prevents + target: H-S3 title: Affinity and anti-affinity constraints must be enforced constraint: > The allocator must read Allowed_Processor_Binding, Not_Collocated, @@ -931,6 +1220,13 @@ artifacts: - id: CC-S5 type: controller-constraint + links: + - type: constrains-controller + target: CTRL-LAYER2 + - type: inverts-uca + target: UCA-S7 + - type: prevents + target: H-S4 title: Aggregate bus bandwidth must be checked constraint: > Protocol selection must check aggregate bandwidth of all connections @@ -942,6 +1238,13 @@ artifacts: - id: CC-S6 type: controller-constraint + links: + - type: constrains-controller + target: CTRL-LAYER2 + - type: inverts-uca + target: UCA-S8 + - type: prevents + target: H-S4 title: Security zone matching must be enforced constraint: > Connections crossing security zone boundaries must be bound to @@ -954,6 +1257,13 @@ artifacts: - id: CC-S7 type: controller-constraint + links: + - type: constrains-controller + target: CTRL-LAYER2 + - type: inverts-uca + target: UCA-S9 + - type: prevents + target: H-S4 title: All cross-processor connections must be identified constraint: > The solver must enumerate all connections whose source and @@ -965,6 +1275,15 @@ artifacts: - id: CC-S8 type: controller-constraint + links: + - type: constrains-controller + target: CTRL-LAYER3 + - type: inverts-uca + target: UCA-S10 + - type: prevents + target: H-S1 + - type: prevents + target: H-S9 title: E2E latency must include all path segments constraint: > End-to-end latency computation must include: thread execution time, @@ -976,6 +1295,13 @@ artifacts: - id: CC-S9 type: controller-constraint + links: + - type: constrains-controller + target: CTRL-LAYER3 + - type: inverts-uca + target: UCA-S11 + - type: prevents + target: H-S3 title: Safety co-location requires verified containment constraint: > Co-locating components of different safety levels on the same @@ -988,6 +1314,13 @@ artifacts: - id: CC-S10 type: controller-constraint + links: + - type: constrains-controller + target: CTRL-LAYER3 + - type: inverts-uca + target: UCA-S12 + - type: prevents + target: H-S9 title: Global validation must run after all layers complete constraint: > After Layer 0-2 produce their results, Layer 3 must run a @@ -1000,6 +1333,13 @@ artifacts: - id: CC-S11 type: controller-constraint + links: + - type: constrains-controller + target: CTRL-REWRITER + - type: inverts-uca + target: UCA-S13 + - type: prevents + target: H-S5 title: Source rewrite must target correct CST node constraint: > The rewriter must identify the CST node for the target component @@ -1011,6 +1351,13 @@ artifacts: - id: CC-S12 type: controller-constraint + links: + - type: constrains-controller + target: CTRL-REWRITER + - type: inverts-uca + target: UCA-S14 + - type: prevents + target: H-S5 title: Source rewrite must preserve existing properties constraint: > The rewriter must not delete, modify, or reorder existing property @@ -1023,6 +1370,13 @@ artifacts: - id: CC-S13 type: controller-constraint + links: + - type: constrains-controller + target: CTRL-REWRITER + - type: inverts-uca + target: UCA-S15 + - type: prevents + target: H-S5 title: Source rewrite output must parse cleanly constraint: > After rewriting, the modified AADL source must be re-parsed by spar @@ -1034,6 +1388,13 @@ artifacts: - id: CC-S14 type: controller-constraint + links: + - type: constrains-controller + target: CTRL-REWRITER + - type: inverts-uca + target: UCA-S16 + - type: prevents + target: H-S5 title: All affected files must be rewritten constraint: > The rewriter must identify all AADL files that need modification @@ -1045,6 +1406,15 @@ artifacts: - id: CC-S15 type: controller-constraint + links: + - type: constrains-controller + target: CTRL-CERTIFIER + - type: inverts-uca + target: UCA-S17 + - type: inverts-uca + target: UCA-S18 + - type: prevents + target: H-S6 title: Optimality certificate must be independently verifiable constraint: > The certificate must contain: (a) the objective function value, @@ -1057,6 +1427,13 @@ artifacts: - id: CC-S16 type: controller-constraint + links: + - type: constrains-controller + target: CTRL-CERTIFIER + - type: inverts-uca + target: UCA-S19 + - type: prevents + target: H-S6 title: Certificate must be generated for every solver run constraint: > Every solver invocation must produce a certificate, including @@ -1068,6 +1445,15 @@ artifacts: - id: CC-S17 type: controller-constraint + links: + - type: constrains-controller + target: CTRL-SOLVER + - type: inverts-uca + target: UCA-S20 + - type: inverts-uca + target: UCA-S21 + - type: prevents + target: H-S8 title: Post-solve analysis must use fresh computation constraint: > Post-solve validation must force full re-computation (either by @@ -1080,6 +1466,13 @@ artifacts: - id: CC-S18 type: controller-constraint + links: + - type: constrains-controller + target: CTRL-SOLVER + - type: inverts-uca + target: UCA-S22 + - type: prevents + target: H-S11 title: Missing properties must be errors, not defaults constraint: > When the solver encounters a component without a required property @@ -1092,6 +1485,13 @@ artifacts: - id: CC-S19 type: controller-constraint + links: + - type: constrains-controller + target: CTRL-LAYER2 + - type: inverts-uca + target: UCA-S23 + - type: prevents + target: H-S4 title: Virtual bus library must distinguish nominal vs worst-case constraint: > The virtual bus library must provide separate worst-case and @@ -1104,6 +1504,13 @@ artifacts: - id: CC-S20 type: controller-constraint + links: + - type: constrains-controller + target: CTRL-LAYER0 + - type: inverts-uca + target: UCA-S1 + - type: prevents + target: H-S12 title: Numerical computation must use integer or bounded arithmetic constraint: > Schedulability computations must use integer arithmetic (picosecond @@ -1120,6 +1527,13 @@ artifacts: - id: LS-S1 type: loss-scenario + links: + - type: caused-by-uca + target: UCA-S1 + - type: leads-to-hazard + target: H-S12 + - type: leads-to-hazard + target: H-S2 title: Floating-point RTA accepts boundary-case task set scenario-type: inadequate-control-algorithm description: > @@ -1141,6 +1555,11 @@ artifacts: - id: LS-S2 type: loss-scenario + links: + - type: caused-by-uca + target: UCA-S4 + - type: leads-to-hazard + target: H-S10 title: Allocator double-counts shared memory scenario-type: inadequate-process-model description: > @@ -1161,6 +1580,11 @@ artifacts: - id: LS-S3 type: loss-scenario + links: + - type: caused-by-uca + target: UCA-S5 + - type: leads-to-hazard + target: H-S3 title: Solver ignores Allowed_Processor_Binding constraint scenario-type: inadequate-control-algorithm description: > @@ -1179,6 +1603,11 @@ artifacts: - id: LS-S4 type: loss-scenario + links: + - type: caused-by-uca + target: UCA-S7 + - type: leads-to-hazard + target: H-S4 title: Aggregate bus bandwidth exceeded scenario-type: inadequate-control-algorithm description: > @@ -1197,6 +1626,11 @@ artifacts: - id: LS-S5 type: loss-scenario + links: + - type: caused-by-uca + target: UCA-S13 + - type: leads-to-hazard + target: H-S5 title: Rewriter inserts binding on wrong subcomponent scenario-type: inadequate-control-algorithm description: > @@ -1217,6 +1651,11 @@ artifacts: - id: LS-S6 type: loss-scenario + links: + - type: caused-by-uca + target: UCA-S15 + - type: leads-to-hazard + target: H-S5 title: Rewriter corrupts property block formatting scenario-type: inadequate-control-algorithm description: > @@ -1236,6 +1675,11 @@ artifacts: - id: LS-S7 type: loss-scenario + links: + - type: caused-by-uca + target: UCA-S21 + - type: leads-to-hazard + target: H-S8 title: Salsa cache returns pre-rewrite property values scenario-type: inadequate-feedback description: > @@ -1258,6 +1702,11 @@ artifacts: - id: LS-S8 type: loss-scenario + links: + - type: caused-by-uca + target: UCA-S9 + - type: leads-to-hazard + target: H-S4 title: Layer 2 misses cross-processor connection scenario-type: inadequate-process-model description: > @@ -1277,6 +1726,13 @@ artifacts: - id: LS-S9 type: loss-scenario + links: + - type: caused-by-uca + target: UCA-S10 + - type: caused-by-uca + target: UCA-S12 + - type: leads-to-hazard + target: H-S9 title: Local optima violate global E2E latency scenario-type: inadequate-control-algorithm description: > @@ -1301,6 +1757,11 @@ artifacts: - id: LS-S10 type: loss-scenario + links: + - type: caused-by-uca + target: UCA-S23 + - type: leads-to-hazard + target: H-S4 title: Virtual bus library understates AFDX worst-case latency scenario-type: inadequate-process-model description: > @@ -1321,6 +1782,11 @@ artifacts: - id: LS-S11 type: loss-scenario + links: + - type: caused-by-uca + target: UCA-S23 + - type: leads-to-hazard + target: H-S7 title: Solver non-determinism from HashMap iteration scenario-type: inadequate-control-algorithm description: > @@ -1341,6 +1807,11 @@ artifacts: - id: LS-S12 type: loss-scenario + links: + - type: caused-by-uca + target: UCA-S11 + - type: leads-to-hazard + target: H-S3 title: DAL-A and DAL-D co-located without partition verification scenario-type: inadequate-control-algorithm description: > @@ -1363,6 +1834,13 @@ artifacts: - id: LS-S13 type: loss-scenario + links: + - type: caused-by-uca + target: UCA-S22 + - type: leads-to-hazard + target: H-S11 + - type: leads-to-hazard + target: H-S2 title: Missing Compute_Execution_Time silently assumed zero scenario-type: inadequate-process-model description: > @@ -1382,6 +1860,11 @@ artifacts: - id: LS-S14 type: loss-scenario + links: + - type: caused-by-uca + target: UCA-S17 + - type: leads-to-hazard + target: H-S6 title: Certificate validates wrong objective function scenario-type: inadequate-control-algorithm description: > @@ -1401,6 +1884,13 @@ artifacts: - id: LS-S15 type: loss-scenario + links: + - type: caused-by-uca + target: UCA-S6 + - type: leads-to-hazard + target: H-S2 + - type: leads-to-hazard + target: H-S9 title: Incremental allocation breaks prior schedulability scenario-type: inadequate-control-algorithm description: > diff --git a/scripts/stpa_migrate_links.py b/scripts/stpa_migrate_links.py new file mode 100755 index 0000000..0867729 --- /dev/null +++ b/scripts/stpa_migrate_links.py @@ -0,0 +1,205 @@ +#!/usr/bin/env python3 +""" +Migrate STPA shorthand fields to canonical `links:` entries. + +Rivet's schema declares link-fields for STPA types (e.g. `uca.controller → +issued-by`, `uca.hazards → leads-to-hazard`). Authors used the shorthand +form (`controller: CTRL-X` at the top level), which rivet's `stpa-yaml` +source format does not expand into the `links:` graph. Result: 625 +cardinality ERRORs in `rivet validate` despite 0 broken cross-refs. + +This script inserts a canonical `links:` block after each artifact's +`type:` line, derived from the shorthand fields. The shorthand fields +themselves are preserved (so authors and the stpa-yaml source format +keep working). After migration, rivet's link-counter sees the explicit +entries and the cardinality errors go to zero. + +Text-based, line-by-line — preserves all comments and formatting. +""" +from __future__ import annotations +import re +import sys +from pathlib import Path + +# Mapping: (artifact_type, shorthand_field) -> canonical link type. +# For scalar shorthand (`controller: CTRL-X`), the value is a single ID. +# For list shorthand (`hazards: [H-1, H-2]`), the value is parsed as a list. +LINK_MAP: dict[tuple[str, str], str] = { + # hazard + ("hazard", "losses"): "leads-to-loss", + # sub-hazard + ("sub-hazard", "parent"): "refines", + # system-constraint + ("system-constraint", "hazards"): "prevents", + # uca + ("uca", "controller"): "issued-by", + ("uca", "hazards"): "leads-to-hazard", + # controller-constraint + ("controller-constraint", "controller"): "constrains-controller", + ("controller-constraint", "ucas"): "inverts-uca", + ("controller-constraint", "hazards"): "prevents", + # loss-scenario + ("loss-scenario", "uca"): "caused-by-uca", + ("loss-scenario", "ucas"): "caused-by-uca", + ("loss-scenario", "hazards"): "leads-to-hazard", + # control-action + ("control-action", "source"): "issued-by", + ("control-action", "target"): "acts-on", +} + +# Fields that carry list values. Others are scalar. +LIST_FIELDS = {"losses", "hazards", "ucas"} + +# Regex: start of an artifact block +RE_ID = re.compile(r'^(?P\s*)- id:\s*(?P\S+)\s*$') +# `type: ` +RE_TYPE = re.compile(r'^(?P\s+)type:\s*(?P\S+)\s*$') +# Scalar field: ` controller: CTRL-X` +RE_SCALAR = re.compile(r'^(?P\s+)(?P[a-z][a-z0-9-]*):\s*(?P[A-Za-z][A-Za-z0-9_-]*)\s*$') +# Inline-list field: ` hazards: [H-1, H-2]` +RE_INLINE_LIST = re.compile(r'^(?P\s+)(?P[a-z][a-z0-9-]*):\s*\[(?P[^\]]*)\]\s*$') +# Block-list field start: ` hazards:` followed by ` - H-1` lines +RE_BLOCK_LIST_HEAD = re.compile(r'^(?P\s+)(?P[a-z][a-z0-9-]*):\s*$') +RE_BLOCK_LIST_ITEM = re.compile(r'^(?P\s+)-\s+(?P[A-Za-z][A-Za-z0-9_-]*)\s*$') +# Existing `links:` block head — if present, skip (already canonical) +RE_LINKS_HEAD = re.compile(r'^(?P\s+)links:\s*$') + + +def parse_list_items(raw: str) -> list[str]: + """Parse the inside of `[a, b, c]` (whitespace-tolerant).""" + return [x.strip() for x in raw.split(",") if x.strip()] + + +def process_file(path: Path) -> tuple[str, int]: + """ + Return (new_text, inserted_link_count). + Inserts a `links:` block after `type:` in each artifact that has + matching shorthand fields AND does not already declare `links:`. + """ + lines = path.read_text().splitlines(keepends=True) + out: list[str] = [] + inserted = 0 + + i = 0 + while i < len(lines): + line = lines[i] + m_id = RE_ID.match(line) + if not m_id: + out.append(line) + i += 1 + continue + + # Found an artifact. Scan to end-of-block (next `- id:` at same + # indent, or next package-level key, or EOF). Inside, find `type:` + # and collect shorthand fields matching the link map. + base_indent = m_id.group("indent") + block_start = i + i += 1 + + type_line_idx: int | None = None + artifact_type: str | None = None + has_links_block = False + collected: list[tuple[str, str]] = [] # (link_type, target_id) + + while i < len(lines): + cur = lines[i] + # Next artifact at same indent — end of this block + next_id = RE_ID.match(cur) + if next_id and next_id.group("indent") == base_indent: + break + # Top-level key (e.g. `artifacts:`, `links:` at file top) at zero indent + if cur and not cur[0].isspace() and cur.strip() and not cur.startswith("#"): + break + + m_type = RE_TYPE.match(cur) + if m_type and type_line_idx is None: + type_line_idx = i + artifact_type = m_type.group("type") + i += 1 + continue + + if RE_LINKS_HEAD.match(cur): + has_links_block = True + + # Shorthand fields — collect if this artifact type maps them + if artifact_type is not None: + m_scalar = RE_SCALAR.match(cur) + if m_scalar: + field = m_scalar.group("field") + if field not in LIST_FIELDS and (artifact_type, field) in LINK_MAP: + link_t = LINK_MAP[(artifact_type, field)] + collected.append((link_t, m_scalar.group("value"))) + + m_inline = RE_INLINE_LIST.match(cur) + if m_inline: + field = m_inline.group("field") + if (artifact_type, field) in LINK_MAP: + link_t = LINK_MAP[(artifact_type, field)] + for v in parse_list_items(m_inline.group("items")): + collected.append((link_t, v)) + + m_blist = RE_BLOCK_LIST_HEAD.match(cur) + if m_blist and (artifact_type, m_blist.group("field")) in LINK_MAP: + link_t = LINK_MAP[(artifact_type, m_blist.group("field"))] + # Walk inline items on subsequent lines + j = i + 1 + while j < len(lines): + m_item = RE_BLOCK_LIST_ITEM.match(lines[j]) + if not m_item: + break + collected.append((link_t, m_item.group("value"))) + j += 1 + + i += 1 + + # Emit the collected lines for this block. If we have collected + # links AND no existing `links:` block, insert after `type:`. + block_end = i # i points at the next block's first line (or EOF) + block = lines[block_start:block_end] + + if collected and not has_links_block and type_line_idx is not None: + # Indent for the inserted `links:` key — same as `type:` indent. + type_indent = RE_TYPE.match(lines[type_line_idx]).group("indent") + item_indent = type_indent + " " # +2 spaces + built = [f"{type_indent}links:\n"] + for link_t, target in collected: + # Block-form flow: rivet's stpa-yaml source expects each + # link as a mapping over two lines, not an inline flow + # mapping. (Semantically equivalent YAML; rivet's parser + # insists on the block form.) + built.append(f"{item_indent}- type: {link_t}\n") + built.append(f"{item_indent} target: {target}\n") + inserted += len(collected) + + # Relative index of the type line inside `block` + rel_type_idx = type_line_idx - block_start + block = ( + block[: rel_type_idx + 1] # everything up to and including `type:` + + built # the new links block + + block[rel_type_idx + 1 :] # rest of the artifact + ) + + out.extend(block) + + return "".join(out), inserted + + +def main() -> int: + root = Path(__file__).resolve().parent.parent + stpa_dir = root / "safety" / "stpa" + files = sorted(stpa_dir.glob("*.yaml")) + total_inserted = 0 + for f in files: + new_text, n = process_file(f) + if n > 0: + f.write_text(new_text) + print(f"{f.relative_to(root)}: +{n} canonical link entries") + total_inserted += n + else: + print(f"{f.relative_to(root)}: unchanged") + print(f"TOTAL: {total_inserted} canonical link entries inserted") + return 0 + + +if __name__ == "__main__": + sys.exit(main())