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

CPS：协同：迈向网络物理系统的基础验证

• 批准号: 1544757
• 负责人: Sorin Lerner
• 金额: $ 70万
• 依托单位: University of California-San Diego
• 依托单位国家: 美国
• 项目类别: Standard Grant
• 财政年份: 2015
• 资助国家: 美国
• 起止时间: 2015-10-01 至 2019-09-30
• 项目状态: 已结题
• 来源: https://www.nsf.gov/awardsearch/showAward?AWD_ID=1544757&HistoricalAwards=false
• 关键词: CPS; Synergy; Towards; Foundational; Verification

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).

网络物理系统中的错误可能导致灾难性后果。经典示例可以追溯到1987年的Therac-25辐射事件和1996年的Ariane 5火箭崩溃。最近，丰田的意外加速错误是由软件错误引起的，某些汽车很容易受到可能接管控制软件的关键部分的攻击，从而使攻击者甚至可以远离制动器。还发现起搏器容易受到可能对患者造成致命后果的攻击。为了减少发生此类错误的机会，该项目研究了一种称为基础验证的技术在网络物理系统中的应用。在基础验证中，使用证明助手完全详细地进行了正式详细的证明，开发的系统被证明是正确的。该提案的主要智力优点是获得了以前无法实现的网络物理系统安全性水平，因为基础验证中的证明是完整的。为了确保该项目中的技术是实用的，可以在真正的飞行四轮驱动器的背景下进行评估。该项目的重要性和重要性是网络物理系统的正确性，安全性和安全性。特别是，该项目奠定了为网络物理系统建立新的正式正确性水平的基础。尽管最初的工作着重于四型四型，但概念，思想和研究贡献具有对其他类型系统的变革性影响，包括动力网软件，汽车，航空电子和医疗设备（从起搏器和胰岛素泵到除颤器和放射线机器）。