DEV Community: Max von Hippel

Automated attack synthesis by extracting protocol FSMs from RFCs

Max von Hippel — Wed, 09 Feb 2022 19:50:01 +0000

Certain automated attack discovery tools, such as 🎹KORG, 🐍SNAKE, or 🧰TCPwn, are designed specifically to ensure that network protocols operate correctly and securely. Such tools generally require a formal representation of the protocol, e.g., a finite state machine (FSM), as well as a formal description of message formats and correctness properties.

TCP FSM	DCCP FSM

Formal protocol specifications can be extracted from two sources: implementations or textual descriptions.

DCCP Implementation	DCCP Description

Many prior works extracted FSMs, message formats, or correctness properties from protocol implementations. For example, 🤖Prospex extracted state machines from implementations by running them and examining their network traces. We are interested in the alternative approach of extracting protocol specifications from textual descriptions.

Network protocols are usually described prosaically in plain-text English-language documents, such as the IETF "Request For Comments" documents, or RFCs. In prior work, we showed how to extract protocol message formats from RFC documents, with grammar-based fuzzing as our motivating use-case. However, implementing an RFC FSM also requires significant human labor and expertise.

In this work, we try to alleviate this human burden by partially automating the process of FSM extraction, with attacker synthesis as our motivating use-case. Our paper will appear in the 2022 IEEE S&P, and our code is open-source and reproducible.

Challenges

In order to extract an FSM from a protocol RFC, we need to first read the protocol RFC. But what does reading the RFC mean, exactly, in an automated context? In our work, it meant analyzing the RFC document using natural language processing, a sub-field of AI concerned with interpreting human language. This approach came with some built-in challenges.

Defining the Problem. Traditional NLP semantic parsing studies methods for translating natural language into a complete formal representation. However, RFCs do not contain "canonical" or "reference" FSMs. They have mistakes, omissions, and ambiguities which are solved as-needed by human experts. Even in theory, there is no complete one-to-one mapping from RFCs to FSMs.
Choosing an NLP Approach. Many off-the-shelf NLP tools exist, typically trained on newswire text. But when such tools are applied to technical domains their performance degrades substantially. Meanwhile, training rule-based systems from scratch requires significant human effort to label the data, and will yield poor results on RFCs because different RFC documents define variables, constraints, and temporal behaviors totally differently.

Our Approach

First, we learn a large-scale word representation for technical language using off-the-shelf tools. Second, we define and learn protocol-independent information from RFCs, using focused zero-shot learning to adapt to new, unobserved protocol documents without re-training. Third, we use a rule-based mapping from the protocol-independent information to FSMs. Fourth, we show how the resulting FSMs can then be used for attacker synthesis - although notice that these FSMs could alternatively be used for other applications, such as grammar-based fuzzing. Let's go over each of these steps in detail below.

1. Learning a Large-Scale Word Representation

We collect a corpus of RFC-related documents such as technical forums, blogs, research papers, and specification documents. We exploit these documents to learn a distributed word representation, also known as an embedding model, for technical language. In particular, we use a BERT embedding model, pre-trained using the masked language model and the next sentence prediction objective using networking data. This process does not require any manual annotation!

2. Zero-Shot Protocol Extraction

Once we have this representation, we turn our attention to learning a model to extract information regarding an FSM from its RFC. Specifically, we want to structurally annotate the protocol RFC, so that we know precisely which parts of the text describe different states, transitions, variables, errors, etc. in the protocol logic. To do this, we define a grammar that describes a higher-level abstraction of the structure of a general FSM for network protocols, as well as the structure of the RFC document describing the FSM.

bool      ::= true | false
type      ::= send | receive | issue
def-tag   ::= def_state | def_var | def_event
ref-state ::= ref_state id="##"
ref-event ::= ref_event id="##" type="type"
ref-tag   ::= ref-event | ref-state
def-atom  ::= <def-tag>engl</def-tag>
sm-atom   ::= <ref-tag>engl</ref-tag> | engl
sm-tag    ::= trigger | variable | error | timer
act-atom  ::= <arg>sm-atom</arg> | sm-atom
act-struct::= act-struct | act-struct act-atom
trn-arg   ::= arg_source | arg_target | arg_inter
trn-atom  ::= <trn-arg>sm-atom<trn-arg> | sm-atom
trn-struct::= trn-struct | trn-struct trn-atom
ctl-atom  ::= <sm-tag>sm-atom</sm-tag>
           | <action type="type">act-struct</action>
           | <transition>trn-struct</transition>
           | sm-atom
ctl-struct::= ctl-atom | ctl-struct ctl-atom
ctl-rel   ::= relevant=bool
control   ::= <control ctl-rel>ctl-struct</control>
e         ::= control | ctl-atom | def-atom | e_0 e_1

The grammar is general-purpose and intended to support any network protocol. At a high level, it consists of:

Definition tags, used to define states, transitions, etc.;
Reference tags, used to observe mentions of previously defined data;
State Machine tags, used to track states and transitions; and
Control flow tags, used to record the syntactic structure of the RFC document.

For example, consider the following snippet from the Datagram Congestion Control Protocol RFC:

The client leaves the REQUEST state for PARTOPEN when it receives a DCCP-Response from the server.

We can annotate this snippet like so:

Now we know where to look in the RFC in order to find certain information (states, transitions, events, etc.). We call this annotated version of the RFC an "intermediate representation". For full details refer to Section III in our paper.

Annotating the RFC document by hand is almost as time-intensive as manually deriving the protocol FSM. Clearly, annotation should be automated! We experimented with several state-of-the-art NLP algorithms for this task:

LinearCRF - a linear-chain conditional random fields model;
NeuralCRF - a BERT encoder enhanced with a Bidirectional LSTM CRF layer;
LinearCRF+R - like LinearCRF but with some heuristic post-processing rules; and
NeuralCRF+R - like NeuralCRF but with those same heuristic post-processing rules.

`LinearCRF`	`NeuralCRF`

We evaluate the algorithms on the BGPv4, DCCP, LTP, PPTP, SCTP, and TCP RFCs, in Section VIII (a) of our paper. Generally, we find that the neural models outperform the linear ones.

3. Protocol State Machine Extraction

Suppose we're studying the DCCP RFC, and we've produced its intermediary representation either by hand or using LinearCRF, NeuralCRF, LinearCRF+R, or NeuralCRF+R. Now that we know where to look in order to read the RFC, it's time to extract an FSM. Recall that an FSM consists of states s ∈ S, some kind of events e ∈ E, and transitions t ∈ S x E x S. We take the stance that there are four kinds of events: timeouts, epsilon-transitions (like noops), send-events, and receive-events.

Luckily, all of this data is explicitly labeled in the intermediary representation! We just need to assemble it all into an extracted FSM. Our algorithm to do exactly that is described in (a) Section VI and (b) Algorithm ExtractTran in the Appendix of our paper. You can also read the actual open-source code here. At a high level, we do the following:

use def_states to determine the FSM states
use transitions to determine the transitions; for each one, search the closest control block for ref_states to determine where the transition begins and ends, and ref_events to determine what exactly occurs during the transition. In the example from before, the correct extracted transition would be:

REQUEST --- rcv(DCCP-Response) --> PARTOPEN

You can see the TCP and DCCP FSMs extracted by the LinearCRF+R and NeuralCRF+R NLP algorithms in the Appendix of our paper. In that same Appendix, we also give "Gold FSMs", which are extracted from RFCs that are annotated by hand. Mistakes in the Gold FSMs stem from issues in our extraction algorithm, or intrinsic ambiguities in the RFC text. We give a detailed case-by-case analysis of such mistakes for the NLP-extracted TCP and DCCP FSMs here.

4. Attacker Synthesis

Finally, we get to the attacker synthesis. Note that attacker synthesis is just one representative protocol analysis technique that uses a protocol FSM. We used the attacker synthesis tool 🎹KORG. Since KORG was designed for perfect, hand-written FSMs, we had to modify it slightly to support imperfect FSMs like those we can extract from RFCs. Our modified version is available here.

Case Studies

We use TCP and DCCP as case studies. For each protocol, we craft four hand-written correctness properties, which we feed to KORG in conjunction with the FSM. Our results are given in TABLE V and discussed in Section VIII. B of our paper. The TL;DR is that using the NLP-derived FSMs, we find one attack against TCP, which we confirm using a hand-written TCP FSM, and we find numerous attacks against DCCP, of which we confirm some but not all using a hand-written DCCP FSM. Here are some of those confirmed attacks:

Attack #32 discovered using TCP property 1 and the LinearCRF+R TCP FSM injects a single ACK to peer 2, causing a desynchronization between the peers which can eventually lead to a half-open connection, which should be impossible.
Attack #96 discovered using DCCP property 2 and the NeuralCRF+R DCCP FSM performs various useless network operations before spoofing each peer in order to guide the other into CLOSE_REQ. The two peers should never both be in CLOSE_REQ at once.

Conclusion

Our work is exciting, because we take a first step toward automatically extracting FSMs (i.e. code) from RFCs (i.e. text). But it's also limited: the FSMs are imperfect, with missing or incorrect transitions, and we still have to write the correctness properties by hand. We have ideas for how to improve on our technique, which we discuss in Section X (Limitations) of our paper. In the mean time, our code is open source and reproducible. We also provide a detailed tutorial on how to use our software.

PL Tutorial for Sean

Max von Hippel — Fri, 07 Aug 2020 22:21:21 +0000

This is a brief and informal overview of a few useful topics in programming languages and theory of computation. I am writing this to share some basic concepts with my friend Sean, but figured I might as well put it online in case other people find it interesting. I am not an expert on these topics and so might make some mistakes. If you notice a mistake, please say so in the comments.

BNF

A grammar is some formal rule that (perhaps inductively) generates or describes all the vocabulary in a language. The least interesting way to do this is to literally write out all the words, as in, N_3 = { 0, 1, 2 }, but this won't work when we have infinitely large languages. For example, you can't realistically write out every single valid program in the Python programming language. This is where BNF comes in. BNF is best explained via an example. The human genome consists of cytosine (C), guanine (G), adenine (A), and thymine (T) molecules super-glued together. (Sorry Sophia, I am about to massacre the biology.) So, a BNF grammar for the terms e (that is, the words of the language) of DNA would look something like this:

e ::= e_0 e_1 | A | C | T | G

The ::= means "is defined to be" and the | means "or". Obviously e_0 and e_1 are inductively defined as instances of e, so an example of the term e_0 e_1 would be T G. But another example would be A T G, where e_0 is A and e_1 is T G.

If you want to do anything fancier than my DNA example, you need more tools, e.g., contexts. I won't get into that in this tutorial.

Untyped Lambda Calculus

The grammar for the untyped lambda calculus is as follows.

e ::= λx.e | x | e_0 e_1

There are some more complexities that I won't get into right now, which basically boil down to your decisions about order of operations. If you want to know more, google "call by value versus call by name". For now, it suffices to observe that you can easily construct arbitrary computations using the lambda calculus. The basic idea is that λx.e is the function that takes as input x and returns e. So the identity function is id = λx.x, and the concatenation function is cat = λx.λy.xy. See what I did there? You can get the equivalent of f(x, y) by writing λx.λy.

If you take the convention that true = λt.λf.t and false = λt.λf.f then you can easily reproduce all the basics of boolean algebra. For more see here.

There remains one more important thing for me to convince you, namely, that lambda calc equations need not terminate. Take the following famous example.

omega = (λx.xx)(λx.xx)

Obviously this can't be reduced. Observe:

f = (λx.xx)
g = (λx.xx)
then omega = f g
           = (λx.xx) g
           = g g 
           = (λx.xx)(λx.xx)
           = omega

From this we conclude that the untyped lambda calculus can do all the basic boolean logic and can also do things that never terminate. With a bit more bit-crunching you can show it's actually Turing Complete. In fact I believe it's the smallest possible Turing Complete language.

For convenience we usually assume some basic tools like +, -, etc. so that we can write things like plus = λx.λy.x+y or ++ = λx.x+1, etc. Since we can do all boolean algebra, we can build these tools in the same we way build our MIPS or X86 CPUs in Computer Architecture as undergrads (with ripple adders, etc.).

STLC

The STLC is the simply typed lambda calculus. It's not too difficult.

B ::= some types you are interested in, e.g., Int, Bool, whatever floats your boat ...
t ::= t -> t | B
e ::= x | λx:t.e | e_0 e_1

The important observation is that now instead of writing λx.e to mean "the function with input x and output e", we write λx:t.e to mean "the function with input x of type t and output e." Then just derive the output type from the input type and the form of e, and you have all the expressive power of a function f : t --> type(e) defined by x |-> e.

Proofs

Generally in PL proofs are written in tree form

assumptions
-----------(deriving rule)
conclusion

as opposed to

assume assumptions
then by deriving rule
conclusion

For example, suppose I want to prove that omega reduces to omega. I might have a reducing rule like:

-----------------(reducing-rule)
(λx.e)z --> e[z/x]

Here we take the usual convention that e[z/x] means "replace every free occurence of x in e with z." For example, (λx.x+λx.x)[z/x] = (λx.x+λx.x), because all the xs are bounded whereas (x(λx.x))[z/x] = z(λx.x), because the first x was not bounded. Bounding works in the same way it would with quantifiers like Ɐ.

In this case with our reducing-rule the proof of omega -> omega could be:

----------------------(reducing-rule)    --------------------(some-var-replacement-rule)
(λx.xx)(λx.xx) --> (xx)[(λx.xx)/x]        (xx)[(λx.xx)/x] = omega
--------------------------------------------------(some-modus-ponens-ish-rule)
omega -> omega

Pi Calculus, Mu Calculus, etc.

There are various other calculi exactly equal in power to the lambda calculus that rely on fixed-point equations. A fixed-point equation is anything of the form

x = f(x)

For example, the fixed-point equation x = x^2 has solutions x = { 0, 1 }.

In a kind of obvious way, all recursive functions can be described as fixed-point equations, where the equation has a solution for a given input iff the function would eventually terminate for that input, in which case the terminating value is a solution to the equation.

I won't explain the Pi and Mu calculi here but you can easily learn them if you want to ... the important thing is just understanding they rely on this basic concept.

Languages and Automata

An important idea to understand is that there is a relationship between languages and automata. Just to illustrate this idea let L be the language generated by the following grammar:

e ::= x | e_0 LET'S GO e_1

So example sentences include x, x LET'S GO x LET'S GO x LET'S GO x, etc.

We can just as easily represent this with an automaton.

      x 
-->(s_0)------>(s_1)
    ^            |          
    |____________|
      LET'S GO

The transitions are labeled, and if you trace any sequence of transitions with your finger and write down the in-order labels, you should get back something generated by the grammar, unless I made a stupid mistake.

For more on this, see JE Pin's work and book.

Automated Attacker Synthesis for Distributed Protocols

Max von Hippel — Tue, 23 Jun 2020 04:07:39 +0000

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

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

Simple Number-Theoretic Insights with Python

Max von Hippel — Mon, 22 Jan 2018 21:39:58 +0000

Sometimes I learn about a new operator, or equivalence class, or some other such function from ZxZ to Z. Often looking at a grid of the numbers 0 - 9 on x and y axes illuminates interesting properties of such functionals. Here I will give some code with which to do just that.

Before I continue, here's a picture of I/O from the code I will be writing in this blog post / article / thing. I am including this at the start so that anyone who reads this knows what the goal of the code is to begin with.

First let's define a few functionals, or functions, or operations, or whatever. This way we can quickly see the utility of our number_table code once we get to that.

Here are mine, but I encourage you to write your own. Note that I am coding in Python3. The code is simple and I think could be fairly easily ported to your language of choice.

# Euclid's Algorithm for Greatest Common Denominator (GCD):
# See https://en.wikipedia.org/wiki/Euclidean_algorithm for more info
euclid = lambda a, b: a if b == 0 else euclid(b, a % b)

# Two numbers are called "relatively prime" if their gcd is 1
relatively_prime = lambda a, b: int(euclid(a,b) == 1)

modulo = lambda a, b: a % b

and_ab = lambda a, b: a & b

Ok, now that we've got a couple cool little functions to investigate out of the way, let's get to the meat of making number grids. I like to colorize my number-grids by number, so I made a little function for coloring numbers in Python.

number_color = lambda n: "\033[1;3" + str(n) + ";40m " + str(n)

It doesn't really do anything for numbers greater than 8, but that's ok because if this bothers you then you can find a clever way to fix it. (This does not bother me.) Also, if you're interested in numbers bigger than 9 you'll have to modify my code a bit anyway, because I don't currently take that into account in the spacing of my table.

Now, here's my number_table code:

def number_table(method):
    # We assume method is defined
    print("    " + " ".join([number_color(n) for n in range(1,10)]))
    print("     _________________________")
    for a in range(1, 10):
        line = number_color(a) + ": "
        for b in range(1, 10):
            r = method(a, b)
            line += number_color(r) + " "
        print(line)

... And here is some more I/O:

Hope this proves useful!

Hi, I'm Max von Hippel

Max von Hippel — Sat, 10 Jun 2017 06:26:17 +0000

I have been coding for 8 years.

You can find me on GitHub as maxvonhippel

I've worked on a variety of academic and professional projects. You can check out my open-source resume here, or my interactive, open-source landing page here.

I aspire to be a cybersecurity engineer. If you have a cool open-source security project you're working on and are looking for contributors, shoot me an email!