state-passing style, where each line of code typically corresponds to a message being sent or received. Sending messages out-of-order is as simple as reordering lines in the script. FlexTLS handles most of the complexity internally, filling in reasonable defaults for any missing values. For example, if the script sends a Finished message immediately after a ServerHello message, bypassing the full handshake, Flex TLS would still derive default well-formed connection keys based on empty key exchange values (see Ref. 3 for more detailed examples of Flex TLS scripts).

For each deviant trace, we generate a FlexTLS client or server script that tests its peer by executing the message sequence, which ends by sending a deviant message. According to the standard, the peer should then send an alert (usually unexpected_message) and close the connection. If a non-alert message is received, or the peer does not respond, we assume it wrongly accepted the message, and we flag the trace for further investigation. Not all the TLS implementations we tested support all the scenarios and ciphersuites considered in our traces, and some had unusual error behavior, so we instrumented our scripts to automatically classify peer behavior as correct, unsupported, or wrong. For flagged traces, we manually reviewed the code of the TLS peer, and wrote more detailed Flex TLS scripts by hand to expose and exploit the state machine flaw.

3. IMPLEMENTATION FLAWS AND ATTACKS

Using FlexTLS, we tested several mainstream open-source TLS clients and servers for state machine flaws. To ensure maximal support across implementations, we restricted our tests to use TLS 1.0 with RSA and DHE ciphersuites. Table 1 summarizes our experimental results for OpenSSL, Gnu TLS, NSS, Secure Transport, Java, Mono, and CyaSSL. Of these, OpenSSL is widely used on servers and on Android phones; NSS is used in many web browsers including Firefox and some versions of Chrome and Opera; SecureTransport is used on Apple devices. Mono and CyaSSL do not support DHE key exchanges, so they are tested on a smaller set of deviant traces. CyaSSL and Secure Transport sometimes tear down the TCP connection when they reject a message, instead of sending a fatal alert as prescribed in the standard, so we filtered out cause of the state machine bug.

The set of deviant traces is large (and even infinite unless we bound the number of renegotiations allowed), so we automatically generate a representative, finite subset using three heuristic rules:

 

Skip If σ; m; n ∈ V and δ = σ; n ∉ V, test δ. Thus, for every prefix of a valid sequence, we skip a message if it is mandatory. For example, ClientHello; Server-Hello(kx=DHE); ServerKeyExchange is a trace that skips the Certificate message. (Pragmatically, we also skip several messages within flights, but not their last messages, as otherwise the peer is deadlocked.)

 

Hop Letσ;m∈V andσ′;n∈ V. Ifσ∼σ′,m≠n, andδ =σ;n∉ V, test δ. Thus, if two valid traces have the same prefix, up to their parameters, and they differ on their next messages, we create a deviant trace from the context of the first trace and the next message of the second trace. For example, ClientHello; Server-Hello(kx=RSA); Certificate; ServerKeyExchange is a trace that sends an unexpected ServerKeyExchange by hopping from RSA to Diffie–Hellmann key exchanges.

 

Repeat If σ; m; σ′ ∈ V and δ = σ; m; σ′; m ∉ V, test δ. Thus, we resend any message that appears in a valid trace at any subsequent invalid position. For example, ClientHello; ServerHello; ...; ServerHelloDone; Client-Hello is a trace where the ClientHello message is repeated in the middle of a handshake, making it invalid.

 

An advantage of generating deviant traces from these rules is that, when a trace is accepted by an implementation, it is relatively simple to track the corresponding state machine bug by manual code review. We also experimented with randomly generated deviant traces, but their manual interpretation was more time-consuming and hence less effective.

2. 3. Running deviant traces with Flex TLS

As can be expected, generating arbitrary sequences of well-formed messages is hard. By design, each message in a protocol depends on previously exchanged values, and must pass many basic checks before being accepted by the state machine—after all, TLS implementations are meant to comply with the protocol. At the very least, we need to provide reasonable defaults for any missing values, for instance when keys are needed to format a message and yet the peer’s input to the key derivation is not available yet.

To this end, we develop Flex TLS, a tool for scripting and prototyping plausible TLS message sequences. To send and receive messages, Flex TLS relies on mi TLS. Using this robust, verified TLS library helped us to significantly reduce false positives due, for instance, to malformed messages or incorrect cryptographic processing.

FlexTLS promotes a succinct and purely functional

Table 1. Running deviant traces against mainstream TLS
implementations
Library Key exchange Traces Bugs
OpenSSL 1.0.1j Client RSA, DHE 83 3
Server RSA, DHE 94 6
GnuTLS3.3.9 Client RSA, DHE 83 0
Server RSA, DHE 94 2
SecureTransport Client RSA, DHE 83 3
55471.14

NSS 3. 17 Client RSA, DHE 83 9 Java 1. 8.0_ 25 Client RSA, DHE 71 6 Server RSA, DHE 94 46 Mono 3. 10.0 Client RSA 35 32 Server RSA 38 34 CyaSSL 3. 2.0 Client RSA 41 19 Server RSA 47 20