Abstract
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.
This work was partially supported by the FP7-ICT-2009-5 Project no. 257876, “SPaCIoS: Secure Provision and Consumption in the Internet of Services”.
This is a preview of subscription content, log in via an institution to check access.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Preview
Unable to display preview. Download preview PDF.
References
Berglund, A., et al.: XML Path Language (XPath) 2.0, 2nd edn. (2007), http://www.w3.org/TR/xpath20/
Ammann, P., Ding, W., Xu, D.: Using a model checker to test safety properties. In: ICECCS, pp. 212–221 (2001)
Armando, A., Carbone, R., Compagna, L.: LTL Model Checking for Security Protocols. Journal of Applied Non-Classical Logics, Special Issue on Logic and Information Security, 403–429 (2009)
Armando, A., et al.: The AVANTSSAR platform for the automated validation of trust and security of service-oriented architectures. In: Flanagan, C., König, B. (eds.) TACAS 2012. LNCS, vol. 7214, pp. 267–282. Springer, Heidelberg (2012)
AVANTSSAR. Deliverable 4.2: AVANTSSAR Validation Platform V.2. (2010a), www.avantssar.eu
AVANTSSAR. Deliverable 5.4: Assessment of the AVANTSSAR Validation Platform (2010b), www.avantssar.eu
Büchler, M., Oudinet, J., Pretschner, A.: Security mutants for property-based testing. In: Gogolla, M., Wolff, B. (eds.) TAP 2011. LNCS, vol. 6706, pp. 69–77. Springer, Heidelberg (2011)
Büchler, M., Oudinet, J., Pretschner, A.: Semi-automatic security testing of web applications from a secure model. In: SERE, pp. 253–262. IEEE (2012) ISBN 978-0-7695-4742-8
Clark, J.A., Dan, H., Hierons, R.M.: Semantic mutation testing. Science of Computer Programming 78(4), 345–363 (2013), http://www.sciencedirect.com/science/article/pii/S0167642311000992 , doi:10.1016/j.scico.2011.03.011, ISSN 0167-6423
Dadeau, F., Héam, P.-C., Kheddam, R.: Mutation-based test generation from security protocols in HLPSL. In: Software Testing, Verification and Validation (ICST), pp. 240–248 (2011)
DeMillo, R.A., Lipton, R.J., Sayward, F.G.: Program Mutation: A New Approach to Program Testing. In: Infotech State of the Art Report, Software Testing, pp. 107–126 (1979)
Dolev, D., Yao, A.: On the Security of Public-Key Protocols. IEEE Transactions on Information Theory 2(29) (1983)
Jia, Y., Harman, M.: An analysis and survey of the development of mutation testing. TSE 37(5), 649–678 (2011)
Kay, M.: XSL Transformations (XSLT) Version 2.0. (2007), http://www.w3.org/TR/xslt20/
Saxonica Limited, Kay, M.: SAXON - The XSLT and XQuery Processor (2012), http://saxon.sourceforge.net/
Mödersheim, S., Viganò, L.: The Open-source Fixed-point Model Checker for Symbolic Analysis of Security Protocols. In: Aldini, A., Barthe, G., Gorrieri, R. (eds.) FOSAD 2007/2008/2009. LNCS, vol. 5705, pp. 166–194. Springer, Heidelberg (2009)
OWASP. OWASP WebGoat Project (2011), https://www.owasp.org/index.php/Category:OWASP_WebGoat_Project
Christey, S.: CWE/SANS Top 25 Most Dangerous Software Errors (2011), http://cwe.mitre.org/top25/index.html
da, A., Simão, S., Maldonado, J.C.: MuDeL: a language and a system for describing and generating mutants. Journal of the Brazilian Computer Society 8, 73–86 (2002)
SPaCIoS. Deliverable 5.2: Proof of Concept and Tool Assessment V.2. (2012)
Turuani, M.: The cl-atse protocol analyser. In: Pfenning, F. (ed.) RTA 2006. LNCS, vol. 4098, pp. 277–286. Springer, Heidelberg (2006), http://dx.doi.org/10.1007/11805618_21
Wimmel, G., Jürjens, J.: Specification-based test generation for security-critical systems using mutations. In: George, C.W., Miao, H. (eds.) ICFEM 2002. LNCS, vol. 2495, pp. 471–482. Springer, Heidelberg (2002)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2013 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Oudinet, J., Calvi, A., Büchler, M. (2013). Evaluation of ASLan Mutation Operators. In: Veanes, M., Viganò, L. (eds) Tests and Proofs. TAP 2013. Lecture Notes in Computer Science, vol 7942. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-642-38916-0_11
Download citation
DOI: https://doi.org/10.1007/978-3-642-38916-0_11
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-642-38915-3
Online ISBN: 978-3-642-38916-0
eBook Packages: Computer ScienceComputer Science (R0)