Evaluation of ASLan Mutation Operators

The AVANTSSAR validation platform is an automated toolset for validating trust and security aspects of Service-Oriented Architectures (SOAs). Models and security properties are specified in lowlevel AVANTSSAR Specification Language (ASLan) and there are three dedicated model-checkers that can validate if such models satisfy the security properties. However, the implementation may deviate from the specification and may contain some vulnerabilities that an attacker could exploit to violate the defined security properties. We have designed a set of semantic mutation operators to inject such vulnerabilities in an ASLan specification. Here we present the implementation of those mutation operators as Extensible Stylesheet Language Transformation (XSLT) scripts. Then, we evaluate the interest of using semantic mutation operators instead of syntactic ones by comparing the number of mutants that lead to the generation of a test case (i.e., a potential attack) and the resulting test suite for a set of existing ASLan specifications.