Introduction

SPaCiTE [1,2,3] is a tool for semi-automatically generating and executing security-relevant test cases for web application. The core concept is a mutation based approach which is both vulnerability-driven and property-driven. The starting point is a secure formal specification \(M\) of the system under validation (SUV). It describes the behavior as well as high level security properties \(\Phi\) (e.g., secrecy, authentication, no XSS, no SQL injection) that the SUV has to fulfill. It is called secure because we assume every trace of model \(M\) to fulfill the specified security properties \(\phi\) (\(\forall \varphi \in \Phi: M \models \varphi\)), which can be checked automatically. Because the model is assumed to be secure, a model checker will not find any trace which could be interpreted as test case that violates the specified security properties. Therefore, SPaCiTE applies semantic mutation operators to the model.
These mutation operators capture common vulnerabilities that are found in web applications and represent them at the abstract model level. The mutation operators are collected in a pre-built library, ideally built once and for all by a security expert. Nevertheless the library is easily extendable in the case new vulnerabilities are discovered. To generate test cases using a secure model, the mutation operators are applied to the secure model, resulting in several mutations \(M'\). If for a property \(\varphi\in\Phi: M'\not\models\varphi\), automatic reasoning technologies (e.g., a model checker) will yield a trace of the model that violates \(\varphi\) in \(M'\). This trace exploits a vulnerability (captured by the applied mutation operator) which yields the violation of \(\varphi\). After concretization, this trace is a useful test case for the SUV: if the SUV is vulnerable, the concretized trace is an exploit; if it is not vulnerable, the trace increases confidence that the vulnerability is not present.

Installation

SPaCiTE is available as an Eclipse plugin. To install it, perform the following tasks:

1. Start Eclipse (version 4.4 or newer) and select Help -> Install New Software... -> Add...

2. Add the following two repositories

    Name: TestNG, Location: http://beust.com/eclipse

    Name: SPaCiTE, Location: http://updatesite.spacite.matt-buechler.com.

3. Select "SPaCiTE" under 'Work with'

4. Select "SPaCiTE" in the appearing tree structure and click Next.

Video and Tutorial

To see SPaCiTE in action, have a look at the SPaCiTE video or try the tutorial. Corresponding example models are available.

Modeling a Web Application

SPaCiTE needs a formal specification of the web application as input. Upon creating a new SPaCiTE project in Eclipse, a basic skeleton of such a model is automatically generated. To complete the model, please consider the Modeling Guidelines.

Mutation Operators

SPaCiTE is based on a mutation based approach. Several syntactic and semantic mutation operators are available. Nevertheless SPaCiTE is flexible and can be extended by additional mutation operators. A tutorial how to define mutation operators can be found here.

Support

If you need support for using SPaCiTE, please use the SPaCiTE support ticket system. Support is not guaranteed, but we try our best to help.

References

[1] M. Büchler, J. Oudinet, and A. Pretschner. Security mutants for property-based testing. In TAP, LNCS 6706, pages 69–77. Springer, 2011.

[2] M. Büchler, J. Oudinet, and A. Pretschner. Semi-automatic security testing of web applications from a secure model. In SERE, pages 253–262. IEEE, 2012.

[3] M. Büchler, J. Oudinet, and A. Pretschner. SPaCiTE – Web Application Testing Engine. In SECTEST, pages 858–859. IEEE, 2012.