This research blog focuses on novel ways to fuzz the TLS cryptographic protocol. Traditionally, fuzzing mutates bits and bytes. That means that the semantics of the protocol are not directly used to mutate the fuzzing input. Symbolic-model Guided Fuzzing fuzzes on a more abstract level. It uses a symbolic model to create inputs. Therefore, there are two main approaches bit-level fuzzing and model-guided fuzzing (also called generation-based fuzzing) 1. This is also called structure-aware fuzzing by Google.
The classical example for a model which creates fuzz inputs is a grammar. A grammar of a programming language can directly generate syntactically correct programs encoded as text. Furthermore, such a grammar can generate abstract syntax trees (AST), which is just an encoding of the program which is easier to mutate. After mutating an abstract syntax tree it is possible to serialize it to a text-file before passing it to the PUT.
Note that an AST is also a model. Therefore, one should differentiate between models which generate inputs (meta-model) and models which represent inputs.
We will not dive into bit-level fuzzing as this evidence suggests that this technique is not able to create enough coverage paths which represent meaningful attack traces. This approach is not suitable for protocols, especially cryptographic ones. Later messages in a cryptographic protocol depend on random nonces generates in previous ones. That means it is very difficult to reach deep states. This is similar to overcome hash checks in traditional fuzzing. Note that checks against hashes are also used through-out TLS.
Now let’s take a look at related approaches which use a model to fuzz TLS.
|frankencerts||Generates “frankenstein” certificates for testing certificate validation|
|TLS-Attacker||Basically a TLS client which executes traces in configurable ways. Like: Send ClientHello with ECPointFormat and HeartbeatExtension. Expect ServerHello and Certificate messages from server. This allows to check for vulnerabilities like Heartbleed.|
|tlsfuzzer||Allows one to create test-cases which send and expect TLS packets. tlsfuzzer can be run against a server to check for vulnerabilities like DROWN or ROBOT.|
|“Symbolic-Model-Aware Fuzzing of Cryptographic Protocols”||Uses IJON to guide the fuzzer. The input for the PUT is a binary file which represents an abstract execution trace. This trace is mutated by standard AFL methods. The execution is guided by IJON, which uses a scoring.|
|flexTLS (abandoned) and miTLS fstar (TLS 1.3)||Similar to tlsfuzzer and TLS-Attacker as flexTLS also describes testcases for TLS communications.|
|SecFuzz||Uses a concrete implementation of a security protocol to generate valid inputs, and mutate the inputs using a set of fuzz operators|
frankencerts, CertificateFuzzer focus only on the certificates and therefore it not really interesting when fuzzing a protocol as a whole. It could serve as a building block though to increase coverage.
tlsfuzzer and TLS-Attacker are quite similar in the sense that they offer a programmatic way to specify and execute traces. They don’t focus on automated fuzzing though2. They are more tools to define explicit test cases. They are not automatically creating interesting traces based on feedback of the PUT. As they are implemented in Python and Java respectively it is also doubtful whether the code is usable in fuzzing because of performance reasons. Fuzzing usually requires a lot of runs to reach good edge or path coverage.
TLS-Attacker and tlsfuzzer offer a solid base to create test cases on which a fuzzer could be built. Unfortunately fuzzers traditionally are written in C/C++ and nowadays in Rust. Therefore, this could be an area in which preparation could be necessary.
flexTLS follows a similar approach. One difference is that flexTLS uses a verified core. But this also comes with the downside that the used languages F# and F* are rather obscure and not used in practical fuzzing. There are three major applications:
- implementing exploits for protocol and implementation bugs;
- automated fuzzing of various implementations of the TLS
- rapid prototyping of the TLS drafts.
SecFuzz goes into the direction of our fuzzing approach but still fuzzes on the binary level and not the logical level.
The fuzzing is only basic though. For example the SmackTLS tool, which is based on flexTLS checks that deviant traces finish with an alert message and terminate properly 3. This is indeed very similar to tlsfuzzer: “While [tlsfuzzer] uses fuzzing techniques for testing (randomisation of passed in inputs), the scripts are generally written in a way that verifies correct error handling: unlike typical fuzzers it doesn’t check only that the system under test didn’t crash, it checks that it returned correct error messages.”
A flexTLS script looks like this4:
The work about “Symbolic-Model-Aware Fuzzing” guides the fuzzer using the IJON. Clients and servers are represented by agents. The input of an abstract execution trace creates agents, does a handshake between them, creates messages and terms. Messages are then sent between the agents.
After each execution of a trace a score is calculated which is used to evaluate the run.
It is possible to simulate that an adversary is able to control several fields in messages like
In order to produce deviant attack traces one can not use a preexisting TLS library, which is used in production as they try hard not to create invalid traces2. Their job is to create happy paths and avoid deviant ones. The only exception I know so far is rustls. It is quite easy to create and parse packets there. To serialize a message:
To parse the same packet again:
The above mentioned approaches all go in the direction of a model guided fuzzer. They are able to create and serialize messages, inject messages or leave them out and fill fields of message with arbitrary values. This is a very good start. What is missing here though is that no tool has a proper algorithm to generate deviant or happy traces and give feedback on them. They are very manual in the sense that they are not fuzzing tools but testing frameworks.