Latest Work

• 

  A Formal Security Assessment Framework for Cooperative Adaptive Cruise Control

  For increased safety and fuel-efficiency, vehicle pla- toons use Cooperative Adaptive Cruise Control (CACC) where vehicles adapt their state, incl. speed and position, based on information exchanged between vehicles. Intruders, however, may carry out attacks against CACC platoons by exploiting the communication channels used to cause harm, e.g., a vehicle crash. Therefore, during design-phase, engineers should provide evidence supporting platoon security. This paper proposes a formal framework for the security verification of CACC platoons to provide such evidence based on precise mathematical models. Our vehicle platoon models support the specification of both cyber, e.g., communication protocols, and physical, e.g., speeds, position, vehicle behaviors. Moreover, we propose intruder mod- els that are parametric on his capabilities of manipulating com- munication channels, i.e., message injection and blocking. Our model is implemented enabling the automated formal verification involving both platoon and intruder models. We validate our machinery with a number of attacks taken from the literature and novel attacks discovered by using our formal machinery.

  Continue Reading »

• 

  Less Manual Work for Safety Engineers: Towards an Automated Safety Reasoning with Safety Patterns*

  The development of safety-critical systems requires the control of hazards that can potentially cause harm. To this end, safety engineers rely during the development phase on architectural solutions, called safety patterns, such as safety monitors, voters, and watchdogs. The goal of these patterns is to control (identified) faults that can trigger hazards. Safety patterns can control such faults by e.g., increasing the redundancy of the system. Currently, the reasoning of which pattern to use at which part of the target system to control which hazard is documented mostly in textual form or by means of models, such as GSN-models, with limited support for automation. This paper proposes the use of logic programming engines for the auto- mated reasoning about system safety. We propose a domain-specific language for embedded system safety and specify as disjunctive logic programs reasoning principles used by safety engineers to deploy safety patterns, e.g., when to use safety monitors, or watchdogs. Our machinery enables two types of automated safety reasoning: (1) identification of which hazards can be controlled and which ones cannot be controlled by the existing safety patterns; and (2) automated recommendation of which patterns could be used at which place of the system to control potential hazards. Finally, we apply our machinery to two examples taken from the automotive domain: an adaptive cruise control system and a battery management system.

  Continue Reading »

• 

  Slow denial-of-service attacks on software defined networks

  Software Defined Networking (SDN) is a network paradigm that decouples the network’s control plane, delegated to the SDN controller, from the data plane, delegated to SDN switches.For increased efficiency, SDN switches use a high-performance Ternary Content-Addressable memory (TCAM) to install rules. However, due to the TCAM’s high cost and power consumption, switches have a limited amount of TCAM memory. Consequently, a limited number of rules can be installed. This limitation has been exploited to carry out Distributed Denial of Service (DDoS) attacks, such as Saturation attacks, that generate large amounts of traffic. Inspired by slow application layer DDoS attacks, this paper presents and investigates DDoS attacks on SDN that do not require large amounts of traffic, thus bypassing existing defenses that are triggered by traffic volume.In particular, we offer two slow attacks on SDN. The first attack, called Slow TCAM Exhaustion attack (Slow-TCAM), is able to consume all SDN switch’s TCAM memory by forcing the installation of new forwarding rules and maintaining them indeterminately active, thus disallowing new rules to be installed to serve legitimate clients.The second attack, called Slow Saturation attack, combines Slow-TCAM attack with a lower rate instance of the Saturation attack. A Slow Saturation attack is capable of denying service using a fraction of the traffic of typical Saturation attacks. Moreover, the Slow Saturation attack can also impact installed legitimate rules, thus causing a greater impact than the Slow-TCAM attack. In addition, it also affects the availability of other network’s components, e.g., switches, even the ones not being directly targeted by the attack, as has been proven by our experiments. We propose a number of variations of these attacks and demonstrate their effectiveness by means of an extensive experimental evaluation. The Slow-TCAM is able to deny service to legitimate clients requiring only 38 s and sending less than 40 packets per second without abruptly changing network resources, such as CPU and memory. Moreover, besides denying service as a Slow-TCAM attack, the Slow Saturation attack can also disrupt multiple SDN switches (not only the targeted ones) by sending a lower-rate traffic when compared to current known Saturation attacks.

  Continue Reading »