We propose extensions to the Dolev-Yao attacker model to make it suitable for arguments about security of Cyber-Physical Systems. The Dolev-Yao attacker model uses a set of rules to define potential actions by an attacker with respect to messages (i.e. information) exchanged between parties during a protocol execution. The model can be used to argue about the security of such protocols (e.g., using model checking). As the traditional Dolev-Yao model considers only information (exchanged over a channel controlled by the attacker), the model cannot directly be used to argue about the security of cyber-physical systems where physical-layer interactions are possible. In this work, we propose a cyber-physical Dolev-Yao (CPDY) attacker model, a general extension of the Dolev-Yao model to allow additional orthogonal interaction channels between the parties. In particular, such orthogonal channels can be used to model physical-layer mechanical, chemical, or electrical interactions between components. In addition, we discuss the inclusion of physical properties such as location or distance in the rule set. We present an example set of additional rules for the Dolev-Yao attacker, using those we are able to formally discover physical attacks that previously could only be found by empirical methods or detailed physical process models.
The formal verification of security properties of CPS is a non trivial task, as CPS introduce physical properties to the system under analysis. SAT SMT solvers used by security analysis tools (e.g., @cite_28 ) do not support such properties. In order to overcome this limitation, one could simulate the process (e.g., @cite_7 ) or adapt the level of abstraction of CPS components. @cite_9 , the author presents a formal definition of an attacker model for CPS. The attacker is defined as a set of pairs representing locations and capabilities. Capabilities are defined as a set of tuples expressing actions, cost (energy time) and range (with respect to the topology) of the attacker. The attacker is assumed to perform two types of attacks: , against a device and against the communications; where the first requires physical access while the second proximity to the node. The actions of the attacker are (remove, read write, reveal, reprogram, starve) and (block, eavesdrop, inject).
@cite_28 @cite_9 @cite_7
1782799247 2952719762
The AVANTSSAR Platform is an integrated toolset for the formal specification and automated validation of trust and security of service-oriented architectures and other applications in the Internet of Services. The platform supports application-level specification languages (such as BPMN and our custom languages) and features three validation backends (CL-AtSe, OFMC, and SATMC), which provide a range of complementary automated reasoning techniques (including service orchestration, compositional reasoning, model checking, and abstract interpretation). We have applied the platform to a large number of industrial case studies, collected into the AVANTSSAR Library of validated problem cases. In doing so, we unveiled a number of problems and vulnerabilities in deployed services. These include, most notably, a serious flaw in the SAML-based Single Sign-On for Google Apps (now corrected by Google as a result of our findings). We also report on the migration of the platform to industry. In recent years, tremendous effort has been spent to modernizing communication infrastructure in Cyber-Physical Systems (CPS) such as Industrial Control Systems (ICS) and related Supervisory Control and Data Acquisition (SCADA) systems. While a great amount of research has been conducted on network security of office and home networks, recently the security of CPS and related systems has gained a lot of attention. Unfortunately, real-world CPS are often not open to security researchers, and as a result very few reference systems and topologies are available. In this work, we present MiniCPS, a CPS simulation toolbox intended to alleviate this problem. The goal of MiniCPS is to create an extensible, reproducible research environment targeted to communications and physical-layer interactions in CPS. MiniCPS builds on Mininet to provide lightweight real-time network emulation, and extends Mininet with tools to simulate typical CPS components such as programmable logic controllers, which use industrial protocols (Ethernet IP, Modbus TCP). In addition, MiniCPS defines a simple API to enable physical-layer interaction simulation. In this work, we demonstrate applications of MiniCPS in two example scenarios, and show how MiniCPS can be used to develop attacks and defenses that are directly applicable to real systems.