Methods for Model-Based and Vulnerability-driven Security Testing

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.