Methods for Model-Based and Vulnerability-driven Security Testing

Quando si tratta di security testing, le capacità e l'esperienza maturate dal tester durante la sua attività sono i fattori chiave che determinano l'accuratezza e l'efficacia del procedimento di testing. Il Model-Based Testing (MBT) è un campo di ricerca che si è sviluppato negli ultimi anni ed è stato recentemente applicato anche per testare la sicurezza dei servizi web. Il MBT si basa sull'utilizzo di un modello formale del System Under Test (SUT) e di tecniche di model-checking per generare test case astratti. L'obiettivo di questa tesi è la definizione ed implementazione di tecniche formali per testare la sicurezza di applicazioni web e di protocolli di comunicazione. Per fare questo, ho sviluppato e applicato tecniche di Mutation-testing, assumendo la presenza di un modello formale del SUT, in grado di generare test case astratti che, dopo una fase di concretizzazione, possono essere eseguiti sull'implementazione del SUT. Oltre a queste tecniche, ho anche ideato e sviluppato un approccio di MBT basato sul concetto di Chained Attacks, una sequenza di exploit che permettono ad un attaccante di compromettere la sicurezza delle applicazioni web. Questo approccio MBT permette inoltre di generare in maniera semi-automatica un modello formale del SUT, processo che spesso rende impraticabile l'impiego di tecniche di MBT in campo industriale.

When it comes to security testing, the skills and experience the tester has acquired during his activity are the key factors that will determine the accuracy and efficiency of the testing process. Model-Based Testing (MBT) is a research field that has been growing and developing for years and it has been lately applied also to test the security of web services. MBT consists in exploiting a formal model of the System Under Test (SUT) and model-checking tools to cast the test generation problem as a model-checking problem. This reduction allows for the generation of a set of Abstract Test Cases (ATC). The objective of my Ph.D. thesis is the definition and implementation of formal techniques to test the security of web applications and communication protocols. To achieve this goal I have developed and applied Mutation Testing techniques, assuming the presence of a secure model of the SUT, to generate ATC that, after a concretization step, can be executed on the SUT's implementation. I have also designed and developed a MBT approach based on the idea of Chained Attacks, a sequence of exploits allowing an intruder to attack the security of a web application, and the formalization of the web attacker. This MBT approach also provide means for the semi-automatic generation of a SUT's model that is usually a task preventing the application of MBT techniques in the industrial field.