Code Monkey home page Code Monkey logo

tlspuffin's Introduction

tlspuffin

Logo with Penguin

TLS Protocol Under FuzzINg
A Dolev-Yao guided fuzzer for TLS
Developed at LORIA, Inria, France and Trail of Bits, USA

Disclaimer: The term "symbolic-model-guided" should not be confused with symbolic execution or concolic fuzzing.

Description

Fuzzing implementations of cryptographic protocols is challenging. In contrast to traditional fuzzing of file formats, cryptographic protocols require a specific flow of cryptographic and mutually dependent messages to reach deep protocol states. The specification of the TLS protocol describes sound flows of messages and cryptographic operations.

Although the specification has been formally verified multiple times with significant results, a gap has emerged from the fact that implementations of the same protocol have not undergone the same logical analysis. Because the development of cryptographic protocols is error-prone, multiple security vulnerabilities have already been discovered in implementations in TLS which are not present in its specification.

Inspired by symbolic protocol verification, we present a reference implementation of a fuzzer named tlspuffin which employs a concrete semantic to execute TLS 1.2 and 1.3 symbolic traces. In fact attacks which mix \TLS versions are in scope of this implementation. This method allows us to utilize a genetic fuzzing algorithm to fuzz protocol flows, which is described by the following three stages.

  • By mutating traces we can deviate from the specification to test logical flaws.
  • Selection of interesting protocol flows advance the fuzzing procedure.
  • A security violation oracle supervises executions for the absence of vulnerabilities.

The novel approach allows rediscovering known vulnerabilities, which are out-of-scope for classical bit-level fuzzers. This proves that it is capable of reaching critical protocol states. In contrast to the promising methodology no new vulnerabilities were found by tlspuffin. This can can be explained by the fact that the implementation effort of TLS protocol primitives and extensions is high and not all features of the specification have been implemented. Nonetheless, the innovating approach is promising in terms of quickly reaching high edge coverage, expressiveness of executable protocol traces and stable and extensible implementation.

Features

  • Uses the LibAFL fuzzing framework
  • Fuzzer which is inspired by the Dolev-Yao symbolic model used in protocol verification
  • Domain specific mutators for Protocol Fuzzing!
  • Supported Libraries Under Test:
    • OpenSSL 1.0.1f, 1.0.2u, 1.1.1k
    • LibreSSL 3.3.3
    • wolfSSL 5.1.0 - 5.4.0
  • Reproducible for each LUT. We use Git submodules to link to forks this are in the tlspuffin organisation
  • 70% Test Coverage
  • Writtin in Rust!

Dependencies

  • build-essential (make, gcc)
  • clang
  • graphviz

OpenSSL 1.0:

  • makedepend from `xutils-dev package

WolfSSL:

  • autoconf
  • libtool

For the python tlspuffin-analyzer:

  • libyajl-dev
  • wheel from Python pip

Building

Build the project:

git clone https://github.com/tlspuffin/tlspuffin.git
git submodule update --init --recursive
cargo build

Running

Fuzz using three clients:

cargo run --bin tlspuffin -- --cores 0-3

Note: After switching the Library Under Test or its version do a clean rebuild (cargo clean). For example when switching from OpenSSL 1.0.1 to 1.1.1.

Testing

cargo test

Command-line Interface

The syntax for the command-line of is:

      tlspuffin [⟨options] [⟨sub-commands⟩]

Global Options

Before we explain each sub-command, we first go over the options in the following.

  • -c, --cores ⟨spec⟩

    This option specifies on which cores the fuzzer should assign its worker processes. It can either be specified as a list by using commas "0,1,2,7" or as a range "0-7". By default, it runs just on core 0.

  • -i, --max-iters ⟨i⟩

    This option allows to bound the amount of iterations the fuzzer does. If omitted, then infinite iterations are done.

  • -p, --port ⟨n⟩

    As specified in [sec:design-multiprocessing] the initial communication between the fuzzer broker and workers happens over TCP/IP. Therefore, the broker requires a port allocation. The default port is 1337.

  • -s, --seed ⟨n⟩

    Defines an initial seed for the prng used for mutations. Note that this does not make the fuzzing deterministic, because of randomness introduced by the multiprocessing (see [sec:design-multiprocessing]).

Sub-commands

Now we will go over the sub-commands execute, plot, experiment, and seed.

  • execute ⟨input⟩

    This sub-command executes a single trace persisted in a file. The path to the file is provided by the ⟨input⟩ argument.

  • plot ⟨input⟩ ⟨format⟩ ⟨output_prefix⟩

    This sub-command plots the trace stored at ⟨input⟩ in the format specified by ⟨format⟩. The created graphics are stored at a path provided by ⟨output_prefix⟩. The option --multiple can be provided to create for each step in the trace a separate file. If the option --tree is given, then only a single graphic which contains all steps is produced.

  • experiment

    This sub-command initiates an experiment. Experiments are stored in a directory named experiments/ in the current working directory. An experiment consists of a directory which contains . The title and description of the experiment can be specified with --title ⟨t⟩ and --description ⟨d⟩ respectively. Both strings are persisted in the metadata of the experiment, together with the current commit hash of , the version and the current date and time.

  • seed

    This sub-command serializes the default seed corpus in a directory named corpus/ in the current working directory. The default corpus is defined in the source code of using the trace dsl.

Rust Setup

Install rustup.

The toolchain will be automatically downloaded when building this project. See ./rust-toolchain.toml for more details about the toolchain.

Make sure that you have the clang compiler installed. Optionally, also install llvm to have additional tools like sancov available. Also make sure that you have the usual tools for building it like make, gcc etc. installed. They may be needed to build OpenSSL.

Advanced Features

Running with ASAN

ASAN_OPTIONS=abort_on_error=1 \
    cargo run --bin tlspuffin --features asan -- --cores 0-3

It is important to enable abort_on_error, else the fuzzer workers fail to restart on crashes.

Compiling with ASAN using rustc

RUSTFLAGS=-Zsanitizer=address cargo +nightly build --target x86_64-unknown-linux-gnu --bin tlspuffin -p tlspuffin --release --features wolfssl530

Generate Corpus Seeds

cargo run --bin tlspuffin -- seed

Plot Symbolic Traces

To plot SVGs do the following:

cargo run --bin tlspuffin -- plot corpus/seed_client_attacker12.trace svg ./plots/seed_client_attacker12

Note: This requires that the dot binary is in on your path. Note: The utility tools/plot-corpus.sh plots a whole directory

Execute a Symbolic Trace (with ASAN)

To analyze crashes you can also execute a trace which crashes the testing harness using ASAN:

cargo run --bin tlspuffin -- execute test.trace

To do the same with ASAN enabled:

ASAN_OPTIONS=detect_leaks=0 \
      cargo run --bin tlspuffin --features asan -- execute test.trace

Crash Deduplication

Creates log files for each crash and parses ASAN crashes to group crashes together.

tools/analyze-crashes.sh

Benchmarking

There is a benchmark which compares the execution of the dynamic functions to directly executing them in benchmark.rs. You can run them using:

cargo bench
xdg-open target/criterion/report/index.html

Documentation

This generates the documentation for this crate and opens the browser. This also includes the documentation of every dependency like LibAFL or rustls.

cargo doc --open

You can also view the up-to-date documentation here.

tlspuffin's People

Contributors

aeyno avatar lcbh avatar maxammann avatar michaelmera avatar

Stargazers

 avatar  avatar  avatar  avatar  avatar  avatar  avatar  avatar  avatar  avatar  avatar  avatar  avatar  avatar  avatar  avatar  avatar  avatar  avatar  avatar  avatar  avatar  avatar  avatar  avatar  avatar  avatar  avatar  avatar  avatar  avatar  avatar  avatar  avatar  avatar  avatar  avatar  avatar  avatar  avatar  avatar  avatar  avatar  avatar  avatar  avatar  avatar  avatar  avatar  avatar  avatar  avatar  avatar  avatar  avatar  avatar  avatar  avatar  avatar  avatar  avatar  avatar  avatar  avatar  avatar  avatar  avatar  avatar  avatar  avatar  avatar  avatar  avatar  avatar  avatar  avatar  avatar  avatar  avatar  avatar  avatar  avatar  avatar  avatar  avatar  avatar  avatar  avatar  avatar  avatar  avatar  avatar  avatar  avatar  avatar  avatar  avatar  avatar  avatar  avatar

Watchers

 avatar  avatar  avatar  avatar  avatar  avatar

tlspuffin's Issues

Implement a trace which outputs and inputs terms

It must be possible to get data out of it. This will probably rusttls Messages.
It also must be possible to inject data. This could come from the attacker.

This task includes refactoring as we do not need the same kind of agents as in the current code.
We should also rename Send to Output and Expect to Input.

Add mutators for traces

This means we want to be able to add input and output steps, as well as mutate who receives which handle.

Use only rustls Messages

Refactor such that we only deal with buffers of rustls messages. Right now we only want to send rustls messages. This means we do not need to store them as byte buffers.

This maybe simplifies code as the parsing of packages happens right at the interface between openssl and rust.

See whether we can refactor VariableData

The VariableData and the data which flows into operations is basically the same. We could simply remove VariableData and replace it with any probably.

Another way would be to add a Enum VariableData. That would also remove the need of Box<> inside the dynamic function type, because the enum would be copyable/cloneable.

Control TLS Handshake Transcript

In TLS we keep a transcript hash of all actions. Maybe the attacker needs some kind of "memory" from which we can calculate a transcript hash.

Add a way to deconstruct messages

Right now we manually deconstruct each message in the old Expect steps. We need a procedure to deconstruct it.

Maybe use generators?

Trace to trigger a Vulnerability

We want to test whether the attacker is able to detect simple implementation vulnerabilities in TLS 1.3.

There are two ways:

  • Choose a known volnerability of which we know that we can trigger it by modifing fields in a TLS message
  • Introduce a vulnerability which can be triggered by an attacker

We do not yet need a way of automatically detecting it. This is done e.g. in https://gitlab.inria.fr/mammann/tlspuffin/-/issues/15

Implementation of a term algebra

A term looks like the following f(g(a, b,c)). There is a basic implementation which allows the following:

  • Evaluate it using concrete implementations
  • Make it possible to dynamically build terms during runtime.

Some possibilities for ways of doing this:

  • Use a message (enum) type from which the types can be derived
    • The defined operations take care of getting the correct type
  • Use higher level apis like KeyScheduleHandshake to implement operations: Needs exposure here https://github.com/ctz/rustls/blob/d03bf27e0b520fe73c901d0027bab12753a42bb6/rustls/src/lib.rs#L279
  • Automatically get all functions from rustls and make it possible to call them (through Map<str, fn>
    • Statically analyze rustls and get all possible ways of calling functions
    • -> This would eliminate the need to define all operations manually
    • Also very hard because attacker capabilities are not exposed easily. Some need context which can not easily be provided (deep static understanding is required)

Model attacker knowledge

The attacker needs to have knowledge available to be able to generate terms.

This could be as simple as a Vector of variables with a specific types and corresponding handles to VariableData.

Detect Deep Structure of Messages

When OpenSSl outputs a TLS message we can only see which fields are there. We are not able to see deeper and know which secrets have been used to compute the message. This would be needed to detect secrecy.

Here are some notes:

  • keyloging callback
  • -> follow flow into bitstrings

dynamic analysis ->

  • find constructors and desctructors in source code manually
  • When creating a tls message log which in formation was used in which order
    • e.g. session->session_id, ssl->server_random, hs->secret, derive_secret , hs->client_handshake_secret, hs->secret, derive_secret , hs->server_handshake_secret
  • Instrument these variables/functions which are traceable via XRay
  • Build terms out of these logs via heuristics.

https://llvm.org/docs/XRay.html#xray-runtime-library

https://github.com/llvm/llvm-project/tree/d480f968ad8b56d3ee4a6b6df5532d485b0ad01e/compiler-rt/lib/xray

Discussion: Modle Variables as dyn Traid or Enum?

https://www.possiblerust.com/guide/enum-or-trait-object

Pro Trait:

  • Open Set
  • No code generation

Pro Enum:

  • Fast
  • Cloneable and no Heap required

The VariableData and the data which flows into operations is basically the same. We could simply remove VariableData and replace it with any probably.

Another way would be to add a Enum VariableData. That would also remove the need of Box<> inside the dynamic function type, because the enum would be copyable/cloneable.

Setup LibAFL

LibAFL needs to be setup:

  • Allow the fuzzer to execute a trace
  • Serialize traces
  • Define a dummy mutator, which does nothing

Trigger CVE 2021-3449 in TLS 1.2

The function symbol op_attack_cve_2021_3449 already removes a specific extension. The renegotiation ClientHello must be constructed and signed/encrypted such that this works.

Use OpenSSL: 1.1.1j

Remove all uses of unwrap()

If the harness panics then the process is stopped. This is usually not a security vulnerability and shouldn't be counted as one by LibAFL.

Therefore we need to make sure that the Harness is not crashing. This can be done using Rust's Result.

Give Fuzzing Runs a Score

Possible metrics:

  • Path Coverage
  • Node Coverage to some extend
  • Different Protocol Runs (probably similar to Path Coverage)
  • New Types of messages/alerts discovered?

Recommend Projects

  • React photo React

    A declarative, efficient, and flexible JavaScript library for building user interfaces.

  • Vue.js photo Vue.js

    🖖 Vue.js is a progressive, incrementally-adoptable JavaScript framework for building UI on the web.

  • Typescript photo Typescript

    TypeScript is a superset of JavaScript that compiles to clean JavaScript output.

  • TensorFlow photo TensorFlow

    An Open Source Machine Learning Framework for Everyone

  • Django photo Django

    The Web framework for perfectionists with deadlines.

  • D3 photo D3

    Bring data to life with SVG, Canvas and HTML. 📊📈🎉

Recommend Topics

  • javascript

    JavaScript (JS) is a lightweight interpreted programming language with first-class functions.

  • web

    Some thing interesting about web. New door for the world.

  • server

    A server is a program made to process requests and deliver data to clients.

  • Machine learning

    Machine learning is a way of modeling and interpreting data that allows a piece of software to respond intelligently.

  • Game

    Some thing interesting about game, make everyone happy.

Recommend Org

  • Facebook photo Facebook

    We are working to build community through open source technology. NB: members must have two-factor auth.

  • Microsoft photo Microsoft

    Open source projects and samples from Microsoft.

  • Google photo Google

    Google ❤️ Open Source for everyone.

  • D3 photo D3

    Data-Driven Documents codes.