A Model-Based Security Testing Approach for Web Applications

Il pentration testing è l'approccio più comune per testare la sicurezza delle applicazioni web, ma il model-based testing sta costantemente maturando in un'alternativa valida e complementare. Il pentration testing è molto conveniente, nel senso che un lasso di tempo breve di pen-testing di solito è sufficiente per rivelare diversi bug, ma l'esperienza dell'analista di sicurezza è fondamentale; il model-based testing si basa su metodi formali, ma l'analista di sicurezza deve prima creare un modello adeguato dell'applicazione sottoposta a test. In questa tesi, propongo un framework basato su modelli formali e che supporta un analista nella realizzazione di test di sicurezza delle applicazioni web. L'idea alla base del framework è che l'uso di tecniche di model-checking possono automatizzare la ricerca di possibili punti di ingresso vulnerabili nelle applicazioni web, cioè, permettono ad un analista di effettuare test di sicurezza senza tralasciare controlli importanti. Inoltre, il framework permette anche di riuso del lavoro: l'analista può inserire la propria esperienza nel framework e (ri)utilizzarla durante i test futuri su diverse applicazioni. Tali test possono essere svolti sia un un singolo analista che dai membri del gruppo di testing di cui fa parte (se presente un'organizzazione più ampia). In questo modo, la potenzialità di un singolo test (su una specifica applicazione web) non è correlata alle competenze di un singolo analista, ma alle competenze di tutto il gruppo di test. Come esempi concreti, presento quattro casi di studio son il fine di dimostrare l'idoneità e la flessibilità del framework. Sono presentati test per diverse vulnerabilità e confrontati con quelli eseguiti con tre tool di sicurezza.

Penetration testing is the most common approach for testing the security of web applications, but model-based testing has been steadily maturing into a viable alternative and complementary approach. Penetration testing is very cost-efficient, in the sense that little pen-testing time usually is enough to reveal several bugs, but the experience of the security analyst is crucial; model-based testing relies on formal methods but the security analyst has to first create a suitable model of the application under test. In this thesis, I propose a formal and flexible model-based framework that supports a security analyst in carrying out security testing of web applications. The main idea underlying this framework is that the use of model-checking techniques can automate the research of possible vulnerable entry points in the web application, i.e., it permits an analyst to perform security testing without missing important checks. Moreover, the framework also al- lows for reuse: the analyst can collect her expertise into the framework and (re)use it during future tests on possibly different web applications, which may be carried out by her or by members of the testing group of the analyst’s organization, if any. In this way, the potentiality of a single test is not related to the expertise of the single analyst on a specific web application but to the expertise of the entire testing group. As concrete examples, I consider four case studies in order to show the suitability and flexibility of the framework. Tests for a variety of vulnerabilities has been performed and compared with the ones executed with three benchmark security tools.