Automated attack synthesis by extracting protocol FSMs from RFCs
Tags: fm, nlp, rfc, security
Published: 2022-02-09 19:50:01

---
title: Automated attack synthesis by extracting protocol FSMs from RFCs
published: true
description: by Maria Leonor Pacheco, Max von Hippel, Ben Weintraub, Dan Goldwasser, and Cristina Nita-Rotaru.
tags: FM,NLP,RFC,security
cover_image: https://upload.wikimedia.org/wikipedia/commons/0/03/Hoe%27s_six-cylinder_press.png
---

Certain automated attack discovery tools, such as [🎹KORG](https://github.com/RFCNLP/RFCNLP-korg), [🐍SNAKE](https://github.com/samueljero/snake), or [🧰TCPwn](https://github.com/samueljero/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)](https://en.wikipedia.org/wiki/Finite-state_machine), as well as a formal description of message formats and correctness properties.

TCP FSM            |  DCCP FSM
:-------------------------:|:-------------------------:
![TCP FSM](https://dev-to-uploads.s3.amazonaws.com/uploads/articles/o7f9ij6y8yik7jkldzex.png)  |  ![DCCP FSM](https://dev-to-uploads.s3.amazonaws.com/uploads/articles/s51mu5cymefl27y5xx57.png)

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

[DCCP Implementation](https://github.com/torvalds/linux/blob/fc02cb2b37fe2cbf1d3334b9f0f0eab9431766c4/net/dccp/dccp.h)         |  [DCCP Description](https://datatracker.ietf.org/doc/html/rfc4340)
:-------------------------:|:-------------------------:
![DCCP implementation from linux kernel](https://dev-to-uploads.s3.amazonaws.com/uploads/articles/axyataqdwkv6yba6vemz.png)  |  ![DCCP RFC textual description snippet](https://dev-to-uploads.s3.amazonaws.com/uploads/articles/zl7g5ci56056ykjzqhld.png)

Many prior works extracted FSMs, message formats, or correctness properties from protocol implementations.  For example, [🤖Prospex](https://sites.cs.ucsb.edu/~chris/research/doc/oakland09_prospex.pdf) 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](https://www.ietf.org/) ["Request For Comments"](https://en.wikipedia.org/wiki/List_of_RFCs) documents, or RFCs.  [In prior work](https://arxiv.org/pdf/1810.04755.pdf), we showed how to extract protocol message formats from RFC documents, with [grammar-based fuzzing](https://github.com/samueljero/snake) 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](https://arxiv.org/pdf/2004.01220.pdf) as our motivating use-case.  Our paper will appear in the [2022 IEEE S&P](https://www.ieee-security.org/TC/SP2022/), and our code is [open-source](https://github.com/RFCNLP) and [reproducible](https://github.com/RFCNLP#reproduce-our-results).

* [Preprint](https://github.com/RFCNLP/RFCNLP/blob/main/rfcnlp.pdf)
* [BibTex](https://github.com/RFCNLP/RFCNLP/blob/main/rfcnlp.bib)

## 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](https://en.wikipedia.org/wiki/Natural_language_processing), a sub-field of AI concerned with interpreting human language.  This approach came with some built-in challenges.

1. **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.
2. **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.

![Overview of our approach](https://dev-to-uploads.s3.amazonaws.com/uploads/articles/8qs9n2oxopdixhp8be90.png)

### 1. Learning a Large-Scale Word Representation

We collect a corpus of RFC-related documents such as [technical forums](https://stackoverflow.com/search?q=tcp), [blogs](https://dev.to/maxvonhippel/automated-attacker-synthesis-for-distributed-protocols-45mn), [research papers](https://arxiv.org/abs/2004.01220), and [specification documents](https://datatracker.ietf.org/doc/html/rfc793). We exploit these documents to learn a [distributed word representation](https://en.wikipedia.org/wiki/Word_embedding), also known as an embedding model, for technical language.  In particular, we use a [BERT embedding model](https://pypi.org/project/bert-embedding/), 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:
- <u>Definition tags</u>, used to define states, transitions, etc.;
- <u>Reference tags</u>, used to observe mentions of previously defined data;
- <u>State Machine tags</u>, used to track states and transitions; and
- <u>Control flow tags</u>, used to record the syntactic structure of the RFC document.

For example, consider the following snippet from the [Datagram Congestion Control Protocol RFC](https://datatracker.ietf.org/doc/html/rfc4340):

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

We can annotate this snippet like so:

![Diagram of snippet annotation](https://dev-to-uploads.s3.amazonaws.com/uploads/articles/7wlavzskod0l7w1kzffu.png)

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](https://github.com/RFCNLP/RFCNLP/blob/main/rfcnlp.pdf).

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](https://liyanxu.blog/2021/02/20/overview-of-conditional-random-field-crf/);
* `NeuralCRF` - a [BERT](https://huggingface.co/docs/transformers/model_doc/bert) encoder enhanced with a Bidirectional [LSTM](https://colah.github.io/posts/2015-08-Understanding-LSTMs/) [CRF](https://homepages.inf.ed.ac.uk/csutton/publications/crftut-fnt.pdf) 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` 
:-------------------------:|:-------------------------:
![LinearCRF](https://dev-to-uploads.s3.amazonaws.com/uploads/articles/roew5vpov1xvs7yrbofc.png)  |  ![NeuralCRF](https://dev-to-uploads.s3.amazonaws.com/uploads/articles/msorq8n7e6ol1zdmphci.png)

We evaluate the algorithms on the [BGPv4](https://github.com/RFCNLP/RFCNLP/blob/main/rfcs-original/BGPv4.txt), [DCCP](https://github.com/RFCNLP/RFCNLP/blob/main/rfcs-original/DCCP.txt), [LTP](https://github.com/RFCNLP/RFCNLP/blob/main/rfcs-original/LTP.txt), [PPTP](https://github.com/RFCNLP/RFCNLP/blob/main/rfcs-original/PPTP.txt), [SCTP](https://github.com/RFCNLP/RFCNLP/blob/main/rfcs-original/SCTP.txt), and [TCP](https://github.com/RFCNLP/RFCNLP/blob/main/rfcs-original/TCP.txt) RFCs, in Section VIII (a) of [our paper](https://github.com/RFCNLP/RFCNLP/blob/main/rfcnlp.pdf).  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 `noop`s), *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](https://github.com/RFCNLP/RFCNLP/blob/main/rfcnlp.pdf).  You can also read the actual open-source code [here](https://github.com/RFCNLP/RFCNLP/blob/main/nlp2promela/xmlUtils.py).  At a high level, we do the following:
- use `def_state`s to determine the FSM states
- use `transition`s to determine the transitions; for each one, search the closest `control` block for `ref_state`s to determine where the transition begins and ends, and `ref_event`s 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](https://github.com/RFCNLP/RFCNLP/blob/main/rfcnlp.pdf).  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](https://github.com/RFCNLP/RFCNLP/blob/main/tutorials/detailed.FSM.error.analysis.md).

### 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](https://github.com/maxvonhippel/AttackerSynthesis).  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](https://github.com/RFCNLP/RFCNLP-korg).

### 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](https://github.com/RFCNLP/RFCNLP/blob/main/rfcnlp.pdf).  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](https://github.com/RFCNLP/RFCNLP/blob/main/rfcnlp.pdf).  In the mean time, our code is [open source](https://github.com/RFCNLP/RFCNLP/) and [reproducible](https://github.com/RFCNLP#reproduce-our-results).  We also provide a detailed [tutorial](https://github.com/RFCNLP/RFCNLP/blob/main/tutorials/attacker.synthesis.md) on how to use our software.