Compiling symbolic attacks to protocol implementation tests

TL;DR

This paper presents an architecture that automatically converts abstract attack scenarios from model-checking tools into concrete tests on protocol implementations, demonstrated by detecting SSL/TLS renegotiation vulnerabilities.

Contribution

It introduces a novel method to bridge the gap between abstract protocol flaws and real-world implementation testing, enhancing blackbox testing capabilities.

Findings

Successfully detected SSL/TLS renegotiation vulnerability

Improved automatic attack generation from abstract scenarios

Enhanced blackbox testing for protocol security

Abstract

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.