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

Abstract: 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.