Most proposals for securing control systems are heuristic in nature, and while they increase the protection of their target, the security guarantees they provide are unclear. This paper proposes a new way of modeling the security guarantees of a Cyber-Physical System (CPS) against arbitrary false command attacks. As our main case study, we use the most popular testbed for control systems security. We first propose a detailed formal model of this testbed and then show how the original configuration is vulnerable to a single-actuator attack. We then propose modifications to the control system and prove that our modified system is secure against arbitrary, single-actuator attacks.

Industrial Control Systems (ICS) implement a distributed process control framework with legacy controllers and proprietary protocols, enabling a wide range of cyber-attacks. The ICS research community and industrial security practitioners recommend implementing TLS/DTLS or bump-in-the-wire techniques for communicating confidential information. In this paper, we discuss how such techniques fail to provide the purpose-built security required in control applications. We examine the proprietary application-layer protocols and how they access the controller memory for performing read/write operations and claim that custom-made ICS security solutions require application-level access to the controller. To this end, we propose SelEnc, a general-purpose modular framework for securely communicating a subset of control information, deemed critical by the process engineer of a controlled environment, with minimal access to the controller memory. We provide a proof-of-concept implementation of the proposed framework over an example testbed and evaluate our construction with two use cases and five different datasets. Our micro-benchmarks indicate a significant reduction in computational overhead (less than 1.5% of overhead incurred due to TLS and other state-of-art approaches), with guarantees of purpose-built security acknowledged at the target control environment.

To protect an Industrial Control System (ICS), defenders need to identify potential attacks on the system and then design mechanisms to prevent them. Unfortunately, identifying potential attack conditions is a time-consuming and error-prone process. In this work, we propose and evaluate a set of tools to symbolically analyse the software of Programmable Logic Controllers (PLCs) guided by an information flow analysis that takes into account PLC network communication (compositions). Our tools systematically analyse malicious network packets that may force the PLC to send specific control commands to actuators. We evaluate our approach in a real-world system controlling the dosing of chemicals for water treatment. Our tools are able to find 75 attack tactics (56 were novel attacks), and we confirm that 96% of these tactics cause the intended effect in our testbed.

In modern societies, critical services such as transportation, power supply, water treatment and distribution are strongly dependent on Industrial Control Systems (ICS). As technology moves along, new features improve services provided by such ICS. On the other hand, this progress also introduces new risks of cyber attacks due to the multiple direct and indirect dependencies between cyber and physical components of such systems. Performing rigorous security tests and risk analysis in these critical systems is thus a challenging task, because of the non-trivial interactions between digital and physical assets and the domain-specific knowledge necessary to analyse a particular system. In this work, we propose a methodology to model and analyse a System Under Test (SUT) as a data flow graph that highlights interactions among internal entities throughout the SUT. This model is automatically extracted from production code available in Programmable Logic Controllers (PLCs). We also propose a reachability algorithm and an attack diagram that will emphasize the dependencies between cyber and physical domains, thus enabling a human analyst to gauge various attack vectors that arise from subtle dependencies in data and information propagation. We test our methodology in a functional water treatment testbed and demonstrate how an analyst could make use of our designed attack diagrams to reason on possible threats to various targets of the SUT.