ABSTRACT. In this paper, we demonstrate the feasibility of a smart malware that advances the state-of-the-art attacks by: (i) indirectly attacking a computing infrastructure through a cyber-physical system (CPS) that manages the environment in which the computing enterprise operates, (ii) disguising its malicious actions as accidental failures, and (iii) self-learning attack strategies from cyber-physical system measurement data. We address the full range of issues, including the construction of the self-learning malware and the launch of a failure injection attack. We validate the attacks in a data-driven CPS simulation environment developed as part of this study.

ABSTRACT. An Implantable Cardioverter Defibrillator (ICD) is a medical device used for the detection of potentially fatal cardiac arrhythmias and their treatment through the delivery of electrical shocks intended to restore normal heart rhythm. An ICD reprogramming attack seeks to alter the device's parameters to induce unnecessary therapy or prevent required therapy. In this paper, we present a formal approach for the synthesis of ICD reprogramming attacks that are both effective, i.e., lead to fundamental changes in the required therapy, and stealthy, i.e., are hard to detect. We focus on the discrimination algorithm underlying Boston Scientific devices (one of the principal ICD manufacturers) and formulate the synthesis problem as one of multi-objective optimization. Our solution technique is based on an Optimization Modulo Theories encoding of the problem and allows us to derive device parameters that are optimal with respect to the effectiveness-stealthiness tradeoff. Our method can be tailored to the patient's current condition, and readily generalizes to new rhythms. To the best of our knowledge, our work is the first to derive systematic ICD reprogramming attacks designed to maximize therapy disruption while minimizing detection.

ABSTRACT. Nowadays, the interconnection of automotive systems with modern digital devices offers advanced user experiences to drivers. Electronic Control Units (ECUs) carry out a multitude of operations using the insecure Controller Area Network (CAN) bus in automotive Cyber-Physical Systems (CPS). Therefore, dangerous attacks, such as disabling brakes, are possible and the safety of passengers is at risk. In this paper, we present TACAN (Transmitter Authentication in CAN), which provides secure authentication of ECUs by exploiting the covert channels without introducing CAN protocol modifications or traffic overheads. TACAN turns upside-down the originally malicious concept of covert channels and exploits it to build an effective defensive technique that facilitates transmitter authentication via a trusted Monitor Node. TACAN consists of three different covert channels for ECU authentication: 1) Inter- Arrival Time (IAT)-based, leveraging the IATs of CAN messages; 2) offset-based, exploiting the clock offsets of CAN messages; 3) Least Significant Bit (LSB)-based, concealing authentication messages into the LSBs of normal CAN data. We implement the covert channels of TACAN on the University of Washington (UW) EcoCAR testbed and evaluate their performance through extensive experiments using real vehicle datasets. We demonstrate the effectiveness of TACAN, highlighting no traffic overheads and attesting the regular functionality of ECUs. In particular, the bit error rates are within 0.1% and 0.42% for the IAT-based and offset-based covert channels, respectively. Furthermore, the bit error rate of the LSB-based covert channel is equal to that of a normal CAN bus, which is 3.1 × 1e-7%.

ABSTRACT. With the rapid development of wireless communication technologies for electrical vehicles (EVs), as a critical part of a pure EV, the battery could be attacked (e.g., draining energy) to reduce driving range and increase driving range anxiety. However, no methods have been proposed to ensure security of EV batteries. In this paper, we propose the first battery attacks, which can turn on air condition and stop battery charging process by sending requests through a smartphone without being noticed by users. We then propose a Battery authentication method (Bauth) to detect the battery attacks. We firstly build a data-driven behavior model to describe a user's habits in turning on air condition and stopping battery charging. In the behavior modelling, to distinguish users that share a vehicle for high modelling accuracy, we apply the random forest technology to identify each user based on battery state. Based on the established behavior model, we then build a reinforcement learning model that judges whether an AC-turn-on or batter-charge-stop request from a smartphone is from the real user based on current vehicle states. We conducted real-life daily driving experiments with different participants to evaluate the battery attack detection accuracy of Bauth. The experimental results show that Bauth can prevent EV batteries from being attacked effectively in comparison with another method and its accuracy reaches as high as 93.44%.

ABSTRACT. Programmable Logic Controllers (PLCs) provide a prominent choice of implementation platform for safety-critical industrial control systems applications. Formal verification provides ways of establishing correctness guarantees, which can be quite important for such safety-critical applications. But since PLC code does not include an analytic model of the system plant, their verification is limited to "shallow'' discrete properties. In this paper, we, thus, start the other way around with hybrid programs that include continuous plant models in addition to discrete control algorithms. Even "deep'' correctness properties of hybrid programs can be formally verified in the theorem prover KeYmaera X that implements differential dynamic logic, dL, for hybrid programs. After verifying the hybrid program, we now present an approach for translating hybrid programs into PLC code. The new tool, HyPLC, implements this translation of discrete control code of verified hybrid program models to real PLC controller code and vice versa. We define the translation of hybrid programs that are written in differential dynamic logic, dL, to programmable logic controller (PLC) code. HyPLC can also translate existing PLC code into the discrete control actions for a hybrid program given an additional input of the continuous dynamics of the system to be verified. This approach allows for the generation of real controller code while preserving, by compilation, the correctness of a valid and verified hybrid program. PLCs are known to be the cyber-physical interface for safety-critical industrial control applications, and HyPLC serves as a pragmatic tool for bridging formal verification of complex cyber-physical systems at the algorithmic level of hybrid programs with the execution layer of concrete PLC code implementations.

ABSTRACT. Robotics applications are typically programmed in low-level imperative programming languages, leaving the programmer to deal with dynamic controllers affecting the physical state, geometric constraints on components, and concurrency and synchronization. The combination of these features ---dynamics, geometry, and concurrency--- makes developing robotic applications difficult. We present PGDC, a programming model for robotics applications consisting of assemblies of robotic components, together with its runtime and a verifier. PGDC combines message-passing concurrent processes with motion primitives, which represent continuous evolution of trajectories in geometric space under the action of dynamic controllers, and explicit modeling of geometric frame shifts, which allow relative coordinate transformations between components evolving in space. We describe a verification algorithm for PGCD programs based on model checking and SMT solvers that statically verify concurrency-related properties such as absence of deadlocks and geometric invariants such as absence of collision during motion. We have implemented a runtime for PGDC programs that compiles down to imperative code on top of ROS and runs directly on robotic hardware. We illustrate the programming model and reasoning principles by building a number of statically verified robotic manipulation programs on top of 3D-printed robotic arm and cart assemblies.

ABSTRACT. We present ThingFlow, a software architecture to write event-processing pipelines for Internet-of-things (IoT) applications. Such applications typically involve sensing, stateful transformations of event streams, state estimation, and control/actuation, learning, and data analytics. They are currently programmed using a zoo of languages, systems, and APIs with ad hoc data passing protocols.

ThingFlow provides three abstractions: sensors which can sample changing physical values, streams of (potentially real-valued) data, and stateful filters, which transform input streams to output streams, and can be composed. ThingFlow programs consist of com- positions of filters scheduled and run by an explicit, asynchronous, scheduler. The semantics of ThingFlow is given as infinite-state communicating state machines. ThingFlow is implemented as a Python API whose core is compact enough to run on very limited microcontrollers such as the ESP8266, while providing support for sensors, message streams over the network, machine learning, and cloud backends. We show the expressiveness, versatility, and simplicity of ThingFlow on a number of examples from the IoT domain, incorporating sensing, filtering, actuation, data analysis, and learning: a navigation example using GPS, a water heater example, and an IoT example using light sensors and wireless light sources.