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.