We present a new generalization of (zk-)SNARKs specifically designed for the application domain of safety-critical control systems. These need to be protected against adversarial tampering as well as non-malicious but unintended system failures due to random faults in components. Our SNARKs combine two additional features at the same time. Besides the verification of correct computation, they also allow, first, the verification of input data authenticity. Specifically, a verifier can confirm that the input to the computation originated from a trusted source. Second, our SNARKs support verification of stateful computations across multiple rounds, ensuring that the output of the current round correctly depends on the internal state of the previous round. Our focus is on concrete practicality, so we abstain from arithmetizing hash functions or signatures in our SNARKs. Rather, we modify the internals of an existing SNARK to extend its functionality. We implement and benchmark our new SNARKs in a sample scenario of a real-time high-integrity flight control system.
With our construction, prover runtime improves significantly over the baseline by a factor of 90. Verification time increases by 36%, but is less than comparable approaches that do not arithmetize hash functions or signatures.
Interesting paper co-authored by Airbus cryptographer Erik-Oliver Blass on using zero-knowledge proofs in flight control systems.
Sensors would authenticate their measurements, the control unit provides in each iteration control outputs together with a proof of output correctness (reducing the need in some cases for redundant computations),
and actuators verify that outputs have been correctly computed