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 critical 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.

Optimal Power Flow (OPF) is a crucial part of the Energy Management System (EMS) as it determines individual generator outputs that minimize generation cost while satisfying transmission, generation, and system level operating constraints. OPF relies on a core EMS routine, namely state estimation, which computes system states, principally bus voltages/phase angles at the buses. However, state estimation is vulnerable to false data injection attacks in which an adversary can alter certain measurements to corrupt the estimator's solution without being detected. It is also shown that such a stealthy attack on state estimation can increase the OPF cost. However, the impact of stealthy attacks on the economic and secure operation of the system cannot be comprehensively analyzed due to the very large size of the attack space. In this paper, we present a hybrid framework that combines formal analytics with Simulink-based system modeling to investigate the feasibility of stealthy attacks and their influence on OPF in a time-efficient manner. The proposed approach is illustrated on synthetic case studies demonstrating the impact of stealthy attacks in different attack scenarios. We also evaluate the impact analysis time by running experiments on standard IEEE test cases and the results show significant scalability of the framework.

Car manufacturers are investing heavily in Autonomous Vehicles (AVs) because of their increasing popularity. AVs employ a combination of high-tech sensors and innovative algorithms to detect and respond to their surroundings, including radar, laser light, GPS, odometer, drive-by-wire control systems, and computer vision. When a user requests for a ride share or rent, the responding AV/IoT device does not have the sufficient capability to store, process, or verify each other. Currently, every AV/IoT device typically needs to rely on a trusted third party, which invokes another trust issue. If the trusted third party is rogue or loses credibility, the whole system will collapse. This paper introduces Chained of Things Framework and develops a blockchain-based secure ride-sharing service between passengers and autonomous vehicles. We implement an initial prototype and provide our initial results based on a proposed protocol.