CPS: Medium: Quantitative Contract-Based Synthesis and Verification for CPS Security

网络物理系统(CP)部署在安全关键型和任务关键型应用程序中，这些应用程序的设计主要考虑安全问题。同时，这些系统的设计必须更加灵活，以适应不断变化的要求和环境条件。该项目致力于CPS设计新方法的基础性工作，以实现“即插即用”方法，从设计阶段就确保系统的安全性和安全性。这种原则性的设计方法可以对新兴的国家“智能”基础设施产生巨大的积极影响。通过与行业合作伙伴的合作，该项目旨在改善CPS行业的设计流程，特别是汽车系统。此外，这个项目计划将研究整合到本科生和研究生的课程工作中，特别是顶石项目，并将对研究人员开发的教科书和在线课程内容产生影响。该项目为基于合同的量化CPS设计开发了一个全新的理论，它平衡了安全要求与关键的安全和性能问题。这一理论满足了工业网络物理系统面临的迫切需求，工业网络物理系统正因推动“即插即用”设计架构而发生转变。这一努力往往会颠覆CPS的设计流程，带来对安全和隐私的新担忧。该方法包括以下几个关键部分：(I)为新的量化时态逻辑中的每个“插件”组件提供精确的接口规范；(Ii)用于检查组件是否符合规范的快速、运行时验证方法；以及(Iii)一种在满足性能和安全规范的同时将组件映射到现有体系结构并最小化成本的新方法。该方法将在工业汽车的背景下开发和评估。提出的严格的基于逻辑的形式主义，在验证和综合方面的算法进步的支持下，有可能创造新的基础科学，并帮助将工业趋势推向即插即用架构的坚实基础。

Cyber-physical systems (CPS) are deployed in safety-critical and mission-critical applications for which security is a primary design concern. At the same time, these systems must be designed to be more flexible to changing requirements and environment conditions. This project pursues foundational work on a new methodology for CPS design to enable a "plug-and-play" approach that also ensures the security and safety of the system from the design phase. Such a principled design approach can have an enormous positive impact on the emerging national "smart" infrastructure. Through collaborations with industry partners, the project aims to improve the design process in the CPS industry with a particular focus on automotive systems. Additionally, this project plans to integrate research into undergraduate and graduate coursework, especially capstone projects, and will have an impact on the textbooks and online course content developed by the researchers.This project develops a fundamentally new theory for quantitative contract-based design of CPS that balances security requirements with critical safety and performance concerns. This theory meets a pressing need faced by industrial cyber-physical systems, which are being transformed by a push towards "plug-and-play" design architectures. This push tends to upend the design process for CPS, bringing with it renewed concerns about security and privacy. The proposed approach has the following key components: (i) a precise interface specification for each "plug-in" component in a novel quantitative temporal logic; (ii) rapid, run-time verification methods for checking component conformance to specifications, and (iii) A new approach for mapping components onto existing architectures while satisfying performance and security specifications, and minimizing costs. The approach will be developed and evaluated in an industrial automotive context. The proposed rigorous logic-based formalism, backed by algorithmic advances in verification and synthesis, has the potential to create new fundamental science and help put the industrial trend towards plug-and-play architectures on a firm footing.