CPS: Breakthrough: Cyber-Physical System Securitization by Responsibility Analysis

程序描述了由计算机执行的一系列动作。不幸的是，程序员会犯错误，攻击者会利用这些错误来转移程序操作的注意力。因此，必须检查程序操作以确保始终安全可靠。程序安全从定义哪些操作可能不安全以及它们何时是坏的开始。出于安全考虑，不安全的行为不能总是被禁止。这个项目正式确立了责任分析的概念。责任分析旨在自动确定哪些程序实体导致不良不安全行为的发生。这可以通过只检查程序文本来实现，因为该文本准确地描述了以后运行程序时可能发生的所有操作。基于程序的操作语义，该项目正式地将语义责任定义为定位不良行为的可能来源的最精确的方法。通过对这种操作语义的抽象解释，在传统的C程序安全分析的基础上，将设计一个合理的静态责任分析。将建立一个原型静态责任分析器，以检查网络物理系统的安全性(给定不良行为和安全策略)。分析结果将用于检查是否所有对不良行为负责的实体都得到了适当授权(或安全政策是错误的)。该工具将帮助程序员在程序设计时合理地修复潜在的漏洞，而不是在检测到对程序的攻击后进行现代的事后补救。这将是网络安全、隐私和网络物理系统融合的一个突破。

Programs describe successions of actions to be performed by computers. Unfortunately programmers make errors which are exploited by attackers to divert program actions from their goals. Accordingly, program actions must be checked to be always safe and secure. Program security starts with the definition of which actions might be insecure and when they are bad. Insecure actions cannot be always forbidden as for safety. This project formalizes the concept of responsibility analysis. Responsibility analysis aims at determining automatically which program entities cause bad insecure actions to happen. This is possible by examining the program text only, because this text precisely describes all possible actions that can happen when later running a program. Based on an operational semantics of programs, the project formally defines semantic responsibility as the most precise way of locating the possible origin of bad actions. A sound static responsibility analysis will be designed by abstract interpretation of this operational semantics, on top of traditional safety analyses of C programs. A prototype static responsibility analyzer will be built to check for the security of cyber-physical systems (given bad actions and a security policy). The result of the analysis will be used to check that all entities responsible for bad actions are duly authorized (or the security policy is wrong). This tool will help programmers to soundly cure potential vulnerabilities at program design time as opposed to present-day post-mortem remedies after those attacks on programs that get detected. This would be a breakthrough at the confluence of cyber security, privacy, and cyber-physical systems.