Biblio

Software-based systems are nowadays complex and highly distributed. In contrast, existing intrusion detection mechanisms are not always suitable for protecting these systems against new and sophisticated attacks that increasingly appear. In this paper, we present a new generic approach that combines monitoring and formal methods in order to ensure attack-tolerance at a high level of abstraction. Our experiments on an authentication Web application show that this method is effective and realistic to tolerate a variety of attacks.

We present the Chained Attacks approach, an automated model-based approach to test the security of web applications that does not require a background in formal methods. Starting from a set of HTTP conversations and a configuration file providing the testing surface and purpose, a model of the System Under Test (SUT) is generated and input, along with the web attacker model we defined, to a model checker acting as test oracle. The HTTP conversations, payload libraries, and a mapping created while generating the model aid the concretization of the test cases, allowing for their execution on the SUT's implementation. We applied our approach to a real-life case study and we were able to find a combination of different attacks representing the concrete chained attack performed by a bug bounty hunter.

We present essential concepts of a model-based testing framework for probabilistic systems with continuous time. Markov automata are used as an underlying model. Key result of the work is the solid core of a probabilistic test theory, that incorporates real-time stochastic behaviour. We connect ioco theory and hypothesis testing to infer about trace probabilities. We show that our conformance relation conservatively extends ioco and discuss the meaning of quiescence in the presence of exponentially distributed time delays.

Testing for security related issues is an important task of growing interest due to the vast amount of applications and services available over the internet. In practice testing for security often is performed manually with the consequences of higher costs, and no integration of security testing with today's agile software development processes. In order to bring security testing into practice, many different approaches have been suggested including fuzz testing and model-based testing approaches. Most of these approaches rely on models of the system or the application domain. In this paper we suggest to formalize attack patterns from which test cases can be generated and even executed automatically. Hence, testing for known attacks can be easily integrated into software development processes where automated testing, e.g., for daily builds, is a requirement. The approach makes use of UML state charts. Besides discussing the approach, we illustrate the approach using a case study.