⚠️ 🧪 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

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.

## 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.

## 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.

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