CPS: Small: Reconciling Safety with the Internet for Cyber-Physical Systems

Internet技术最初是为了传递信息而开发的，现在越来越多地用于控制和操作家庭、工厂、医疗设施和运输系统中的物理设备，这只是几个应用领域。在这些更基于物理的应用程序中，系统行为不当的后果可能是可怕的，不仅涉及信息丢失或泄漏，还涉及生命损失。从历史上看，用于安全关键系统的计算机已经完全与互联网隔离，以保护它们免受恶意黑客和对其资源的不可预测的需求。但是，互联网连接带来的好处是不可抗拒的，它使更复杂的服务成为可能。该项目正在开发一套基于数学的设计模式和开源软件，这些软件利用互联网技术，同时保证安全性、可靠性和对恶意攻击的弹性。其中一种模式赋予网络系统更强的协调时间概念，以确保系统的行为一致，即使面对网络中不可预测和不可控的延迟。另一种模式利用边缘计算，将计算服务放置在使用它们的设备附近，例如在医院、汽车和火车上以及工厂中，以减轻依赖基于云的远程服务的风险。即使互联网基础设施崩溃，边缘计算机也能保证持续安全运行，就像偶尔发生的恶意攻击一样。技术描述：物联网（IoT）在网络物理系统中利用互联网技术，但互联网的协议和原则不是为与物理世界交互而设计的。例如，在任何广泛的互联网技术中，及时性都不是一个因素，服务质量（QoS）特性几十年来一直被例行公事地忽略。尽管如此，互联网的属性在CPS中可能被证明是有价值的，包括全局命名空间、可靠的（最终的）消息传递、通过非对称加密实现的端到端安全性、基于证书的身份验证，以及在基于云的仓库中聚合来自多个来源的数据的能力。该提案利用了最近的发展，有望弥合这一差距，甚至可以在工厂自动化和运输等安全关键、时间敏感的应用中使用互联网技术。具体来说，我们利用时间敏感网络（TSN）技术；使用智能网关将安全关键服务与尽力而为的服务隔离开来，并为基于云的服务提供本地代理；本地集中式、全球分布式认证授权；以及分布式实时服务中基于时间的连贯语义的发展。这个项目的重点将放在可靠的并发计算模型，确保正确组合的类型理论方法，以及在软件体系结构中实现这些形式化的方法，该软件体系结构将Internet服务中广泛使用的隐藏不可控延迟的机制与安全关键系统中可重复、可测试和健壮的实时服务的需求协调起来。一个开源的参考实现将与关于模型形式属性的分析论文一起交付。该奖项反映了美国国家科学基金会的法定使命，并通过使用基金会的知识价值和更广泛的影响审查标准进行评估，被认为值得支持。

Internet technology, originally developed to convey information, is increasingly being used to control and operate physical devices in homes, factories, medical facilities, and transportation systems, to name just a few application domains. In these more physically-grounded applications, the consequences of misbehavior of a system can be dire, involving not just loss or leakage of information, but loss of life. Historically, computers used in safety-critical systems have been completely isolated from the Internet to protect them from malicious hackers and unpredictable demands for their resources. But the benefits that Internet connectivity offers are irresistible, enabling far more sophisticated services. This project is developing a suite of mathematically-grounded design patterns and open-source software that leverages Internet technology while guaranteeing safety, reliability, and resilience to malicious attacks. One of these patterns endows a networked system with a stronger coordinated notion of time to ensure consistent behavior of the system even in face of unpredictable and uncontrollable delays in the network. Another of these patterns leverages edge computing, placement of computing services near the devices that use them, in hospitals, onboard in cars and trains, and in factories, for example, to mitigate the risks of relying on remote cloud-based services. Edge computers can ensure continuous safe operation even in face of Internet infrastructure collapse, as has occasionally happened under malicious attack.Technical Description:The Internet of Things (IoT) leverages Internet technology in cyber-physical systems, but the protocols and principles of the Internet were not designed for interacting with the physical world. For example, timeliness is not a factor in any widespread Internet technology, with Quality-of-Service (QoS) features having been routinely omitted for decades. Nevertheless, properties of the Internet could prove valuable in CPS, including a global namespace, reliable (eventual) delivery of messages, end-to-end security through asymmetric encryption, certificate-based authentication, and the ability to aggregate data from a multiplicity of sources in cloud-based warehouses. This proposal leverages recent developments that hold promise to bridge the gap, enabling the use of Internet technologies even in safety-critical, timing-sensitive applications such as factory automation and transportation. Specifically, we leverage time-sensitive network (TSN) technology; the use of smart gateways to isolate safety-critical services from best-effort services and to provide local proxies for cloud-based services; locally centralized, globally distributed authentication and authorization; and the development of coherent time-based semantics for distributed real-time services. The focus of this project will be on sound concurrent models of computation, on type-theoretic methods for ensuring correct composition, and on the realization of these formalisms in a software architecture that reconciles widely-used mechanisms in Internet services to hide uncontrollable latencies with the need for repeatable, testable, and robust real-time services in safety-critical systems. An open-source reference implementation will be delivered together with analytical papers on the formal properties of the models.This award reflects NSF's statutory mission and has been deemed worthy of support through evaluation using the Foundation's intellectual merit and broader impacts review criteria.