In the last decade, Remote Attestation (RA) emerged as a distinct security service for detecting attacks on embedded devices, cyber-physical systems (CPS) and Internet of Things (IoT) devices. RA involves verification of current internal state of an untrusted remote hardware platform (prover) by a trusted entity (verifier). RA can help the latter establish a static or dynamic root of trust in the prover and can also be used to construct other security services, such as software updates and secure deletion. Various RA techniques with different assumptions, security features and complexities, have been proposed for the single-prover scenario. However, the advent of IoT brought about the paradigm of many interconnected devices, thus triggering the need for efficient collective attestation of a (possibly mobile) group or swarm of provers. Though recent work has yielded some initial concepts for swarm attestation, several key issues remain unaddressed, and practical realizations have not been explored. This paper’s main goal is to advance swarm attestation by bringing it closer to reality. To this end, it makes two contributions: (1) a new metric, called QoSA: Quality of Swarm Attestation, that captures the information offered by a swarm attestation technique; this allows comparing efficacy of multiple protocols, and (2) two practical attestation protocols — called LISAa and LISAs — for mobile swarms, with different QoSA features and communication and computation complexities. Security of proposed protocols is analyzed and their performance is assessed based on experiments with prototype implementations.

In this manuscript, we present a detailed case study about model-based attack detection procedures for Cyber-Physical Systems (CPSs). In particular, using EPANET (a simulation tool for water distribution systems), we simulate a Water Distribution Network (WDN). Using this data and sub-space identification techniques, an input-output Linear Time Invariant (LTI) model for the network is obtained. This model is used to derive a Kalman filter to estimate the evolution of the system dynamics. Then, residual variables are constructed by subtracting data coming from EPANET and the estimates of the Kalman filter. We use these residuals and the Bad-Data and the dynamic Cumulative Sum (CUSUM) change detection procedures for attack detection. Simulation results are presented – considering false data injection and zero-alarm attacks on sensor readings, and attacks on control input – to evaluate the performance of our model-based attack detection schemes. Finally, we derive upper bounds on the estimator-state deviation that zero-alarm attacks can induce.

We discuss the use of formal modeling to discover potential attacks on Cyber-Physical systems, in particular Industrial Control Systems. We propose a general approach to achieve that goal considering physical-layer interactions, time and state discretization of the physical process and logic, and the use of suitable attacker profiles. We then apply the approach to model a real-world water treatment testbed using ASLan++ and analyze the resulting transition system using CL-AtSe, identifying four attack classes. To show that the attacks identified by our formal assessment represent valid attacks, we compare them against practical attacks on the same system found independently by six teams from industry and academia. We find that 7 out of the 8 practical attacks were also identified by our formal assessment. We discuss limitations resulting from our chosen level of abstraction, and a number of modeling shortcuts to reduce the runtime of the analysis.

Applications for TinyOS, a popular operating system for embedded systems and wireless sensor networks, are written in nesC, a C dialect prone to the same type and memory safety vulnerabilities as C. While availability and integrity are critical requirements, the distributed and concurrent nature of such applications, combined with the intrinsic unsafety of the language, makes those security goals hard to achieve. Traditional memory safety techniques cannot be applied, due to the strict platform constraints and hardware differences of embedded systems. We design nesCheck, an approach that combines static analysis and dynamic checking to automatically enforce memory safety on nesC programs without requiring source modifications. nesCheck analyzes the source code, identifies the minimal conservative set of vulnerable pointers, finds static memory bugs, and instruments the code with the required dynamic runtime checks. Our prototype extends the existing TinyOS compiler toolchain with LLVM-based passes. Our evaluation shows that nesCheck effectively and efficiently enforces memory protection, catching all memory errors with an overhead of 0.84% on energy, 5.3% on code size, up to 8.4% on performance, and 16.7% on RAM.