Latest Work

• 

  Automated Checking of Proof Transformations*

  The proof of many foundational results in structural proof theory, such as theadmissibility of the cut rule and the completeness of the focusing discipline,rely on permutation lemmas. It is often a tedious and error prone task to provesuch lemmas as they involve many cases. Indeed, some cut-elimination results in the literature had to be corrected, even withdrawn, due to missing cases of neededpermutation lemmas. This paper proposes an automated method to prove permutationlemmas. Proof systems are specified in a linear logical framework with subexponentials. From these specifications, we extract logic programs to enumerate all casesinvolved in the proof of a permutation lemma, and to check which cases are satisfied and which cannot be inferred to be satisfied. Finally, we print allcases in a reader friendly format (using \LaTeX) very close to figures appearingin proof theory textbooks. This work is implemented as the tool Quatiand tested for a number of proof systems: linear logic, LJ, LK, MLJ,S4, among others.

  Continue Reading »

• 

  Slow TCAM Exhaustion DDoS Attack*

  Software Defined Networks (SDN) facilitate network man- agement by decoupling the data plane which forwards packets using ef- ficient switches from the control plane by leaving the decisions on how packets should be forwarded to a (centralized) controller. However, due to limitations on the number of forwarding rules a switch can store in its TCAM memory, SDN networks have been subject to saturation and TCAM exhaustion attacks where the attacker is able to deny service by forcing a target switch to install a great number of rules. An underlying assumption is that these attacks are carried out by sending a high rate of unique packets. This paper shows that this assumption is not necessarily true and that SDNs are vulnerable to Slow TCAM exhaustion attacks (Slow-TCAM). We analyse this attack arguing that existing defenses for saturation and TCAM exhaustion attacks are not able to mitigate Slow- TCAM due to its relatively low traffic rate. We then propose a novel defense called SIFT based on selective strategies demonstrating its effec- tiveness against the Slow-TCAM attack.

  Continue Reading »

• 

  On the Accuracy of Formal Verification of Selective Defenses for TDoS Attacks*

  Telephony Denial of Service (TDoS) attacks target telephony services, such as Voice over IP (VoIP), not allowing legitimate users to make calls. There are few defenses that attempt to mitigate TDoS attacks, most of them using IP filtering, with limited applicability. In our previous work, we proposed to use selective strategies for mitigating HTTP Application-Layer DDoS Attacks demonstrating their effectiveness in mitigating different types of attacks.Developing such types of defenses is challenging as there are many design options, \eg, which dropping functions and selection algorithms to use. Our first contribution is to demonstrate both experimentally and by using formal verification that selective strategies are suitable for mitigating TDoS attacks.We used our formal model to help decide which selective strategies to use with much less effort than carrying out experiments. Our second contribution is a detailed comparison of the results obtained from our formal models and the results obtained by carrying out experiments. We demonstrate that formal methods is a powerful tool for specifying defenses for mitigating Distributed Denial of Service attacks allowing to increase our confidence on the proposed defense before actual implementation.

  Continue Reading »