Model inference and security testing in the spacios project

The SPaCIoS project has as goal the validation and testing of security properties of services and web applications. It proposes a methodology and tool collection centered around models described in a dedicated specification language, supporting model inference, mutation-based testing, and model checking. The project has developed two approaches to reverse engineer models from implementations. One is based on remote interaction (typically through an HTTP connection) to observe the runtime behaviour and infer a model in black-box mode. The other is based on analysis of application code when available. This paper presents the reverse engineering parts of the project, along with an illustration of how vulnerabilities can be found with various SPaCIoS tool components on a typical security benchmark.