Compiling symbolic attacks to protocol implementation tests
This addresses the challenge of validating abstract security flaws in real-world protocol implementations, which is crucial for improving cybersecurity in electronic transactions.
The paper tackles the problem of bridging the gap between abstract attack scenarios from security protocol specifications and concrete penetration tests on real implementations, proposing an architecture to automatically generate abstract attacks and convert them to implementation tests. As a proof of concept, it detected a renegotiation vulnerability in some SSL/TLS implementations.
Recently efficient model-checking tools have been developed to find flaws in security protocols specifications. These flaws can be interpreted as potential attacks scenarios but the feasability of these scenarios need to be confirmed at the implementation level. However, bridging the gap between an abstract attack scenario derived from a specification and a penetration test on real implementations of a protocol is still an open issue. This work investigates an architecture for automatically generating abstract attacks and converting them to concrete tests on protocol implementations. In particular we aim to improve previously proposed blackbox testing methods in order to discover automatically new attacks and vulnerabilities. As a proof of concept we have experimented our proposed architecture to detect a renegotiation vulnerability on some implementations of SSL/TLS, a protocol widely used for securing electronic transactions.