# The Closer You Look, The More You Learn:
A Grey-box Approach to Protocol State Machine Learning

Chris McMahon Stone
University of Birmingham  Sam L. Thomas
University of Birmingham  Mathy Vanhoef
New York University Abu Dhabi  James Henderson
University of Birmingham  Nicolas Bailluet
ENS Rennes  Tom Chothia
University of Birmingham

###### Abstract

In this paper, we propose a new approach to infer state machine models from
protocol implementations. Our method, StateInspector, learns protocol states
by using novel program analyses to combine observations of run-time memory and
I/O. It requires no access to source code and only lightweight execution
monitoring of the implementation under test. We demonstrate and evaluate
StateInspector’s effectiveness on numerous TLS and WPA/2 implementations. In
the process, we show StateInspector enables deeper state discovery, increased
learning efficiency, and more insightful post-mortem analyses than existing
approaches. Further to improved learning, our method led us to discover
several concerning deviations from the standards and a high impact
vulnerability in a prominent Wi-Fi implementation.

##  1 Introduction

Flaws in protocol state machines have led to major vulnerabilities in many
cryptographic protocols, ranging from TLS [18] to WPA/2 [39]. Thus, the
ability to extract these state machines from implementations and verify their
correctness is an attractive means to perform security analysis. Moreover,
since state machine models provide a succinct representation of the inner
workings of an implementation—summarising tens of thousands of lines of code
in a diagram that fits on a single page—they are also significantly easier to
reason about and analyse than the implementation itself. Current state-of-the-
art approaches to extract state machines are built on active model learning
algorithms that descend from the work of Angluin on learning regular sets [4].
Angluin introduced an algorithmic framework, the Minimally Adequate Teacher
(MAT), and the learning algorithm L*. These techniques were later adopted for
learning mealy-machine models [29, 34] and implemented in the open-source
library LearnLib [27, 32]. The release of this library sparked a number of
efforts to deploy model learning for applications such as conformance testing,
legacy system inference, and most relevantly, security protocol analysis. In
the security domain, it has been applied to various protocols, including TLS
[17, 18], SSH [22], Wi-Fi [36], TCP [20], OpenVPN [16], and many others [2, 3,
37].

An inherent limitation of these works, which all perform a type of black-box
model inference, is that they rely entirely on I/O observations. This means
that any protocol behaviour which does not manifest via I/O, or does so beyond
the preconfigured bound of the learning algorithm, cannot be extracted. In
this paper, we present a new paradigm for model learning which overcomes this
limitation. Our technique examines protocol behaviour “under-the-hood”, with
respect to an implementation’s concrete execution state and how it handles
I/O. As a result, we are able to learn models that capture more behaviour and
obtain insights beyond what is possible by just considering I/O, allowing for
easier model inspection and understanding.

Our state machine learning method works in two stages. In the first stage, we
capture snapshots of the implementation’s execution context (i. e., memory and
registers) whilst it runs the protocol, which we then analyse to identify the
locations in memory that define the protocol state for each possible state. In
the second stage, we learn the complete state machine by sending inputs to the
protocol implementation and analysing the identified locations to see which
values the state defining memory takes, and so which protocol state has been
reached. This allows us to recognise each protocol state as soon as we reach
it, making learning more effective than previous methods that require
substantially more queries.

Similar to black-box learning, we are able to reason about the correctness of
our approach, in the sense that we can list the assumptions that must hold for
learning to terminate and result in a correct state machine. We verify that
our assumptions are reasonable and and realistic for analysing implementations
of complex, widely deployed protocols, including TLS and WPA/2. Further, we
are able to demonstrate case studies of protocols that contain difficult to
learn behaviour, that our method is able to learn correctly, but state-of-the-
art black-box approaches cannot learn: either due to non-termination, or
because they output the incorrect state machine.

Table 1: Comparison of protocol model learning approaches. Style refers to active generation of inputs sequences, or passive trace replays. Requirements denote: (P)rotocol Implementation, (A)bstraction functions for I/O, (T)races of protocol packets, and (F)uzzer. Learned information categorised as input (I), input to protocol state (I2PS), and input to concrete state (I2CS).  |  |  Goals |  Style | Requirements |  Crypto-protocols | What is learned? |  State-classifier
---|---|---|---|---|---|---|---
|  |  |  |  P |  A |  T |  F |  |  I |  I2PS |  I2CS |
Black-box |  Model learning [18, 36] |  Model extraction |  Active |  |  |  |  |  |  |  |  |  I/O
|  Pulsar [23] |  State-aware fuzzing |  Passive |  |  |  |  |  |  |  |  |  I/O
Grey-box |  Prospex [14] |  Protocol RE |  Passive |  |  |  |  |  |  |  |  |  Control-Flow-I/O
|  MACE [11] |  Input discovery |  Active |  |  |  |  |  |  |  |  |  I/O
|  AFLnet [30] |  State-aware fuzzing |  Active |  |  |  |  |  |  |  |  |  I/O
|  StateInspector |  Model extraction |  Active |  |  |  |  |  |  |  |  |  Memory

Contribution Summary:

  * •

We present the design and implementation of a new model inference approach,
StateInspector, which leverages observations of run-time memory and program
analyses. Our approach is the first which can map abstract protocol states
directly to concrete program states.

  * •

We demonstrate that our approach is able to learn states beyond the reach of
black-box learning, while at the same time improve learning efficiency.
Further, the models we produce allow for novel, post-mortem memory analyses
not possible with other approaches.

  * •

We evaluate our approach by learning the models of widely used TLS and WPA/2
implementations. Our findings include a high impact vulnerability, several
concerning deviations from the standards, and unclear documentation leading to
protocol misconfigurations.

To facilitate future research, we make StateInspector and its test corpus
publicly available as open source [1].

We organise the paper as follows: we first provide the necessary background on
model learning and binary analysis, then discuss the limitations of prior work
and present a set of guiding research questions. Next, we present a high-level
overview of our method, StateInspector, and the assumptions we make, and
follow it with a more in-depth discussion of our algorithm and learning
framework. We then provide a thorough evaluation with respect to the current
state of the art, and our research questions, for a number of TLS and WPA/2
implementations. Finally, we discuss the validity of our assumptions and the
implications if they do not hold.

##  2 Background

###  2.1 Model Learning

The models we learn take the form of a Mealy machine. For protocols, this type
of model captures the states of the system which can be arrived at by
sequences of inputs from a set $I$, and trigger corresponding outputs from a
set $O$. We consider Mealy machines that are complete and deterministic. This
means that for each state, and input $i\in I$, there is exactly one output and
one possible succeeding state.

Mealy machine learning algorithms include $L^{*}$ [4, 29, 34] and the more
recent space-optimal TTT algorithm [26]. In essence, all of these algorithms
work by systematically posing output queries from $I^{+}$ (i. e., non-empty
strings of messages), each preceded by a special reset query. These queries
are mapped from abstract strings to concrete messages by an oracle, and then
forwarded to the System Under Test (SUT). Each response from the SUT is then
mapped back to an abstract output $o\in O$ for each prefix of the input
message string, i. e., $p\in I^{+}$. Once a hypothesis which achieves specific
properties, namely completeness and closedness, has been built, a secondary
procedure begins where equivalence queries are posed to the teacher. These
queries attempt to find counter-examples to refine the hypothesis. In black-
box settings, these can be generated in various ways, including random
testing, or more formally complete methods like Chow’s W-Method [12].
Unfortunately, using the W-Method is highly expensive, essentially requiring
an exhaustive search of all possible input sequences up to a specified bound.
Naturally, a higher bound increases the number of queries required to learn a
state machine and any states beyond this bound cannot be learned. In order to
strike a trade-off between ensuring learning is tractable and obtaining
representative model, selection of this bound requires careful consideration.
Learned models can be analysed for interesting behaviour either manually, or
automatically, e. g., by using formal model checking [22, 20].

###  2.2 Binary Program Analysis

Our method does not require access to the source code of the SUT. Instead, we
perform our analyses at the level of assembly language instructions,
registers, and program memory. We base our analyses on two techniques: taint
propagation and symbolic execution. Both methods compute properties of memory
locations and registers along an execution path.

Taint propagation tracks the influence of _tainted_ variables by instrumenting
code and tracking data at run time. Any new value that is derived from a
tainted value will also carry a taint, for example, if variable A is tainted
and influences variable B, and variable B in turn influences C, then variable
C is also tainted meaning it is (indirectly) influenced by A.

Symbolic execution computes constraints over _symbolic_ variables based on the
operations performed on them. For instance, suppose A is marked as symbolic,
and a variable B is derived from A using some expression `B=f(A)`, then
symbolic execution will track this relation between both variables. More
importantly, if we encounter a branch condition (e. g., if-then-else) that
depends on a symbolic variable, we can query an SMT solver to obtain suitable
assignments that explore all feasible branches.

##  3 Motivation and Related Work

In Table 1, in addition to StateInspector, we summarise five key approaches
whose central aim is to learn a model of the state machine implemented by a
protocol. Each approach learns this model for different reasons (i. e.,
fuzzing, reverse-engineering, or conformance testing), and their assumptions
also differ (i. e., black or grey-box access, known or unknown target
protocols, and active or static trace-based learning). In this section, we
discuss the fundamental limitations of these key approaches, and demonstrate
the need for a new direction. In doing so, we relate other works whose
contributions also bear noteworthy relevance. We finish by presenting a set of
research questions that serve as guiding principles for the design and
evaluation of our proposal.

Limited Coverage Learned model coverage in passive trace-based learning
approaches (e. g., [23, 14]) is entirely determined by the quality of pre-
collected packet traces, and consequently is most appropriate for learning
unknown protocols. On the other hand, since active methods can generate
protocol message sequences on-the-fly, their coverage capability is self-
determined. All state-of-the-art active methods (black-box [18, 36, 17, 21,
22] and grey-box [11, 30]) use automata learning algorithms (e. g., L* or TTT)
for their query generation and model construction, and such algorithms are
known to have two key limitations. First, queries to a target system are
constructed with a fixed, pre-defined set of inputs (i. e., protocol
messages). This means that behaviour triggered with inputs outside of this set
cannot be explored. To help alleviate this issue, two approaches integrating
automata learning with grey-box analyses have been proposed—MACE [11], which
uses concolic execution, and AFLnet [30], which uses fuzzing. Despite some
success when applied to text-based protocols, these and other existing model
learning techniques suffer from a second issue, namely, limited exploration
with respect to the _depth_ of the state machine.

1
---
0
---
2
---
3
---
auth / error
---
data / error
---
close / error
---
init / ack
---
-
---
init / ack
---
x11
---
auth / error
---
data / error
---
init / error
---
data / error
---
close / error
---
all / -
---
init / error
---
close / close
---
close / close
---
auth / ack
---
data / ack
---
auth / ack
---
auth / error
---
data / error
---
close / error
---

Figure 1:  State machine with a deep-state backdoor that can only be activated
by sending 12 consecutive init messages.

Consider the state machine in Figure 1. In this simple protocol, a backdoor
exists that allows us to transition from state 1 (not authenticated) to state
2 (authenticated) by supplying an input of 11 init messages, as opposed to an
auth message111This backdoor is similar to a flaw found in a WPA/2
implementation [36], which permitted a cipher downgrade after 3 failed steps
of the handshake.. To learn this state machine, state-of-the-art model
learning with the TTT-Algorithm [26] and modified W-Method [18] requires ~360k
queries to discover the backdoor, but fails to terminate after 1M
queries—essentially operating by brute-force. This is because the number of
queries posed is polynomial in the number of messages, states and exploration
depth. Moreover, to identify this backdoor, we must set a maximum exploration
depth of at least 11. In practice, however, since query complexity explodes
with a high bound, most works use a much lower bound (e. g., 2 in [18, 22]),
or use random testing which lacks completeness. This query explosion is also
exacerbated by large input sets. Hence, for systems where time-spent-per-query
is noticeable (e. g., a few seconds, as is the case with some protocols), it
is apparent that learning such systems requires a more efficient approach.

Limited Optimisations Similar to the problem of limited coverage, current
approaches also lack sufficient information to optimise learning. That is, I/O
observations do not enable learning effort to be focused where it is likely to
be most fruitful. Consider de Ruiter et al.’s application of black-box
learning to RSA-BSAFE for C TLS [18]. Their learner cannot detect that the
server does not close the connection upon handshake termination, and, thus,
exhausts its exploration bound, posing tens of thousands of superfluous
queries.

Prospex’s grey-box approach [14] has the potential to avoid such an issue
through its alternative modelling of states based on execution traces.
However, it cannot capture states that only manifest as changes to memory, e.
g., counter increments per message read, and its coverage is inherently
limited due to the use of trace-replays. Consequently, like MACE [11] and
AFLnet [30], it is not applicable to protocols with complex state or replay-
protection (i. e., security protocols).

Limited Insight A further downside of methods that infer models based
exclusively on I/O is that they may result in an over-abstraction. This can
impede an analyst in obtaining a sufficiently detailed understanding of the
implementation. Additionally, as active learning methods produce models that
depend on how they map between concrete and abstract messages, their learned
models will be inaccurate if the mapping is incorrect. This mapping is done by
a test harness, which is a highly flexible implementation of the target
protocol (denoted by P in Table 1). The harness must be able to send and
interpret protocol messages in an arbitrary order. However, this is a complex
task, and the developer of the harness often has to make (undocumented)
decisions on how to handle unexpected or malformed messages. As a result,
accurately interpreting the resulting I/O model can be difficult to almost
impossible, potentially making the resulting model effectively incorrect. This
downside is exemplified in a black-box analysis of TLS by de Ruiter et al.
[18]. In particular, the author’s acknowledge that their state machines for
OpenSSL 1.0.1g and 1.0.1j are incorrect due to differing assumptions between
the implementation and their test harness. Unfortunately, determining whether
a resulting model is incorrect due to a flawed test harness, or whether there
is in fact a bug in the tested implementation, is impossible based on the I/O
model alone. Instead, an expert must manually analyse both the harness and
implementation to determine this. Thus, I/O models alone provide limited
insight, which extra grey-box information can help overcome.

We note that some works extend black-box learning with taint analysis to learn
register automata for protocols [25, 33]. Such automata are more insightful
than Mealy machines, since they attempt to model conditions on state data for
transitions between states. Unfortunately, these proposals assume access to
source code and do not scale to _real-world_ protocols.

Research Questions Based on the above limitations of current works, we use the
following research questions to guide the design of our new grey-box approach,
StateInspector:

RQ1: Can we expand the capability of model learning to locate deep states
typically beyond reach of current approaches, especially when learning with
large input sets?

RQ2: Can we exploit grey-box information in order to apply more targeted
learning, resulting in efficiency gains?

RQ3: Can we employ observations of internal SUT behaviour, e. g., API usage or
memory classifications of states, for more insightful analysis of the inferred
I/O models?

Learner
---
Concolic analyser
---
Test harness
---
SUT
---
API interceptor
---
Watchpoint handler
---
I/O channel
---
Debug channel
---
Output queries
---
Type & memory
---
classifications
---
Black-box component
---
Grey-box component
---
Execution monitor
---
Input/output
---
Snapshots & watchpoint queries
---

Figure 2: Grey-box State Learning Architecture.

##  4 Overview

We depict a high-level overview of our approach in Figure 2. Our method
combines insights into the runtime behaviour of the SUT (provided by the
execution monitor and concolic analyser) with observations of its I/O
behaviour (provided by the test harness) to learn models that provide
comparable guarantees to traditional black-box approaches. We organise this
section by first stating the assumptions we make about the state machines our
approach learns, and then provide an overview of its operation. So that the
reader has a clear understanding of all assumptions we make of the
implementations we analyse, we also state assumptions about the configurable
parameters of our method. We defer discussion of the choice of their concrete
assignments, and how the assumptions can be loosened (and the implications of
doing so) to later sections, so that they can be understood in context.

Our first assumption is standard for state machine learning:

Assumption 1. The protocol state machine of the SUT is finite, and can be
represented by a mealy machine.

In all concrete implementations, each state of this mealy machine will
correspond to a particular assignment of values to specific “state-defining”
memory locations, allocated by the implementation. We use two terms to discuss
these locations and the values assigned to them, which we define as follows:

######  Definition 1 (Candidate State Memory Location)

Any memory location that takes the same value after the same inputs, for any
run of the protocol.

######  Definition 2 (A Set of State-Defining Memory)

A minimal subset of candidate state memory locations whose values during a
protocol run uniquely determine the current state.

For simplicity, we also refer to a member of any state-defining memory set as
state memory. Our next assumption is that we know a priori the complete
language needed to interact with the SUT and hence generate the state machine:

Assumption 2. All protocol states can be reached via queries built up from the
inputs known to our testing harness $I^{+}$.

Under these assumptions, we now describe the operation of our approach. Our
learner uses a test harness to interact with the SUT. This test harness is
specific to each protocol analysed and tracks session state, and is
responsible for communicating with the SUT and translating abstract
representations of input and output messages (for the learner) to concrete
representations (for the SUT). In the first phase of learning, the learner
instructs the test harness to interact with the SUT to exercise normal
protocol runs, trigger errors, and induce timeouts multiple times. We capture
snapshots of the SUT’s execution context (i. e., its memory) for each of these
runs using an execution monitor. We perform subsequent analysis of the
snapshots in order to determine a set of candidate memory locations that can
be used to reason about which state the SUT is in. We make the following
assumption about this memory:

Assumption 3. A set of state-defining memory for all states is allocated along
a normal protocol run, and this memory will take a non-default value in the
normal run, during error handling, or timeout routines.

Any memory location found to have the same value for each sequence of inputs
for each run is considered candidate state memory. And any location that takes
the same value in all states is discarded. Assumption 3 ensures that this
reduced set of locations will be a set of state-defining memory, however, this
set may also contain superfluous locations. Further, this set of locations may
not be state-defining for every state, and is rather a superset of locations
for all states.

The next phase of learning uses the candidate set to construct a model of the
protocol state machine. During this process, we identify the set of state-
defining memory for each state. This allows us to determine if two states
arrived at from the same input sequence should be considered equal, even if
their memory differs, as we only need to consider the values of state-defining
locations when performing this so-called equivalence check. It also allows us
to effectively ignore any superfluous locations in our candidate set since
they will not be considered state-defining for any state.

To learn the state machine, we queue all queries from $I^{+}$ to fulfill the
completeness property for states in a mealy machine. Namely, that all inputs
are defined for each state. We perform these queries iteratively in increasing
length. As in the first phase, we take snapshots of the execution state of the
SUT on each I/O action. Each time a distinct state, according to its I/O
behaviour and defined state memory, is discovered, we queue additional queries
to ensure that the state is also fully defined (i. e., we attempt to determine
all states reachable from it). We continue building the automaton in this way
until no new states are found.

As well as state memory, it is possible that our candidate set contains
locations with assignments that appear to be state-defining for all states
identified from the set of posed inputs, but are actually not. For instance,
if a protocol implementation maintains a counter of the messages received, it
might be mistaken for state memory, leading to a self loop in the state
machine being conflated with an infinite progression of seemingly different
states. Recognising such memory will prevent our framework from mistaking a
looping state from an infinite series of states, and so ensures termination.
To determine if such memory exists and if it can be ignored, we perform a
merge check. This allows us to replace a series of states repeated in a loop,
with a single state and a self loop. This check is only performed between
states that have the same observed input and output behaviour, and are
connected at some depth (i. e., one is reachable from the other). We make the
following assumption about this depth:

Assumption 4. The depth that we check for possible merge states is larger than
the length of any loop in the state machine of the implementation being
tested.

When performing a merge check, we consider two states equal if the values
assigned to their state-defining locations are equal. Therefore, for each
location that differs, we must determine if it behaves as state memory for
each state (we discuss the conditions for this in Section 5.5). To do so, we
use a novel analysis (implemented in the concolic analyser in Figure 2). This
analysis identifies a memory location as state-defining when this location
influences decisions about which state we are in. Concretely, this is encoded
by checking if the location influences a branch that leads to a write to any
candidate state memory. That is, state-defining memory will control the state
by directly controlling writes to (other) state memory, and non-state-defining
memory will not. This leads to our final assumption:

Assumption 5. Any state-defining memory will control a branch, along an
execution path triggered by messages from the set $I^{+}$, and it will lead to
a write to candidate state memory within an a priori determined number of
instructions.

We discuss the selection of the above bound in Section 5.5.2, but note that it
is a configurable parameter of our algorithm. We complete learning when no
further states can be merged, and no new states (that differ in I/O behaviour
or state memory assignment) can be discovered by further input queries. At
this point, StateInspector outputs a representative mealy machine for the SUT.

##  5 Methodology

The learner component of Figure 2 orchestrates our model inference process. It
learns how the SUT interacts with the world by observing its I/O behaviour via
the test harness, and learns how it performs state-defining actions at the
level of executed instructions and memory reads and writes, via the execution
monitor. Inference begins with a series of bootstrap queries in order to
identify candidate state memory, i. e., $M$. All queries posed to the SUT in
this stage serve the dual purpose of identifying state memory and also
refining the model. This ensures minimal redundancy and repetition of queries.
Given an estimation of $M$, we then proceed to construct the state machine for
the implementation by identifying each state by its I/O behaviour and set of
state-defining memory. Throughout this process we perform merge checks which
determine if two states are equivalent with respect to the values of their
state-defining locations.

###  5.1 Monitoring Execution State

To monitor a SUT’s state while it performs protocol related I/O, we take
snapshots of its memory and registers at carefully chosen points. As many
protocols are time-sensitive, we ensure that this monitoring is lightweight to
avoid impacting the protocol’s behaviour. More specifically:

  1. 1.

We avoid inducing overheads such that the cost of each query becomes
prohibitively high.

  2. 2.

We do not interfere with the protocol execution, by, for example, triggering
timeouts.

  3. 3.

We only snapshot at points that enable us to capture each input’s effect on
the SUT’s state.

To perform a snapshot, we momentarily pause the SUT’s execution and copy the
value of its registers and contents of its mapped segments to a buffer
controlled by the execution monitor. To minimise overheads, we buffer all
snapshots in memory, and only flush them to disk after the SUT has finished
processing a full query. We find that the overheads induced by snapshotting in
this way are negligible and do not impact the behaviour of any of the
protocols analysed.

To identify when to perform snapshots, we infer which system calls (syscalls)
and fixed parameters a SUT uses to communicate with its client/server. We do
this by generating a log of all system calls and passed parameters used during
a standard protocol run. We then identify syscall patterns in the log and
match them to provided inputs and observed outputs. The number of syscalls for
performing I/O is small, hence the number of patterns we need to search for is
also small, e. g., combinations of bind, recvmsg, recvfrom, send, etc. When
subsequently monitoring the SUT, we hook the identified syscalls and perform
state snapshots when they are called with parameters matching the those in our
log.

####  5.1.1 Mapping I/O Sequences To Snapshots

To map I/O sequences to snapshots, we maintain a monotonic clock that is
shared between our test harness (which logs I/O events) and our execution
monitor (which logs snapshot events). We construct a mapping by _aligning_ the
logged events from each component, as depicted in Figure 3. When doing so, we
face two key difficulties. First, implementations may update state memory
before or after responding to an input, hence we must ensure we take snapshots
to capture both possibilities (i. e., case ❸ in Figure 3). Second, some parts
of a query may not trigger a response, hence we must account for the absence
of write-like syscalls triggering a snapshot for some queries (i. e., cases ❷
and ❹).

❶
---
❷
---
❸
---
❹
---
Figure 3: Mapping I/O sequences to snapshots. We depict four cases ❶-❹,
snapshot events are shown on the left and I/O on the right. We indicate
read/input events in red, write/output events in blue, state changes in
yellow, and connection close events in green. ❶ shows the case where snapshots
and state changes are trivially aligned with I/O. ❷ shows the case where a
state change occurs without a corresponding output event. ❸ shows the case
where state changes occur after output events. ❹ shows the case where a state
change occurs after the last input event, with no output before the connection
is closed.

For all scenarios, we trigger _input_ event snapshots after _read_ -like
syscalls return, and _output_ event snapshots just before _write_ -like
syscalls execute. We take additional snapshots for _output_ events before each
read-like syscall. This enables us to always capture state changes, even if no
corresponding _write_ -like syscall occurs, or the state change happens after
the output is observed.

If there is no output to the final input of a query $q$, then we instruct the
learner to pose an additional query with an extra input, $q||i$ for all $i\in
I$. We expect there to be a read event corresponding to the final input of one
of these queries—thus providing us with a snapshot of the state after
processing the penultimate input. If the SUT does not perform such a read, i.
e., it stops processing new input, as in case ❹, we detect this by
intercepting syscalls related to socket closure, and inform the learner that
exploration beyond this point is unnecessary.

###  5.2 Identifying Candidate State Memory

In the first stage of learning, our objective is to identify a set of possible
memory locations whose values represent state (Definition 1), i. e., $M$. Our
analyses aim to find $M$ such that the only locations it contains are values
that can be used to discern if we are in a given state, for all possible
protocol states that the SUT can be in.

Snapshot Generation To form an initial approximation of $M$, we perform
bootstrap queries against the SUT, this produces a set of memory snapshots
where all of the memory which tracks state is defined and used (Assumption 3).
Our bootstrap queries take the form, $BF=\\{b_{0},b_{1},...b_{n}\\}$, where
$b_{i}\in I^{+}$. The first of these queries $b_{0}$ is set as the happy flow
of the protocol. This is the expected normal flow of the protocol execution,
which we assume prior knowledge of. For example, in TLS 1.2,
$b_{0}=(ClientHelloRSA,\allowbreak ClientKeyExchange,\allowbreak
ChangeCipherSpec,\allowbreak Finished)$. The other queries in $BF$ are
specific mutations of this happy flow, automatically constructed with the
intention of activating error states, timeout states, and retransmission
behaviour. Each of these queries $b_{x}$ is derived by taking all prefixes
$p_{x}$ of the happy flow $b_{0}$, where $0<|p_{x}|\leq|b_{0}|$, and for all
inputs in $I$, and appending to $p_{x}$ each $i\in I$ a fixed number of times
$T$ such that $b_{x}=p_{x}||i^{T}$.

Every bootstrap query is executed at least twice, so that we have at least two
snapshots for each equivalent input sequence, which we require for the next
step of our analysis. When compared to black-box approaches, one might assume
that our method requires many more queries in order to facilitate learning.
This is not the case. In fact, once we identify a SUT’s state memory, we can
reuse all of the bootstrap queries for refining our model in subsequent
phases.

When possible, we also attempt to alternate functionally equivalent input
parameters to the SUT across bootstrap flows. We do this to maximise the
potential number of locations we eliminate due to not holding the same value
at equivalent states (Assumption 3). For example, for TLS implementations, we
execute some bootstrap flows with different server certificates, which enables
us to eliminate memory that would otherwise have to be identified as non-
state-defining using our concolic analyser—a comparatively heavyweight
procedure.

❶
---
❷
---
❸
---
Figure 4: Allocation alignment across different executions. Each large block
represents the memory layout of a different protocol run; coloured squares
represent state-defining locations. Allocation alignment computes a mapping of
allocations of a given run (blue squares) to a _base_ configuration (red
squares). Using this mapping, we can _diff_ snapshots that have different
configurations, e. g., ❶ and ❸, by first mapping them onto a common
configuration, i. e., ❷.

Handling Dynamic Memory To facilitate handling multiple simultaneous sessions,
client/server implementations generally allocate state memory on-demand. This
presents a challenge when identifying state-defining locations, as logically
equivalent allocations may not reside at the same offsets across different
protocol executions. To address this non-determinism, we compute a mapping of
each execution’s allocations to a single _base_ configuration. This enables us
to analyse all snapshots together with respect to a common configuration,
rather than pair-wise. Figure 4 visualises our approach. We first construct an
allocation log for each execution that records a timestamp, the stack pointer
(i. e., callee return address), and call parameters, of every call to a memory
allocation function (e. g., malloc and free). Then, to derive a mapping
between two logs, we _align_ their allocations/frees, by matching them on
their log position, allocation size, and calling context (recorded stack
pointer). We choose our _base_ configuration, or log, as the largest _happy
flow_ log, under the assumption that it will contain all allocations related
to state-defining locations for any possible session.

Snapshot Diffing Following mapping each bootstrap snapshot’s allocations onto
the _base_ log, we _diff_ them to obtain our candidate set $M$. Each element
$m\in M$ corresponds to the location of a contiguous range of bytes of
dynamically allocated memory, which we represent by: an allocation address, an
offset relative to the start of the allocation, and a size.

We perform diffing by first grouping all snapshots by their associated I/O
sequences. Then, for each group, we locate equivalent allocations across
snapshots and identify allocation-offset pairs which refer to byte-sized
locations with the same value. We then check that every identified location
also contains the same value in every other I/O equivalent snapshot, and is a
non-default value in at least one snapshot group (Assumption 3). This gives us
a set of candidate state memory locations. We note that as this process is
carried out at the byte level, we additionally record all bytes that do not
abide by this assumption. This enables us to remove any misclassified bytes
once we have established the real bounds of individual locations (Section
5.3.1).

###  5.3 Minimising Candidate State Memory

Given our initial set of candidate state memory locations, we reduce $M$
further by applying the following operations:

  1. 1.

Pointer removal: we eliminate any memory containing pointers to other
locations in memory. We do this by excluding values which fall within the
address-space of the SUT and its linked libraries.

  2. 2.

Static allocation elimination: we remove any full allocations of memory which
are assigned a single value in the first snapshot which does not change
throughout the course of our bootstrap flows.

  3. 3.

Static buffer elimination: we remove any contiguous byte ranges larger than 32
bytes that remain static.

Static allocation and buffer elimination are used to filter locations
corresponding to large buffers of non-state-defining memory, for example, in
OpenSSL, they eliminate locations storing the TLS certificate.

####  5.3.1 Candidate State Memory Type-Inference

The values stored at state-defining locations are often only meaningful when
considered as a group, e. g., by treating four consecutive bytes as a 32-bit
integer. Since we perform snapshot diffing at a byte-level granularity, we may
not identify the most-significant bytes of larger integer types if we do not
observe their values changing across snapshots. As learning the range of
values a location can take is a prerequisite to determine some kinds of
termination behaviour, we attempt to monitor locations with respect to their
intended types.

To learn each location’s bounds, we apply a simple type-inference procedure
loosely based upon that proposed by Chen et al. [9]. We perform inference at
the same time as we analyse snapshots to handle uncertain state memory
locations (Section 5.5). During this analysis, we simulate the SUT’s execution
for a fixed window of instructions, while doing so, we analyse loads and
stores from/to our candidate state memory. To perform inference, we log the
prefixes used in each access, e. g., in mov byte ptr [loc_1], 0, we record
byte for loc_1. Then, following our main snapshot analysis, we compute the
maximal access size for each location and assign each location a corresponding
type. To disambiguate overlapped accesses, we determine a location’s type
based on the minimal non-overlapped range. For example, if we observe that
loc_1 and loc_1+2 are both accessed as 4-byte values, we compute loc_1’s type
as two bytes and loc_1+2 as four bytes. Following type-inference, we update
our model and the state classifications maintained by our learner using the
new type-bounds discovered.

###  5.4 State Merging

2
---
3
---
1
---
4
---
6
---
7
---
5
---
cke /
---
empty
---
appdata /
---
empty
---
cke /
---
empty
---
appdata /
---
empty
---
appdata /
---
empty
---
cke /
---
closed
---

Figure 5: An example scenario where merge conditions for states 1 and 2 are
met, when D is set to 1. The state learner would as such taint test any
differing memory between the two states to estimate if this memory is state
defining.

We consider a unique assignment of candidate state memory a unique state
(Definition 2). Hence two states reachable by the same inputs, with equivalent
assignments for these locations can be considered equal and merged. However,
by applying a trivial equality check, if $M$ is not minimal, i. e., it is an
over-approximation, this check may not yield the correct outcome. Which, in
the worst case could lead to non-termination of learning. We therefore must
address this to ensure learning is possible in all cases with respect to
Assumption 1, namely that the state machine being learned is finite. The
method we present in this section handles this possibility by allowing for
states to be merged under the assumption that our candidate set contains
superfluous locations. We attempt to merge states in the model each time all
queries in the queue of a given length have been performed. We call this the
merge check. It operates by identifying pairs of base and merge states, which
can be merged into a single state. These pairs are selected such that two
properties hold: ❶ the merge state must have I/O equivalence to the base, and
❷ the merge state should be reachable from the base. I/O equivalence signifies
all input-output pairs are equal for the two states, to a depth $D$. The
intuition is that if I/O differences have not manifested in $D$ steps, they
may in fact be the same state, and we should therefore check if the
differences in their memory are state relevant. The base-to-merge state
reachability must also be possible in $D$ steps (Assumption 4). We enforce
this property based on the observation that in security protocol
implementations, state duplication is more likely with states along the same
path. So-called loopback transitions often occur where inputs are effectively
ignored with respect to the state, however their processing can still result
in some changes to memory, resulting in duplication for our memory classified
states. Loops in models between multiple states are less common, but will be
checked by our learner provided the number of states involved is less than or
equal to $D$.

In Figure 5, we present an example of where the mergeability properties hold,
with $D=1$ for states 1 and 2—they are I/O equivalent to depth 1, and state 2
is reachable from state 1. Our merge check determines whether the memory that
distinguishes the states is state-defining. Algorithm 1 (see Appendix) shows a
sketch of our approach. In summary, for each location of differing memory, and
for each input message (to ensure completeness), we monitor the execution of
the SUT. We supply it with input messages to force it into the state we wish
to analyse (i. e., state 1 or 2 in our example in Figure 5), we then begin to
monitor memory reads to the tracked memory location. We follow this by
supplying the SUT with each input in turn and perform context snapshots on the
reads to the memory location, which we call a watchpoint hit. We then supply
each of these snapshots as inputs to our concolic analyser (detailed in the
next section), which determines if the SUT uses the value as state-defining
memory (Assumption 5). If our analysis identifies any location as state
defining, then we do not perform a merge of the two states. Conversely, if all
tested locations are reported as not state-defining, then we can merge the
merge state into the base state, and replace the transition with a self loop.

###  5.5 Handling Uncertain State Memory

Forming our candidate set $M$ by computing the differences between snapshots
gives us an over-approximation of all of the locations used discern which
state the SUT is in. However, an implementation may not use all of these
locations to decide which state it is in for every state. As described in the
previous section, when testing if two memory configurations for the same I/O
behaviour should be considered equivalent, we must identify if differing
values at candidate locations imply that the configurations correspond to
different states (i. e., the differing locations are state-defining), or if
the values they take are not meaningful for the particular state we are
checking. For a given state, by analysing how locations actually influence
execution we can easily tell state-defining locations from those that are not,
as in all cases, non-state-defining locations will have no influence on how
state is updated. Since this kind of analysis is expensive, the diffing phase
is crucial in minimising the number of candidate locations to
analyse—typically reducing the number to tens, rather than thousands.

####  5.5.1 Properties Of State-Defining Memory

To confirm a given location is state-defining, we attempt to capture execution
traces of its location behaving as state-defining memory. We summarise these
behaviours below, which we base on our analysis of various implementations:

  1. 1.

Control-dependence: writes to state memory are control-dependent on reads of
state memory. To illustrate this, consider the typical case of a state enum
flag read forming the basis of a decision for which code should process an
incoming message, and the resulting state machine transition defined by a
write to state memory.

  2. 2.

Data-dependence: non-state memory that is conditionally written to due to
dependence on a read from state memory may later influence a write to state
memory.

  3. 3.

State-defining and state-influential locations: for a particular state, its
state-defining memory locations (Definition 2) will always be read from before
they are written to (to tell which state one is in), and subsequent writes to
state memory will be control- or data-dependent upon the values of those reads
(Assumption 5). For state-influencing locations, e. g., input buffers, this
property will not hold—while the contents of a buffer may influence state, it
will not directly define it, and will be written to before being read.

####  5.5.2 Discerning State-Defining Locations

❷ check
---
backdoor depth
---
❸ skip check of
---
verify result
---
❹ perform state
---
change
---
❶ verify result
---
stored in eax
---
Close
---
Connection
---
Figure 6: OpenSSL client verification bypass. At ❶ we check the client
certificate signature, at ❷ we check if the read_seq counter is equal to 11,
if so, we bypass the check of the result of client certification verification
via ❸. At ❹ we perform a state update that is control-dependent on read_seq’s
value. StateInspector identifies the dependence and dynamically adjusts the
learning depth to discover the deep-state change.

If a location holds more than one value when performing a merge check, we
apply an additional analysis to determine if it is state-defining. First, we
identify execution paths that are control-dependent on the value stored at the
location. Then, we check if any of those paths induce a write to known state
memory. If so, we classify the location as state-defining.

We base our analysis on a variation of byte-level taint propagation combined
with concolic execution. We apply it in sequence to state snapshots taken on
reads of the candidate location $addr$. We start analysis from the instruction
$pc$ performing the read that triggered the state snapshot. Our analysis
proceeds by tainting and symbolising $addr$, then tracing forwards until we
reach a branch whose condition is tainted by $addr$. If we do not reach a
tainted conditional within $W$ instructions, we do not continue analysing the
path. At the conditional, we compute two assignments for the value at
$addr$—one for each branch destination. We then symbolically explore each of
the two paths until we have processed $W$ instructions or we reach a return
instruction. If we observe a write to known state memory on either path, we
consider $addr$ to be state-defining. Figure 6 depicts an example location
that requires such analysis. The counter read_seq is used to implement a
sneaky backdoor that bypasses client certificate verification in OpenSSL. Our
analysis finds that read_seq taints the branch jz update_state, and thus,
leads to a state change. We therefore classify it as state-defining.

We select an analysis bound of $W=512$ based on the observation that reads
from memory involved in comparisons tend to have strong locality to the
branches they influence. Since we analyse multiple state snapshots for each
$addr$, generated for every possible input in $I$, we reduce the chance for
missing locations used in state-defining ways outside of our bound. In
practice, we find that our selection of $W$ leads to no false negatives, and
note that it can be configured to a larger value to handle problematic
implementations.

##  6 Implementation

Our resulting implementation [1] consists of a Java-based learner, a ptrace-
based [7] execution monitor, and test harnesses in Python and Java. Our
concolic analyser is built using Triton [31] and IDA Pro [24]. In total,
StateInspector consists of over 10kloc across three different languages.

##  7 Results

In this section, we present the evaluation of our approach, StateInspector,
with respect to the research questions outlined in Section 3. To this end, we
test the implementations of two security protocols, TLS and WPA/2. We
additionally carry out tests on a intentionally modified TLS implementation,
as well as a number of purpose-built protocols.

We address RQ1 by demonstrating that our approach makes it possible to learn
models with both large input sets and identify the presence of deep states in
our purpose built protocols and OpenSSL. In doing so, we also show how grey-
box observations make it possibly to target and optimise learning (RQ2),
thereby avoiding cases of futile state exploration which degrade black-box
learning performance. Finally, in order to illustrate the additional insights
over I/O that our method affords (RQ3), we discuss our findings regarding the
disparity between I/O and memory state classifications of two OpenSSL
implementations, as well as an investigation of troublesome state memory in
Hostap.

Table 2: Model learning results on TLS 1.2 and WPA/2 servers. TLS experiments
are repeated with two alphabets, core and extended. Times specified in hours
and minutes (hh:mm). Experiments which did not terminate within 3 days are
denoted: $\blacksquare$.

|  Protocol |  Implementation | Classifying Mem. |  Mem. States |  I/O States |  Total Queries |  I/O Mem. Queries |  Watchpoints |  Total Time | Black-Box
---|---|---|---|---|---|---|---|---|---|---
|  |  |  Locations |  Allocations |  |  |  |  |  Queries |  Hits |  |  Queries |  Time
Core Alpha. |  TLS 1.2 |  RSA-BSAFE-C 4.0.4 |  88 |  14 |  11 |  9 |  128 |  109 |  19 |  4 |  00:06 |  204k |  $\blacksquare$
|  TLS 1.2 |  Hostap TLS |  159 |  32 |  11 |  6 |  194 |  160 |  34 |  17 |  00:24 |  971 |  01:48
|  TLS 1.2 |  OpenSSL 1.0.1g |  126 |  16 |  19 |  12 |  488 |  280 |  208 |  116 |  00:18 |  5819 |  00:42
|  TLS 1.2 |  OpenSSL 1.0.1j |  125 |  16 |  13 |  9 |  291 |  165 |  126 |  23 |  00:10 |  1826 |  00:13
|  TLS 1.2 |  OpenSSL 1.1.1g |  126 |  6 |  6 |  6 |  88 |  86 |  2 |  0 |  00:02 |  175 |  00:02
|  TLS 1.2 |  GnuTLS 3.3.12 |  172 |  7 |  16 |  7 |  265 |  129 |  36 |  42 |  00:10 |  1353 |  00:21
|  TLS 1.2 |  GnuTLS 3.6.14 |  138 |  7 |  18 |  8 |  973 |  452 |  522 |  121 |  00:36 |  3221 |  00:52
Ext. Alpha. |  TLS 1.2 |  RSA-BSAFE-C 4.0.4 |  165 |  7 |  14 |  7 |  918 |  688 |  230 |  635 |  01:08 |  133k |  $\blacksquare$
|  TLS 1.2 |  OpenSSL 1.1.1g |  467 |  66 |  11 |  11 |  535 |  524 |  11 |  0 |  01:05 |  1776 |  01:25
|  TLS 1.2 |  OpenSSL 1.0.1g |  554 |  110 |  40 |  20 |  2454 |  1816 |  594 |  609 |  04:21 |  20898 |  21:05
|  TLS 1.2 |  GnuTLS 3.3.12 |  185 |  5 |  23 |  19 |  1427 |  1274 |  153 |  128 |  02:05 |  66k |  $\blacksquare$
|  TLS 1.2 |  GnuTLS 3.6.14 |  157 |  6 |  13 |  11 |  730 |  673 |  57 |  37 |  01:32 |  66k |  $\blacksquare$
|  WPA/2 |  Hostap 2.8† |  138 |  3 |  24 |  6 |  1629 |  804 |  825 |  261 |  03:30 |  2127 |  03:30
|  WPA/2 |  IWD 1.6 |  135 |  8 |  5 |  5 |  264 |  126 |  138 |  597 |  01:02 |  3000+ |  08:00+

$\dagger$ For Hostap, we stopped both learners at ~200 minutes, as we found
that its state machine is infinite and would prevent both approaches
terminating.

Figure 7: Learned model for OpenSSL 1.0.1g

###  7.1 TLS

We evaluate the interesting examples of TLS 1.2 servers from the work of de
Ruiter et al. [18], the latest versions of these servers, and both the server
and client implementations of Hostap’s internal TLS library. This spans 4
different code bases, and 7 unique implementations. We learn these models with
two separate input sets, one containing the core TLS messages (as in de Ruiter
et al.), and where possible, another with a much larger input set, including
client authentication and multiple key exchanges (as provided by the TLS-
Attacker test harness [35]). Table 2 lists the time taken to learn all models,
as well as the identified candidate state memory details, query statistics and
number of states identified. Further, we list the number of queries required
to learn the same models with state-of-the-art black-box learning, i. e., the
TTT algorithm [26] with the modified W-Method equivalence checking of [18]
with a conservative equivalence checking depth of 3. For practical reasons, we
cut off black-box experiments after 3 days if they show no sign of approaching
termination.

####  7.1.1 OpenSSL

We tested a number of different versions of OpenSSL, ranging from 2014 to
2020. Of particular interest is the OpenSSL server running version 1.0.1g. A
state machine for this implementation was presented at Usenix 2015 [18]. It
modelled a previously discovered critical vulnerability: specifically, if a
ChangeCipherSpec (CCS) message was sent before the ClientKeyExchange, the
server would compute the session keys using an empty master secret. Prior to
finalising our model, which we depict in Figure 7, we replicated the notably
different model presented in [18], by using an identical test harness. As
described in Section 3, this harness sent invalid Finished messages on paths
with more than one ClientHello. This results in a model where the dashed green
path (s0, s2, s6, s16, s13, s11) and dotted red path (s0, s2, s7, s18, s15) in
Figure 7 always lead to an Alert and connection closure after receiving the
final input. As this was a test harness configuration issue, we sought to use
StateInspector in order to confirm this fact. In Table 3 (Appendix B), we list
the differences in memory between states on alternative paths to handshake
completion, and the known happy flow state s4. These differences were
identified once learning had terminated. As merge conditions were never met
for these states, we carried out a post-analysis stage, where we used
StateInspector to determine whether the differing memory defined the
respective states. We found that it did not. Despite these states sharing
different I/O definitions, when compared to state s4, all were equivalent in
terms of state-defining memory, thus indicating that the test harness was
responsible for the differences. This example also illustrates where I/O
interpretation by the test harness is misleading. States s15 and s17, which
manifest due to the aforementioned early-CCS vulnerability, are also
equivalent to the happy flow state s4. The I/O difference in this case is due
to the fact that the test harness cannot decrypt the response (hence
DecryptError). We note that this post-learning analysis does not come for
free, therefore, we only execute such checks when further model investigation
is needed.

When testing client authentication with the extended alphabet, we also
discovered inconsistencies in the documentation, which, at worst, have the
potential to cause vulnerable misconfigurations. We discuss this further in
Appendix D.

####  7.1.2 RSA-BSAFE-C

We selected this implementation as it serves to demonstrate that our method is
applicable not just to open-source implementations, but also to closed-source.
The implementation demonstrates a further advantage of our approach over
black-box learning. In particular, we observe that each time the server sends
an Alert message, it performs a partial socket shutdown. Specifically, it
executes a shutdown(n, SHUT_RD) on the connection with the test harness. This
means that it no longer accepts input, however, this is not detectable by the
test harness. For our approach, this is not a problem; we can observe the
shutdown syscall and prevent further inputs from this point. For black-box
learning, the socket closure is not detected, and so learning continues
exploring beyond the receipt of an Alert message. As shown in Table 2, this
leads to many superfluous queries, and, as a result, the learner fails to
terminate within 3 days for either alphabet. In comparison, our algorithm is
able to learn the same models with 128 queries in 6 minutes for the core TLS
functionality, and in ~1 hour for a more complex model capturing client
authentication and alternative key exchanges. Notably, this latter test
revealed that repeated ClientHello’s are only permitted when the server is
configured with forced client authentication.

####  7.1.3 GnuTLS

Our tests on the TLS server implementations in GnuTLS 3.3.12 and 3.6.14 showed
substantial changes between the two versions. In particular, each version
required us to hook different syscalls for snapshotting. State count also
differed, especially so when testing with the extended alphabet. Analysis of
the models revealed slightly different handling of Diffie-Hellman key
exchanges, which in the older version resulted in a path of states separate
from RSA key exchange paths.

The difference in learning performance between the two approaches, in the case
of the extended alphabet, was profound. Black-box learning failed to terminate
after 3 days and over 60k queries. We found that this was due to multiple
states and inputs warranting empty responses. Consequently, black-box learning
exhausted its exploration bound, trying all possible combinations of the
troublesome inputs at the affected states. In contrast, as shown in Table 2,
StateInspector is able to handle such cases much more effectively. This is in
part because some groups of inputs are found to result in equivalent
snapshots, and when the state equivalence is not immediately evident, our
merging strategy quickly finds memory differences are inconsequential.

####  7.1.4 Hostap-TLS

We tested Hostap’s internal TLS library as both a client and server. Although
this library is described as experimental, it is used in resource-constrained
Wi-Fi devices with limited flash space [13] and by Wi-Fi clients in embedded
Linux images created using Buildroot [8], e. g., motionEyeOS [15].

Surprisingly, we found that this TLS library always sends TLS alerts in
plaintext, which might leak information about the connection. Further, some
frames from the extended alphabet, such as Heartbeat requests or responses
were not supported, and sending them resulted in desynchronisation of the TLS
connection. We therefore do not include learning results for this
implementation with the extended alphabet.

More worrisome, the model showed that against a client, the ServerKeyExchange
message can be skipped, meaning an adversary can instead send ServerHelloDone.
The client will process this message, and then hits an internal error when
sending a reply because no RSA key was received to encrypt the premaster
secret. When Ephemeral Diffie-Hellman is used instead, the client calculates
$g^{cs}$ as the premaster secret with $s$ equal to zero if no
ServerKeyExchange message was received. Because the exponent is zero, the
default math library of Hostap returns an internal error, causing the
connection to close, meaning an adversary cannot abuse this to attack clients.
Nevertheless, this does illustrate that the state machine of the client does
not properly validate the order of messages.

###  7.2 WPA/2’s 4-Way Handshake

We also tested WPA/2’s 4-way handshake which is used to authenticate with Wi-
Fi networks. There are two open source implementations of this handshake on
Linux, namely the ones in IWD (iNet Wireless Daemon) and Hostap, and we test
both.

To learn the state machine, we start with an input alphabet of size 4 that
only contains messages which occur in normal handshake executions. Our test
harness automatically assigns sensible values to all of the fields of these
handshake messages. To produce larger input sets, we also tried non-standard
values for certain fields. For example, for the replay counter, we tried the
same value consecutively, set it equal to zero, and other variations. To this
end, we created two extended alphabets: one of size 15 and another one of size
40.

To also detect key reinstallation bugs [39], we let the SUT send an encrypted
dataframe after completing the handshake. In the inferred model, resulting
dataframes encrypted using a nonce equal to one are represented using
`AES_DATA_1`, while all other dataframes are represented using `AES_DATA_n`. A
key reinstallation bug, or a variant thereof, can now be automatically
detected by scanning for paths in the inferred model that contain multiple
occurrences of `AES_DATA_1`.

One obstacle that we encountered is handling retransmitted handshake messages
that were triggered due to timeouts. Because this issue is orthogonal to
evaluating our memory-based state inference method, we disabled
retransmissions, and leave the handling of retransmissions as future work.

####  7.2.1 IWD

We found that the state machine of IWD does not enter a new state after
receiving message 4 of the handshake. This means an adversary can replay
message 4, after which it will be processed by IWD, triggering a key
reinstallation. Note that this is not a default key reinstallation, i. e., we
confirmed that existing key reinstallation tools cannot detect it [38]. The
discovered reinstallation can be abused to replay, decrypt, and possibly forge
data frames [39]. We reported this vulnerability and it has been patched and
assigned CVE-2020-NNNNN [5]. When running our tool on the patched version of
IWD, the state machine enters a new state after receiving message 4, which
confirms that the vulnerability has been patched.

With black-box testing, the key reinstallation is only found when using a
small input alphabet _and_ when the test harness always sends handshake
messages with a replay counter equal to the last one used by the AP. If the
harness instead increments the replay counter after sending each handshake
message, the key reinstallation can only be discovered when using an extended
alphabet. However, in that case black-box learning takes much longer: after 3
hours the learner creates a hypothesis model that includes the vulnerability,
but it is unable to verify this hypothesis within 8 hours (at which point we
terminated the learner). This shows that our method handles larger input
alphabets more efficiently, especially when queries are slow, resulting in
more accurate models and increasing the chance of finding bugs.

####  7.2.2 Hostapd

One obstacle with Hostapd is how the last used replay counter in transmitted
handshake messages is saved: our learner initially includes this counter in
its candidate state memory set. When trying to merge states with different
replay counter values, our concolic analysis determines this value to be state
defining. Indeed, Hostapd checks whether incoming frames include a particular
value. However, with each loop of the state machine, the expected value
changes, and hence the learner prevents the merge. This results in a violation
of Assumption 1, meaning learning will not terminate. Like with other
violations of assumptions, we addressed this by including a time bound on the
learning. Because of this we also do not explore a bigger alphabet. For a fair
comparison, we used the same time bound in our method and in black-box
learning. The models which were produced with both approaches within ~200
minutes were equivalent. Under these conditions, we note that both resulting
state machines followed the standard and contained no surprising transitions.

###  7.3 Example Protocols

In order to highlight the capability of StateInspector to identify states deep
in a protocol, we test a minimally modified version of OpenSSL, in addition to
a variety of example protocols. We note that states in protocols beyond
typical learning bounds are not only theoretical—a state machine flaw in a
WPA/2 router [36] found a cipher downgrade was possible after 3 failed
initiation attempts (which would have been missed with configured bounds less
than 3, as in [18]).

Our modification of OpenSSL (version 1.0.1j), consists of a 4 line addition
(Appendix C, Listing 8), which hijacks existing state data to implement a
simple client authentication bypass, activated by $n$ unexpected messages (see
Figure 6 of Section 5.5.2). To learn this model, we used an extended alphabet
of 21 messages, including core TLS functionality, client certificates, and
various data frames. With $n=5$, black-box learning configured with a bound
equal to $n$, fails to identify the state after 3 days of learning and ~100k
queries (and showed no signs of doing so soon). StateInspector, on the other
hand, identifies the main backdoor-activation state in under 2 hours and ~1.2k
queries and the second activation variant (with two preceding ClientHellos, as
opposed to the usual one) in under 3 hours and ~2.5k queries. Doubling the
depth $n$ results in 3.2k and 4k queries respectively—an approximately linear
increase. Black-box learning predictably failed to locate the even deeper
state due to its exponential blow up in this particular scenario.

Our motivating example protocol of Section 3, Figure 1 also showed a dramatic
advantage over black-box learning, even with a simple model and small input
alphabet. We implemented this protocol similarly to a real protocol, with
state maintained between an enum and counting integer combined. With black-box
learning, this model took 360k queries and 20 hours to identify the auth-
bypass but failed to terminate its analysis after 4 days. StateInspector
identified the backdoor in 149 queries in just over minute, with the concolic
analyser taking up 20 seconds of that time.

##  8 Discussion

We have shown that relaxing the restriction of pure black-box analysis
improves practical model learning: we can learn new types of states and gain
more insights, all in less time. While we have shown our assumptions make a
justifiable trade-off between practicality and completeness, we acknowledge
that they may not hold for all protocol implementations. Thus, in this
section, we discuss possible limitations.

If the machine is not finite (Assumption 1), then, like black-box methods, our
approach will fail to terminate. Likewise, with respect to Assumption 4, if
loops within a state machine exist beyond the configured depth bound, and the
memory across these states is always changing (e. g., a counter), then
StateInspector will interminably duplicate states. In both of these cases,
like black-box methods, we provide a means to bound exploration. We choose to
bound by a configurable time, but this can also be done by exploration depth.
In the worst case, the resulting models will be no less representative than
those learned with black-box methods. False negatives due to missed candidate
state memory and concolic analysis also have the potential to be problematic.
As a consequence of Assumption 3, we may miss candidate locations if they do
not change during any bootstrap flow. An example of this kind of memory is one
allocated only after entering an error state. Fortunately, our results and
analysis of implementation code indicate that this assumption holds for most
protocols.

An inherent requirement of grey-box analysis is the ability to introspect a
program’s execution state. Whilst we ensure this is performed as non-
invasively as possible, it does limit the types of SUT which can be tested.
For example, our method would not be appropriate for protocols running on
certain types of embedded device, e. g., EMV cards. However, for devices with
sufficient debug access, e. g., JTAG, StateInspector could be used to learn
implementations for which black-box learning proves to be too slow.

Finally, although StateInspector is designed to work with both closed and
open-source implementations, it is often the case—as with most of our tested
protocols—that we do have access to source code. If this is the case, our tool
is able to map uses of state memory to source code locations—which
substantially aids in the analysis of inferred models.

##  9 Future Work

One key contribution of StateInspector is its ability to identify the
structures within a program which are used to maintain its runtime state.
Further, locations within the program which manipulate state memory can also
be easily identified. Recent works in the domain of fuzzing (protocols [10,
28] and more general software [6, 19]) have sought to combine program state
coverage with traditional CFG block coverage for fuzzing feedback. These
efforts have hitherto required a manual specification of state changing
locations—something we believe can be aided by the approaches of
StateInspector.

##  10 Conclusion

Black-box testing is fundamentally limited because it can only reason about
how a SUT interacts with the outside world. On the one hand, this means that a
large number of queries are required to learn state machines even for simple
protocols, and on the other, because we have no insight into _how_ the SUT
processes inputs, we cannot optimise queries to trigger or avoid certain
behaviours.

In contrast, our grey-box approach, StateInspector, overcomes many of these
issues. It is able to efficiently handle larger input spaces and protocols
that trigger state changes at non-trivial depths, resulting in more accurate
and insightful models, that can be learned in substantially fewer queries. As
testament to this, we were able to discover a new, high impact vulnerability
in IWD, and numerous concerning deviations from the standards in other
implementations.

## References

  * [1] StateInspector (URL obscured for anonymous review).  https://github.com/XXXX/YYYYY.
  * [2] Fides Aarts, Joeri De Ruiter, and Erik Poll.  Formal models of bank cards for free.  In Software Testing, Verification and Validation Workshops (ICSTW), 2013 IEEE Sixth International Conference on, pages 461–468. IEEE, 2013\.
  * [3] Fides Aarts, Julien Schmaltz, and Frits Vaandrager.  Inference and abstraction of the biometric passport.  In International Symposium On Leveraging Applications of Formal Methods, Verification and Validation, pages 673–686. Springer, 2010.
  * [4] Dana Angluin.  Learning regular sets from queries and counterexamples.  Information and computation, 75(2):87–106, 1987.
  * [5] Anonymous.  Iwd: CVE-2020-NNNNN (details obscured for anonymous review).
  * [6] Cornelius Aschermann, Sergej Schumilo, Ali Abbasi, and Thorsten Holz.  Ijon: Exploring deep state spaces via fuzzing.  In 2020 IEEE Symposium on Security and Privacy (SP), pages 1597–1612. IEEE, 2020.
  * [7] Erik Bosman.  ptrace-burrito.  Retrieved 3 September 2020 from https://github.com/brainsmoke/ptrace-burrito, 2020.
  * [8] Buildroot Association.  Buildroot.  Retrieved 3 September 2020 from https://buildroot.org/, 2020.
  * [9] Peng Chen and Hao Chen.  Angora: Efficient fuzzing by principled search.  In 2018 IEEE Symposium on Security and Privacy, 2018.
  * [10] Yurong Chen, Tian Lan, and Guru Venkataramani.  Exploring effective fuzzing strategies to analyze communication protocols.  In Proceedings of the 3rd ACM Workshop on Forming an Ecosystem Around Software Transformation, pages 17–23, 2019.
  * [11] Chia Yuan Cho, Domagoj Babic, Pongsin Poosankam, Kevin Zhijie Chen, Edward XueJun Wu, and Dawn Song.  Mace: Model-inference-assisted concolic exploration for protocol and vulnerability discovery.  In USENIX Security Symposium, volume 139, 2011.
  * [12] Tsun S. Chow.  Testing software design modeled by finite-state machines.  IEEE transactions on software engineering, (3):178–187, 1978.
  * [13] CodeApe123.  Hostapd porting and use.  Retrieved 9 January 2021 from https://blog.csdn.net/sean_8180/article/details/86496922, 2020.
  * [14] Paolo Milani Comparetti, Gilbert Wondracek, Christopher Kruegel, and Engin Kirda.  Prospex: Protocol specification extraction.  In Security and Privacy, 2009 30th IEEE Symposium on, pages 110–125. IEEE, 2009.
  * [15] Calin Crisan.  motioneyeos.  Retrieved 3 September 2020 from https://github.com/ccrisan/motioneyeos, 2020.
  * [16] Lesly-Ann Daniel, Erik Poll, and Joeri de Ruiter.  Inferring openvpn state machines using protocol state fuzzing.  In 2018 IEEE European Symposium on Security and Privacy Workshops (EuroS&PW), pages 11–19. IEEE, 2018.
  * [17] Joeri de Ruiter.  A tale of the openssl state machine: A large-scale black-box analysis.  In Nordic Conference on Secure IT Systems, pages 169–184. Springer, 2016.
  * [18] Joeri De Ruiter and Erik Poll.  Protocol State Fuzzing of TLS Implementations.  In USENIX Security, volume 15, pages 193–206, 2015.
  * [19] Andrea Fioraldi, Daniele Cono D?Elia, and Davide Balzarotti.  The use of likely invariants as feedback for fuzzers.  In Usenix, editor, USENIX 2021, 30th USENIX Security Symposium, 11-13 August 2021, Virtual Conference, 2021.
  * [20] Paul Fiterău-Broştean, Ramon Janssen, and Frits Vaandrager.  Combining model learning and model checking to analyze tcp implementations.  In International Conference on Computer Aided Verification, pages 454–471. Springer, 2016.
  * [21] Paul Fiterau-Brostean, Bengt Jonsson, Robert Merget, Joeri de Ruiter, Konstantinos Sagonas, and Juraj Somorovsky.  Analysis of DTLS implementations using protocol state fuzzing.  In 29th USENIX Security Symposium (USENIX Security 20), pages 2523–2540. USENIX Association, August 2020.
  * [22] Paul Fiterău-Broştean, Toon Lenaerts, Erik Poll, Joeri de Ruiter, Frits Vaandrager, and Patrick Verleg.  Model learning and model checking of ssh implementations.  In Proceedings of the 24th ACM SIGSOFT International SPIN Symposium on Model Checking of Software, SPIN 2017, pages 142–151. ACM, 2017\.
  * [23] Hugo Gascon, Christian Wressnegger, Fabian Yamaguchi, Daniel Arp, and Konrad Rieck.  Pulsar: Stateful black-box fuzzing of proprietary network protocols.  In International Conference on Security and Privacy in Communication Systems, pages 330–347. Springer, 2015.
  * [24] Hex-Rays.  Ida pro.  Retrieved 3 September 2020 from https://www.hex-rays.com/products/ida/, 2020.
  * [25] Falk Howar, Bengt Jonsson, and Frits Vaandrager.  Combining black-box and white-box techniques for learning register automata.  In Computing and Software Science, pages 563–588. Springer, 2019\.
  * [26] Malte Isberner, Falk Howar, and Bernhard Steffen.  The ttt algorithm: a redundancy-free approach to active automata learning.  In International Conference on Runtime Verification, pages 307–322. Springer, 2014.
  * [27] Malte Isberner, Falk Howar, and Bernhard Steffen.  The open-source learnlib.  In International Conference on Computer Aided Verification, pages 487–495. Springer, 2015.
  * [28] Roberto Natella and Van-Thuan Pham.  Profuzzbench: A benchmark for stateful protocol fuzzing, 2021.
  * [29] Oliver Niese.  An integrated approach to testing complex systems.  PhD thesis, Universität Dortmund, 2003.
  * [30] Van-Thuan Pham, Marcel Böhme, and Abhik Roychoudhury.  Aflnet: a greybox fuzzer for network protocols.  In 2020 IEEE 13th International Conference on Software Testing, Validation and Verification (ICST), pages 460–465. IEEE, 2020.
  * [31] QUARKSLAB.  Triton.  Retrieved 3 September 2020 from https://triton.quarkslab.com/, 2020\.
  * [32] Harald Raffelt, Bernhard Steffen, and Therese Berg.  Learnlib: A library for automata learning and experimentation.  In Proceedings of the 10th international workshop on Formal methods for industrial critical systems, pages 62–71. ACM, 2005.
  * [33] Timo Schrijvers, FW Vaandrager, and NH Jansen.  Learning register automata using taint analysis.  Bachelors Thesis, 2018.
  * [34] Muzammil Shahbaz and Roland Groz.  Inferring mealy machines.  FM, 9:207–222, 2009.
  * [35] Juraj Somorovsky.  Systematic fuzzing and testing of tls libraries.  In Proceedings of the 2016 ACM SIGSAC Conference on Computer and Communications Security, pages 1492–1504, 2016.
  * [36] Chris McMahon Stone, Tom Chothia, and Joeri de Ruiter.  Extending automated protocol state learning for the 802.11 4-way handshake.  In European Symposium on Research in Computer Security, pages 325–345. Springer, 2018.
  * [37] Martin Tappler, Bernhard K Aichernig, and Roderick Bloem.  Model-based testing iot communication via active automata learning.  In 2017 IEEE International conference on software testing, verification and validation (ICST), pages 276–287. IEEE, 2017.
  * [38] Mathy Vanhoef.  Krack attack scripts.  Retrieved 30 January 2020 from https://github.com/vanhoefm/krackattacks-scripts, 2021.
  * [39] Mathy Vanhoef and Frank Piessens.  Key Reinstallation Attacks: Forcing Nonce Reuse in WPA2.  In Proceedings of the 24th ACM Conference on Computer and Communication Security. ACM, 2017.

##  Appendix A Algorithm to Generate Watchpoint Hit Snapshots

Result: list of $watchpointHitExecutionDumps$

Input: $(addr,size)$ of memory to test, prefix query $p$ to arrive at
$mergeState$, the $SUT$

foreach  _$(input,st)\in reachableFrm(mergeState,1)$_ do

if  _$outputFor(input,st)\in disabled$_ then

$continue;$

end if

$initialiseWatchpointMonitor(SUT,addr,size)$;

$executeQuery(SUT,p||input)$;

end foreach

Algorithm 1 Generation of watchpoint hit snapshots.

##  Appendix B OpenSSL State Memory Analysis

Table 3: The sets of differing memory for states on suspected and confirmed alternate paths to successful handshake completion, when compared to the legitimate happy flow state 4 (s4) memory. State IDs |  | Addresses of differing memory to s4
---|---|---
s14 |  {22mm[] {112mm[] | {0x555555a162a0, 0x4b0, 0x13}
|  | {0x555555a162a0, 0x4b0, 0x120}
|  | {0x555555a162a0, 0x4b0, 0x0}
|  | {0x555555a0e6b0, 0x160, 0x0}
|  | {0x555555a0e6b0, 0x160, 0x10}
s15, s17, s13 |  | {0x555555a0e6b0, 0x160, 0x44}
|  | {0x555555a0e6b0, 0x160, 0x68}
|  | {0x555555a0e6b0, 0x160, 0x6c}
|  | {0x555555a0e6b0, 0x160, 0xc0}
|  | {0x555555a0e6b0, 0x160, 0xc8}
|  | {0x555555a0e6b0, 0x160, 0xd2}

Using the learning output of StateInspector, we carried out an investigation
into what the differing memory in Table 3 actually constituted. We were able
to do this by referring to the logs produced by the tool, which print the
source code details of any watchpoint hits made at reads of the tested memory.
All considered states shared the two differing addresses listed at the top of
the table. The first of these represented a counter referred to as the
sequence number. This value increments for each message received after the
ChangeCipherSpec message and is used for constructing MACs. The second address
in the table refers to the frame type of the just received message. This value
is determined as not state defining because from any given state it is always
written to before being read, i. e., it may be state influencing, but not
defining (ref. 5.5.1). The third address in the table pertains to a flag which
determines if the client has attempted more than one ClientHello message. Only
prior to the receipt of a ClientKeyExchange is this flag ever read (and
therefore used to define the state). Consequently, it is not considered state
defining for any of the states listed in the table. The remaining memory
refers to arbitrary certificate data which we also found was not state
defining. In particular, we were unable to detect any reads of the memory from
the states considered.

##  Appendix C OpenSSL Client Authentication Bypass Backdoor

A four line modification to OpenSSL 1.0.1j, which introduces a client
authentication bypass at a configurable depth (BACKDOOR_DEPTH). In the first
part, we hijack a counter, the read_sequence counter, and conditionally
increment it each time an unexpected data frame is read whilst waiting on the
ClientCertificateVerify signature. In the second part, if this counter reaches
the specified depth value, invalid ClientCertificateVerify signatures are
ignored, and the handshake proceeds to the ChangeCipherSpec state. After this
point, the read_sequence is automatically reset by the implementation for use
in later MAC calculations.

⬇

|\setcounter{FancyVerbLine}{138}|

@@ /ssl/s3_pkt.c:139 ssl3_read_n()

SSL3_BUFFER *rb;

+++ // Backdoor pt 1: Set-up

+++ if(s->state == SSL3_ST_SR_CERT_VRFY_A)

+++ ++(*s->s3->read_sequence);

\parif (n <= 0) return n;

rb = &(s->s3->rbuf);

|\setcounter{FancyVerbLine}{682}|

@@ /ssl/s3_srvr.c:683 ssl3_accept()

ret=ssl3_get_cert_verify(s);

\--- if (ret <= 0) goto end;

+

+++ // Backdoor pt 2: Activation

+++ if(*s->s3->read_sequence != BACKDOOR_DEPTH

+++ && ret <= 0) {

+++ goto end;

+++ } else {

...

s->state=SSL3_ST_SR_FINISHED_A;

s->init_num=0;

+++ }

##  Appendix D Misleading OpenSSL Documentation

When testing the built-in server of OpenSSL, we found that configuring it to
enforce client authentication is rather error-prone. In particular, after an
initial reading of the documentation for how to do so, we came across the
option below:

    -verify int, -Verify int
        The verify depth to use. This specifies the
        maximum length of the client certificate
        chain and makes the server request a
        certificate from the client. With the
        -verify  option a certificate is requested
        but the client does not have to send one,
        with the -Verify option the client must
        supply a certificate or an error occurs.

Following this, we used the -Verify option when starting the built-in server.
Surprisingly though, our learned models indicated that the server accepted
invalid client certificates. At first glance, this looked like a severe
vulnerability, however, upon closer inspection of the documentation we found
an extra option was required:

    -verify_return_error
        Verification errors normally just print a
        message but allow the connection to
        continue, for debugging purposes. If this
        option is used, then verification errors
        close the connection.

Our online investigation revealed we were not alone in our confusion. A recent
Github issue222https://github.com/openssl/openssl/issues/8079 describes the
same misleading configuration, and resulted in a patch to the OpenSSL client
implementation333https://github.com/openssl/openssl/pull/8080. Unfortunately,
a similar patch was not written for the server implementation, resulting in a
confusing disparity between the command-line options for the client and
server. We have reported this issue to the OpenSSL developers.