Automated Attacker Synthesis for Distributed Protocols

Motivation

Distributed protocols are complicated and important. They are complicated because they require coordination between distributed components to achieve a goal, often in the presence of bugs, faults, and attacks. They are important because of the goals they achieve, e.g., anonymously accessing the web, or supporting private and spam-free messaging. Vulnerabilities arise from protocol complexity, and matter because of protocol importance. In this work, we automatically synthesize attackers against distributed protocols, in order to exploit complex logic flaws that humans tend not to notice.

Citation for arXiv preprint:

@article{von2020automated,
  title={Automated Attacker Synthesis for Distributed Protocols},
  author={von Hippel, Max and Vick, Cole and Tripakis, Stavros and Nita-Rotaru, Cristina},
  journal={arXiv preprint arXiv:2004.01220},
  year={2020}
}

In this blog post, I will play fast and loose with the mathematics, and skip details, in order to efficiently communicate the principal idea of our project. In doing so, I follow the esteemed footsteps of Bartosz Milewski. For monotonically more formal versions of this material, refer to my SafeComp 2020 presentation, our SafeComp 2020 paper, or the arXiv preprint.

Pseudo-Formal Problem Statement

Imagine a harbor full of ships and boats. There are pirate ships, fishing ships, naval ships, submarines (which are boats!), paddle-boats, etc. Each ship or boat has a Signalman, whose job is to communicate with other nearby vessels via a formal language of small flags called semaphores.

(Image courtesy of @owendaveydraws)

In particular, the harbor has:

• A prescribed topology, in the sense that only certain vessels can communicate with one another. For example, if your boat is over the horizon from mine, then we cannot communicate, because we cannot see one another.

• Prescribed interfaces, in the sense that each vessel has only certain flags it can send or receive. A vessel cannot stitch together new flags, nor can the Signalman on the vessel magically learn to interpret messages she was not previously trained for.

• A charter (📃) denoting the rules that the harbor as a system must abide by.

We use the symbol ⊨ to mean models or makes true or satisfies, as in, The-Harbor ⊨ 📃. The goal of the attacker is to modify The-Harbor to some system The-Harbor', such that ¬ (The-Harbor' ⊨ 📃), that is, such that the modified harbor violates the charter.

Suppose The-Harbor contains vessels V0, ..., Vn, W0, ..., Wk, and, The-Harbor ⊨ 📃.

Replace vessels V0, ..., Vn with evil doppelgängers V0', ..., Vn' such that the modified system The-Harbor' = V0' ║ ... ║ Vn' ║ W0 ║ ... ║ Wk does not model 📃, i.e., ¬ (The-Harbor' ⊨ 📃).

Pseudo-Formal Solution

We formalize a gadget called a daisy process. Given a Signalman 🧔, the daisy of 🧔 is the simplest non-deterministic automaton that exhausts the space of message-receive and message-send events in the interface of 🧔.

Next, we define The-Harbor' by replacing V0, ..., Vn with daisy(V0), ..., daisy(Vn), and we model-check the result. If the model-checker finds no violating runs, then no attackers exist. On the other hand, if the model-checker finds a violating run, then we automatically translate that violating run into a series of reproducing processes A0, ..., An. When we replace V0, ..., Vn with A0, ..., An, we get a new system The-Harbor-Attacked that van violate the charter. (If W0, ..., Wk are deterministic, then The-Harbor-Attacked will always violate the charter.)

Deliverables

Ok, so, we have pseudo-formally described an attack strategy for naval logistics based on program transformations and reduction to model-checking. But how does this actually manifest in the real world? How might this impact my Signal chat, or my HBO stream?

(It is unlikely to impact your Signal chat; I am not that good of a cryptographer.)

1. We built an open-source tool called Korg. If you are a protocol engineer, or an individual interested in protocol security, we encourage you to download the tool and play with it! You will need to learn Promela, but this is pretty easy. In fact you can probably learn most of it from just the examples in our demo/ folder. Extensive documentation for our tool is available online.

2. We wrote a paper about our method, where we applied Korg to the TCP connection establishment and tear-down routine. We found realistic (known) attacks against TCP totally automatically, in a matter of seconds or minutes. (TCP is a fundamental protocol of the Internet stack.) An extended preprint of that paper is available on arXiv; a condensed version will be presented in SafeComp 2020 and published in the Springer LNCS series.

Demo

We present the following adorable proof of concept. Our models are written in Promela, but should be easy enough to read so long as you understand that chan is a type for channels of communication, mtype is like an enum, chan ? msg means chan.wait-to-recieve(msg), and chan ! msg means chan.send(msg).

First, the harbor, without our vulnerable process v0 = Bob. The only vessel is an evil pirate named Alice, who is deathly afraid of the royal navy and so will not attack anyone with a royal navy semaphore, but will ruthlessly pillage anyone else until they raise their white flag.

mtype = { white, royal, pirate, trading }

chan alice2bob = [0] of { mtype }
chan bob2alice = [0] of { mtype }

bool aliceRetired = false

active proctype alice() {
SCOPING:
    if
    :: bob2alice ? _ -> goto PIRATESTUFF;
    fi
PIRATESTUFF:
    alice2bob ! pirate;
    if
    :: bob2alice ? white -> goto SCOPING;
    :: bob2alice ? royal -> goto end;
    fi
end:
    aliceRetired = true
}

Second, the vulnerable process v0 = Bob, a simple fisherman who has a royal flag but is too dim to use it when confronted with Alice.

active proctype bob() {
FISHING:
    do
    :: bob2alice ! trading;
    :: alice2bob ? pirate -> bob2alice ! white; 
    od
end:
}

Here is Bob's interface in YAML format.

bob2alice:
    I:
    O:white,royal,trading
alice2bob:
    I:pirate
    O:

Notice how although Bob isn't programmed to use a royal flag, in theory, he could.

Let's define a LTL (Linear Temporal Logic) property saying that Alice never gives up or dies.

ltl aliceNeverDies {
    always (aliceRetired == false)
}

Now, we can run this problem through Korg.

And the result we get is the sensible one, where Bob uses that royal flag and escapes piracy for good.

active proctype attacker() {

        bob2alice ! royal;
        alice2bob ? pirate;
        bob2alice ! royal;
}