VeritAS

Computers and software that implement flight control tasks in aircraft must meet the highest safety requirements, as human lives depend on their correct functioning. Faulty flight computers must be identified and deactivated within the shortest possible time to prevent error propagation with fatal consequences. Previous solutions to ensure the integrity of such systems are based on computer replicas: the control function is executed in parallel on several computers (replicas), which compare each other to detect discrepancies. The realization of this solution is technically complex: The computers have to be synchronized in an elaborate way and have to show consensus between input and intermediate results. This is enforced by elaborate algorithms, losing a lot of computing time and bandwidth. In addition, computers and software usually need to be similar to be comparable. Thus, errors that are present in the replicated computers in the same way (common-mode errors) are likely. Overall, fault tolerance of computer systems and the proof of it is the main cost driver of flying computer systems. No small aircraft today has a safety-critical, all-digital flight control system! In the large aircraft sector, about 100 M€ are spent on the development and certification of digital flight control.

A new branch of research from cryptography suggests that a disruptively different solution for security-critical systems is possible: What if a computer can verifiably and non-falsifiably prove that it has performed its task correctly? That is, in addition to the result of the control function, a computer produces a proof, which can be quickly verified by a verifier algorithm, that it has correctly processed the expected task (an algorithm implemented in software). The proof is tamper-proof, meaning that a faulty computer is not able to generate a valid proof for an incorrectly performed computation due to a hardware or software error. The verification of the proof is so simple that a very small computer is sufficient to perform it. Such a solution, if applicable, would represent a radical paradigm shift for safety-critical computing systems. Synchronization, consensus, and other requirements imposed by the replica method are eliminated. New, more compact, lighter-weight safety-critical system architectures will be possible, and proving correctness will be easier. Even more, functions could be implemented in a safety-critical manner where this is not possible today due to their complexity, e.g. advanced artificial intelligence algorithms such as image recognition.

The proposed concept can be made possible by enormous progress in the last 8 years in the methods of Verifiable Computing. A number of algorithms have been developed that allow proving and verifying the correctness of computations without having executed them themselves. There are initial applications in the areas of cryptocurrencies and blockchain. The possibilities of Verifiable Computing for safety-critical real-time systems are very promising but have not been explored so far. We would like to fill this gap in VeritAS and answer the following research questions:

1. What is the actual potential of current verifiable computing methods in terms of the complexity of verifiable algorithms (prover) and the effort of verification (verifier)?
2. What new safety-critical system architectures are technically feasible, what do they look like, and how should they be evaluated in terms of effort and benefits?
3. Are there requirements for Verifiable Computing in avionics systems that are not yet feasible - both in terms of technical feasibility and applicable certification requirements?

To answer this question, a demonstrator has been developed at ILS that includes the first real-time verifiable control algorithm for a simplified elevator control system.