MobSTer: A model-based security testing framework for web applications

Abstract

Web applications have become one of the preferred means for users to perform a number of crucial and security-sensitive operations such as selling and buying goods or managing bank accounts, official documents, personal health records, and smart houses. The pervasive adoption of such web applications calls for an extensive security analysis in order to avoid attacks. Penetration testing is the most common approach for testing the security of web applications, but model-based security testing has been steadily maturing into a viable alternative and/or complementary approach. Penetration testing is very efficient, but the experience of the security analyst is crucial; model-based security testing relies on formal methods, but the security analyst has to first create a suitable model of the web application. In this paper, we introduce MobSTer, a formal and flexible model-based security testing framework that contributes to filling the gap between these two security testing approaches. The main idea underlying this framework is that the use of model-checking techniques can automate the search for possible vulnerable entry points in the web application, ie, it permits an analyst to perform security testing without missing important checks. Moreover, the framework also allows for reuse: The analyst can collect her expertise into the framework and (re)use it during future tests on possibly different web applications. We have implemented MobSTer as a prototype and applied it to test a number of case studies to assess its strength and concretely evaluate it with respect to four state-of-the-art tools normally used by penetration testers.