Automated Attacker Synthesis for Distributed Protocols
Tags: formalmethods, synthesis, security, protocol
Published: 2020-06-23 04:07:39

---
title: Automated Attacker Synthesis for Distributed Protocols
published: true
description: Or, breaking protocols with formal methods.
tags: FormalMethods,Synthesis,Security,Protocol
cover_image: https://dt7v1i9vyp3mf.cloudfront.net/styles/news_large/s3/imagelibrary/A/ARP2600FS_01-PuQeYCI21FSRbkAR2V3raR6FzVKyVF6I.jpg
---

## 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](https://www.torproject.org/), or [supporting private and spam-free messaging](https://twitter.com/futurepaul/status/1273234983138754560?s=20).  **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](https://arxiv.org/abs/2004.01220):
```
@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](https://github.com/hmemcpy/milewski-ctfp-pdf/blob/fb7962437c8d47d34a236d77620db14311ceee9f/src/content/0.0/preface.tex#L50).  For monotonically more formal versions of this material, refer to [my SafeComp 2020 presentation](https://link.springer.com/chapter/10.1007/978-3-030-54549-9_9), our [SafeComp 2020 paper](https://link.springer.com/chapter/10.1007/978-3-030-54549-9_9), or the [arXiv preprint](https://arxiv.org/abs/2004.01220).

## Pseudo-Formal Problem Statement

Imagine a harbor full of ships and boats.  [There are pirate ships](https://www.ctga.ox.ac.uk/publications/cybersecurity-and-age-privateering-historical-analogy), fishing ships, naval ships, submarines ([which are boats!](https://www.usni.org/magazines/naval-history-magazine/2017/october/bluejackets-manual-ships-and-boats-and)), 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*.

![sempahores](https://dev-to-uploads.s3.amazonaws.com/i/1pl6zy70aeze3pspbxhs.jpeg)

(Image courtesy of [@owendaveydraws](https://twitter.com/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](https://github.com/maxvonhippel/AttackerSynthesis).  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](http://spinroot.com/spin/Man/promela.html), 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.](https://mxvh.pl/AttackerSynthesis/)

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](https://arxiv.org/abs/2004.01220); a condensed version will be presented in [SafeComp 2020](http://safecomp2020.di.fc.ul.pt/) and published in the Springer LNCS series.

## Demo

We present the following adorable [proof of concept](https://www.alchemistowl.org/pocorgtfo/).  Our models are written in [Promela](http://spinroot.com/spin/Man/promela.html), 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.

![Imgur](https://i.imgur.com/97RtESe.jpg)

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;
}
```