One of the top security risks reported by the Open Web Application Security Project (OWASP) regarding web applications and services is the incorrectly configured user and session authentication, which enables attackers to exploit passwords, keys, or session tokens, or take control of user accounts to assume their identities (OWASP, 2013).

To address this challenge, we present a model-based mutation testing (MBMT) approach for evaluating the authentication and authorization of web services in a multi-user context. Figure 2 below illustrates an overview of our approach, which includes three main steps.

Step 1. Modeling & Model-based Testing:  we describe the expected behaviour of the web service under test as a UPPAAL Timed Automata (www.uppaal.com) model. Once we check that the implementation of the web service conforms to this model by generating tests from the model and executing them against the implementation.

Figure 1: Example model of a user interaction with a Blog

Step 2.  Mutant generation & Selection: In the second step, we create variants of the model, denoted as mutants, to simulate possible deviations from the intended behaviour. The mutants are derived from a set of well-defined programs, known mutation operators that systematically change the given model.  Since not all mutants are not suitable for the testing (i.e., they are wrong models, or trivial) we apply model-checking properties such as reachability to select valid mutants.

Step 3, Model-based Mutation Testing and Analysis:  The valid mutants are used to generate tests against the implementation.  If the tests generated from the mutant fail, it means that the implementation does not allow the deviation in behaviour and we categorize it as a killed mutant. However, if the tests generated from a mutant model pass successfully, then it means that the implementation may allow a deviation from the intended functionality, thus known as an alive mutant. In this case, we perform further investigation of both the specification and implementation.

Overview of our Model-based Mutation Testing approach

Figure 2: Overview of our Model-based Mutation Testing approach

𝝁UTA Model-Based Mutation Testing Tool for UTA

μUTA tool implements the mutation operators for UPPAAL models. It also implements the reachability criteria for each mutation operator and separates the valid mutants from trivial, or invalid mutants. The tool extends the online model-based testing of UPPAAL Tron by adding mutation generation and selection. Such extension makes the μUTA tool a strong and reliable testing tool for performing robustness testing.

The main advantage of μUTA is the automatic mutation generation, selection, and execution. μUTA is implemented in Python and uses UPPAAL specification model as the input, creates mutants based on the selected mutation operators, verifies the mutants using reachability criteria, and classifies them into valid and invalid groups. The reachability and infection criteria are implemented by a subset of CTL (computation tree logic) verification rules.  A test report is generated detailing the number of mutants killed and alive, including the localization of the mutated statements in the model for further analysis.

The approach and the tool were presented in detail in a conference publication: Siavashi, Faezeh and Truscan, Dragos and Vain, Jüri, Vulnerability Assessment of Web Services with Model-based Mutation Testing. In: 2018 IEEE International Conference on Software Quality, Reliability and Security. IEEE, 2018. Preliminary results show that model-based mutation testing can be an efficient tool in assessing the security vulnerabilities of web applications and services.

Share This