Latest Work

• 

  Resource-Bounded Intruders in Denial of Service Attacks

  Denial of Service (DoS) attacks have been a serious security concern, as no service is, in principle, protected against them. Although a Dolev-Yao intruder with unlimited resources can trivially render any service unavailable, DoS attacks do not necessarily have to be carried out by such (extremely) powerful intruders. It is useful in practice and more challenging for formal protocol verification to determine whether a service is vulnerable even to resource-bounded intruders that cannot generate or intercept arbitrary large volumes of traffic. This paper proposes a novel, more refined intruder model where the intruder can only consume at most some specified amount of resources in any given time window. Additionally, we propose protocol theories that may contain timeouts and specify service resource usage during protocol execution. In contrast to the existing resource-conscious protocol verification models, our model allows finer and more subtle analysis of DoS problems. We illustrate the power of our approach by representing a number of classes of DoS attacks, such as, Slow, Asymmetric and Amplification DoS attacks, exhausting different types of resources of the target, such as, number of workers, processing power, memory, and network bandwidth. We show that the proposed DoS problem is undecidable in general and is PSPACE-complete for the class of resource-bounded, balanced systems. Finally, we implemented our formal verification model in the rewriting logic tool Maude and analyzed a number of DoS attacks in Maude using Rewriting Modulo SMT in an automated fashion.

  Continue Reading »

• 

  TSNsched: Automated Schedule Generation for Time Sensitive Networking*

  Time Sensitive Networking (TSN) is a set of stan- dards enabling high performance deterministic communication using time scheduling. Due to the size of industrial networks, configuring TSN networks is challenging to be done manually. We present TSNsched, a tool for automatic generation of schedules for TSN. TSNsched takes as input the logical topology of a net- work, expressed as flows, and outputs schedules for TSN switches by using an SMT-solver. The generated schedule guarantees the desired network performance (specified in terms of latency and jitter), if such schedules exist. TSNsched supports unicast and multicast flows, such as, in Publish Subscribe networks; can combine existing variants of TSN scheduling problems, and reason about the best-effort and priority TSN traffic. TSNsched can be run as a standalone tool and also allows rapid prototyping with the available JAVA API. We evaluate TSNsched on a number of realistic-size network topologies. TSNsched can generate high performance schedules, with average latency less than 1000μs, and average jitter less than 20μs, for TSN networks, with up to 73 subscribers and up to 10 multicast flows.

  Continue Reading »

• 

  Formal Security Verification of Industry 4.0 Applications

  Without appropriate counter-measures, cyber-attacks can exploit the increased system connectivity provided by Industry 4.0 (I4.0) to cause catastrophic events, by, e.g., injecting or tampering with messages. The solution supported by standards, such as, OPC-UA, is to sign or encrypt messages. However, given the limited resources of devices, instead of encrypting all messages in the network, it is better to encrypt only the messages that if tampered with or injected, could lead to undesired configurations. This paper describes the use of formal verification to analyse the security of I4.0 applications. We formalize in Rewriting Logic, I4.0 applications and systems, i.e., networked sets of devices, and a symbolic intruder model. Our formalization can be executed by the tool Maude to automate such security analysis, e.g., determine which messages are sufficient to sign in order avoid injection and tampering attacks.

  Continue Reading »