Search for: All records

A water treatment center (WTC) removes contaminants and unwanted components from the water and makes the water more acceptable to the end-users. A modern WTC is equipped with different water sensors and uses a combination of wired/wireless communication network. During the water treatment process, controllers periodically collect sensor measurements and make important operational decisions. Since accuracy is vital, a WTC also uses different data validation mechanisms to validate the incoming sensor measurements. However, like any other cyber-physical system, water treatment facilities are prone to cyberattacks and an intelligent adversary can alter the sensors measurements stealthily, and corrupt the water treatment process. In this work, we propose WTC Checker (WTC2), an impact-aware formal analysis framework that demonstrates the impact of stealthy false data injection attacks on the water treatment sensors. Through our work, we demonstrate that if an adversary has sufficient access to sensor measurements and can evade the data validation process, he/she can compromise the sensors measurements, change the water disinfectant contact time, and inflict damage to the clean water production process. We model this attack as a constraint satisfaction problem (CSP) and encode it using Satisfiability Modulo Theories (SMT). We evaluate the proposed framework for its threat analysis capability as well as its scalability by executing experiments on different synthetic test cases. 

The supervisory control and data acquisition (SCADA) network in a smart grid requires to be reliable and efficient to transmit real-time data to the controller. Introducing SDN into a SCADA network helps in deploying novel grid control operations, as well as, their management. As the overall network cannot be transformed to have only SDN-enabled devices overnight because of budget constraints, a systematic deployment methodology is needed. In this work, we present a framework, named SDNSynth, that can design a hybrid network consisting of both legacy forwarding devices and programmable SDN-enabled switches. The design satisfies the resiliency requirements of the SCADA network, which are specified with respect to a set of identified threat vectors. The deployment plan primarily includes the best placements of the SDN-enabled switches. The plan may include one or more links to be installed newly. We model and implement the SDNSynth framework that includes the satisfaction of several requirements and constraints involved in the resilient operation of the SCADA. It uses satisfiability modulo theories (SMT) for encoding the synthesis model and solving it. We demonstrate SDNSynth on a case study and evaluate its performance on different synthetic SCADA systems.