CPS: Synergy: Towards Foundational Verification of Cyber-Physical Systems

网络物理系统中的错误可能会导致灾难性的后果。经典的例子可以追溯到1987年的Therac-25辐射事件和1996年的阿丽亚娜5号火箭坠毁事件。最近，丰田的意外加速漏洞是由软件错误造成的，某些汽车被发现容易受到攻击，这些攻击可能会占领控制软件的关键部分，使得攻击者甚至可以远程禁用刹车。起搏器也被发现容易受到攻击，这些攻击可能会给患者带来致命的后果。为了减少发生这种错误的机会，这个项目调查了一种名为基础验证的技术在网络物理系统中的应用。在基础验证中，正在开发的系统使用证明助手被证明是正确的、完全正式的细节。该提案的主要学术价值是达到了以前无法达到的网络物理系统的安全水平，因为基础核查中的证明是完全详细地进行的。为了确保该项目中的技术是实用的，它们是在真实的飞行四轴飞行器的背景下进行评估的。该项目更广泛的意义和重要性是提高了网络物理系统的正确性、安全性和安全性。特别是，该项目为网络物理系统引入新的形式正确性奠定了基础。尽管最初的工作重点是四轴飞行器，但其概念、想法和研究贡献可能会对其他类型的系统产生革命性影响，包括电网软件、汽车、航空电子设备和医疗设备(从起搏器和胰岛素泵到除颤器和辐射机)。

Errors in cyber-physical systems can lead to disastrous consequences. Classic examples date back to the Therac-25 radiation incidents in 1987 and the Ariane 5 rocket crash in 1996. More recently, Toyota's unintended acceleration bug was caused by software errors, and certain cars were found vulnerable to attacks that can take over key parts of the control software, allowing attackers to even disable the brakes remotely. Pacemakers have also been found vulnerable to attacks that can cause deadly consequences for the patient. To reduce the chances of such errors happening, this project investigates the application of a technique called Foundational Verification to cyber-physical systems. In Foundational Verification, the system being developed is proved correct, in full formal detail, using a proof assistant. The main intellectual merit of the proposal is the attainment of previously unattainable levels of safety for cyber-physical systems because proofs in Foundational Verification are carried out in complete detail. To ensure that the techniques in this project are practical, they are evaluated within the context of a real flying quadcopter. The project's broader significance and importance is the improved correctness, safety and security of cyber-physical systems. In particular, this project lays the foundation for ushering in a new level of formal correctness for cyber-physical systems. Although the initial work focuses on quadcopters, the concepts, ideas, and research contributions have the potential for transformative impact on other kinds of systems, including power-grid software, cars, avionics and medical devices (from pacemakers and insulin pumps to defibrillators and radiation machines).