Vérification et sûreté › Sûreté et cybersécurité

Vérification et sûreté

Cette page n’est pas encore traduite : voici la version anglaise.

Safety and cybersecurity: STPA, error propagation, TARA

The safety analysis (error propagation, fault trees, STPA) and the cybersecurity risk assessment (ISO/SAE 21434) archec makes from the model.

Safety: error propagation and STPA#

A part says what errors it makes and what becomes of the errors that reach it (the idea of AADL's error model annex); the links carry them. archec derives each hazard's fault tree and an FMEA row per error source from it, and checks them against the ones written by hand:

component Sensor { out speed: can sends SPEED { produces omission, value } }
component Ctrl {
  in left: can receives SPEED { contains late; turns value into omission }
  in right: can receives SPEED { turns value into omission }
  out cmd: can sends CMD { from-all left, right }   // redundant: both must fail
}
failure-mode FM-S1 "Sensor 1 dead" { of Car.s1; produces omission; probability 1e-5 }
hazard HZ-01 "No braking on demand" { …; error omission on Car.brakes.cmd; caused-by FM-CTRL, G-SENSORS }
  • Error types: omission, commission, value, early, late. produces on an output is an error source; a failure-mode with of and produces rates it (probability). contains on an input stops errors (all: every type), turns a into b changes their type. An output takes the errors of every input, or of those from names; from-all is an AND.
  • Derived: each hazard with error … on … gets a fault tree, its minimal cut sets and its rate (1 − ∏(1 − ∏ p) over the cut sets); each source an FMEA row — where its error goes, and the hazards it leads to. They are marked derived in archec safety, the LaTeX and HTML specification and the editor.
  • Checks: a written tree (caused-by, gates) with other cut sets than the derived one (fta-mismatch), a failure mode whose causes are not the hazards its error reaches (fmea-mismatch), a hazard no error reaches (error-unreached), unknown error types.

STPA (Leveson's analysis, as Gaphor's RAAML writes it) uses the architecture as its control structure: a control action goes from a controller part to the part it controls, over the links, and feedback comes back.

control-action CA-BRAKE "Apply the brakes" {
  from Car.adcu
  to Car.brakes
  carries BRAKE_CMD
  feedback WHEEL_SPEED
  not-applicable duration
  because "The brakes release on their own when the command stops."
  uca UCA-1 "No braking with an obstacle ahead" {
    type not-provided
    causes HZ-01
    constraint REQ-SAF-1
    loss-scenario LS-1 "The radar misses it in heavy rain" { factor feedback; constraint REQ-SAF-2 }
  }
}
  • The four types: not-provided, provided (causing a hazard), timing (too early, too late, out of order), duration (stopped too soon, applied too long).
  • Checks: each control action considered for the four types, or said not-applicable (stpa-incomplete); each UCA leads to a hazard and is prevented by a constraint, a requirement (uca-untraced); a link carries the action from the controller to the process, and the feedback back (stpa-no-path); a UCA with no loss scenario is a hint.
  • archec safety main.arche [--json] prints the hazards, the derived trees and FMEA, and the STPA tables (exit 1 on a mismatch or an STPA gap); the LaTeX and HTML specification have them in their Safety section, and the editor's model tree under Safety.

Cybersecurity (TARA)#

A threat analysis and risk assessment after ISO/SAE 21434, next to the safety analysis:

asset AS-BRAKE "Brake commands" { of Car.adcu.can_brake; properties integrity, availability }
damage-scenario DS-BRAKE "Full braking on the motorway" { asset AS-BRAKE; property integrity; safety severe }
threat TS-SPOOF "Spoofed brake commands" { damages DS-BRAKE; stride spoofing; via Car.chassis_can; vector adjacent; treatment reduce; goal CSG-01 }
attack-path AP-OBD "From the OBD port" { threat TS-SPOOF; elapsed week; expertise proficient; knowledge restricted; window moderate; equipment standard }
security-goal CSG-01 "Brake commands are authentic" { text "…"; answers TS-SPOOF }
  • Feasibility of an attack path: the attack-potential points (annex G) — 0–9 high, 10–13 medium, 14–19 low, 20+ very low; a threat takes its easiest path.
  • Risk (1–5): impact (the worst rating of what it damages) by feasibility. CAL: impact by attack vector. Both use the standard's example tables.
  • Checks: a risk of 4 or 5 with no treatment, reduce with no security goal, retain/share with no claim, a goal's CAL lower than its threats need, unrated paths and damage scenarios (security-risk, cal-too-low, tara-incomplete).
  • archec tara main.arche [--json] prints the table (exit 1 on an untreated risk of 4 or 5); the LaTeX specification has a TARA section. Security goals are Arche requirements of category security; the rest is archec's (Arche has no place for it yet).