Shield Synthesis: Runtime Enforcement for Reactive Systems

2 min read

Bloem and colleagues synthesise a “shield” that sits on the outputs of a reactive hardware design and corrects them, without delay, so that a small set of critical safety properties always holds. The design itself is a black box (a third-party IP core, or something too big to model check). The shield must correct in the same clock tick, it may not halt or insert steps, and it should deviate as little as possible. Their notion of k-stabilisation bounds the recovery: after a forced deviation the shield may differ from the design for at most k consecutive steps; a second violation inside that window drops it into a fail-safe mode that only enforces correctness. The synthesis reduces to safety games solved with BDDs.

Findings

  • Traffic light controller with two injected bugs (skipping the all-red phase; only the highway turns red for an emergency vehicle): a 1-stabilising shield, synthesised in a fraction of a second, fixes both, 5 latches and 41 AIG gates after ABC optimisation.
  • ARM AMBA bus arbiter: two guarantees take 0.1 s, four guarantees (G1+2+3+5) take 242 s, and several three- and four-guarantee combinations time out after 3600 s. Synthesis time grows fast with the property set.
  • LTL specification patterns (Dwyer et al.), with liveness turned into bounded response: most take under 0.4 s. A bounded-until pattern with bound 16 took 377 s and gave a shield of 18 latches and 13140 AIG gates.

Limits

  • Only safety properties. Liveness (“the request is eventually granted”) is out of scope.
  • The shield trusts the inputs it sees. It guards a design against its own bugs, and a lying sensor upstream is invisible to it.
  • The tool is a proof of concept with explicit-state steps, and the authors leave scaling optimisations to future work.

Relevance

The idea of a bounded recovery phase followed by a fail-safe mode is a formal version of what robot safety state machines do informally. It is the ancestor of shielded RL and a cousin of Simplex; see runtime monitoring and failure recovery. An open question for robust robotics: what should k be for a robot that has to keep moving.