โš ๏ธ ๐Ÿงช This post is work-in-progress. Changes are expected as this post is part of my research series.

โœ๏ธ This post allows you to create annotations using hypothes.is. Open the sidebar on the right.

tlspuffin: Symbolic Trace of CVE-2021-3449

research-blog

CVE-2021-3449 is not caused by a flaw of the protocol itself, but because of an implementation issue. To demonstrate that tlspffin is able to find this vulnerability we encode the attack as a symbolic trace.

Input Step #0

A term which evaluates to a ClientHello message and is sent to Agent 1 which is a TLS server.

Output Step #1

We tell Agent 1 to output messages and annotate them with the observed ID $(0,x)$, where $x$ is the index of the message sent during this step.

Input Step #2

A term which evaluates to a ClientKeyExchange message and uses binary data which was observed at (0,2).

Input Step #3

A term which evaluates a ChangeCipherSpec message as traffic is encrypted from now on.

Input Step #4

A term which evaluates an encrypted Finished message. It uses a signed transcript of previously sent messages, including the initial ClientHello.

Input Step #5

A term which evaluates an encrypted ClientHello with a renegotiation extension which includes the signed verification data of the last Finished message.

The Big Picture

The above terms are quite hard to read as they contain cloned sub-terms. By clustering the terms and reusing sub-terms we can make it visually clear that sub-terms are indeed reused.

All steps in a single clustered directed graph.

Note that the above trace does not use a client agent. Is uses a single agent which uses the OpenSSL library and acts as a server. After executing the above trace OpenSSL crashes with a segementation fault.

Do you have questions? Send an email to max@maxammann.org