PISE: Protocol Inference Using Symbolic Execution
and Automata Learning
Ron Marcovich

Orna Grumberg

Gabi Nakibly

Technion - Israel Institute of Technology{ron.mar,orna,gnakibly}@cs.technion.ac.il

Abstract—Protocol Inference is the process of gaining information about a protocol from a binary code that implements it. This
process is useful in cases such as extraction of the command andcontrol protocol of a malware, uncovering security vulnerabilities
in a network protocol implementation or verifying conformanceto the protocol’s standard. Protocol inference usually involves
time-consuming work to manually reverse engineer the binarycode.
We present a novel method to automatically infer statemachine of a network protocol and its message formats directlyfrom the binary code. To the best of our knowledge, this is thefirst method to achieve this solely based on a binary code ofa single peer. We do not assume any of the following: accessto a remote peer, access to captures of the protocol’s traffic,
and prior knowledge of message formats. The method leverages
extensions to symbolic execution and novel modifications toautomata learning. We validate the proposed method by inferring
real-world protocols including the C&C protocol of Gh0st RAT,a well-known malware.

I. I NTRODUCTION
The process of gaining information about a communication
protocol from the binary code that implements it is called
Protocol Inference. Such a process is employed in several practical scenarios. Many malwares set up a command and control(C&C) channel with the attacker’s server. Over that channel
they receive commands from the server and send information
gathered from the victim machine. Oftentimes, knowing thecommands expected to be received by the malware is helpful
to analyze the goals and logic of the malware. Nonetheless,these commands may not be easily obtained if no prior trafficof the C&C channel has been captured or the attacker server
is no longer operational. In such cases one needs to infer the
C&C protocol from the malware’s binary only.
Additionally, security vulnerabilities of a network protocol
software are often caused by deviations from the intended
protocol’s logic. For example, a vulnerability in an implementation of a server program may accept data from theclient before the user was authenticated or after a message
that closes the connection is received. Such deviations may
be even intentional and pose an undesirable back door to theWorkshop on Binary Analysis Research (BAR) 2023
3 March 2023, San Diego, CA, USA
ISBN 1-891562-84-3
https://dx.doi.org/10.14722/bar.2023.23002
www.ndss-symposium.org

program. Moreover, improper implementation of a protocol
logic may lead to non-conformance to other implementationsof the same protocol. To reveal such improper implementationsof a protocol, one needs to infer the protocol implemented by
the software and compare it to the protocol’s desired logic.
In this work we propose PISE: a method to automaticallyinfer the protocol directly from a given binary code. The
method extracts the protocol state machine and the formats ofeach of the protocol’s message types. The method leverages
an extended L* algorithm [2] to learn the protocol’s statemachine.
L* is based on a Teacher and a Learner, whose goal isto reveal the state machine of an unknown language (in ourcase, the sequences of the protocol’s message exchanges). The
Learner presents membership queries and equivalence queries
that the Teacher answer.
To answer the algorithm’s membership queries we use
modified symbolic execution of the binary program. The modifications track the program’s network activity and guide thesymbolic execution through a messages exchange according
to the Learner’s query. The symbolic execution is also leveraged to uncover messages that may follow a valid message
exchange. Predicates representing the protocol’s message types
are derived based on these example messages. As new message
types are revealed they are fed back to the L* algorithm toextend the protocol’s state machine. Equivalence queries of
the L* algorithm are answered using a standard sampling
approximation using membership queries.
We emphasize that the only input to the proposed method isthe binary code of a single peer of the protocol. In particular,
we do not assume: (1) Access to the binary code of the remotepeer. (2) Access to network traffic recordings that containvalid protocol sessions. (3) Access to an online instance of theremote peer. Namely, we cannot recreate valid session traffic.
(4) Prior knowledge of messages’ formats and the partition tomessage types.
To the best of our knowledge, PISE is the first protocol
inference method that has none of the above assumptions. We
believe that the lack of such assumptions makes our method
widely suitable for many real-world use cases of protocol
inference. For example, often when the C&C protocol of a
malware is analyzed, the protocol peer, i.e. the C&C server, isunobtainable nor it is online, furthermore past malware traffic
has not been recorded. Hence, the binary code of the malware
is the only source of information about the protocol.

II. P REVIOUS W ORKS

III. P RELIMINARIES
A. Deterministic Finite Automaton (DFA) Learning
A deterministic finite automaton (DFA) M is a five-tuple,(Q, Σ, δ, q0 , F ), all of them nonempty, whereas: Q is a finite
set of states, Σ is a finite set of input symbols (alphabet),δ : Q × Σ → Q is a transition function, q0 ∈ Q is an initialstate and F ⊆ Q is a set of accept states. Let w = σ1 ...σnbe a string over the alphabet Σ. We say that M accepts w
if there exist r0 , ..., rn ∈ Q such that r0 = q0 , rn ∈ F and∀0 ≤ i ≤ n − 1, ri+1 = δ(ri , σi+1 ).
Let Σ∗ = {σ1 ...σn | σi ∈ Σ, n ≥ 0} be the set of all
finite strings over the alphabet Σ. We define L(M ) = {w ∈Σ∗ | M accepts w} as the language of M . A set of words
L ⊆ Σ∗ is a regular language iff there exists DFA M suchthat L = L(M ).
Automata learning identifies an unknown regular language
L by learning a DFA M such that L(M ) = L. The L*
algorithm [2] solves this problem. It assumes a minimallyadequate Teacher, which is an oracle that can answer two
types of queries: Membership query and Equivalence query.
In a Membership query, the Teacher should indicate whether
a given word w is in L or not. In an Equivalence query, theTeacher should indicate, given a conjectured DFA M ′ , whether
L(M ′ ) = L, and provide a counterexample otherwise (a wordin the symmetric difference of L and L(M ′ )).
In its internal data, the L* algorithm saves a description of
the currently learned automaton in a structure called observation table. The observation table is updated during the learning
process according to the answers of the Teacher.
The basic L* algorithm assumes Σ (alphabet) is known.
Several works [12] [13] propose extended algorithms to deal
with an alphabet that is revealed (or grows) during the execution of the algorithm.

There are several published works that deal with the problem of learning information about a network protocol. The
approach presented in [8] uses recorded network traffic as
input. It analyzes the traffic and uses heuristics to extract
different protocol fields.
To infer information about the protocol that may not be
captured in recorded traffic only, several methods [4] [3] [17][9] were introduced that combine the recorded traffic withexecution traces of the server, allowing them to learn more
about the messages’ formats, and even gain some insights
about the semantics of messages and message fields.
All of these works do not deal with the problem of learning
the protocol state machine. This was the motivation for thework [7] which introduced Prospex. This work extended
previous works in two directions: First, they developed amechanism to identify messages of the same type. They use
this information to partition messages with similar role in the
protocol into clusters. The second extension is a method toinfer the state machine of the protocol. Prospex method, likeall the mentioned methods, requires captures of protocol’s
traffic.
Another important contribution is the work [6] that introduced a method for on-line inference of botnet C&C protocol,using active instances of it. They chose to represent a protocol
as a Mealy machine and used L* extension by [14] for learning mealy machines. They actively query the control server
responses for a sequences of messages. They also introduced
caching and prediction optimizations to L* in order to reduce
the amount of membership queries sent to the server. Theirwork, as an on-line method, assumes the server is available
and answers appropriately. They also assume known message
formats by using previous work [4].
Another related work is the work [1] that introduces amethod to infer a Java class specification (order of method
calls) using model checking and L*, which is similar to what
we apply in our work. In their case, however, the alphabet (themethods) is known in advance. The work [10] utilizes L* forthe purpose of model checking and suggests learning-basedalgorithms to automate assumption generation in assumeguarantee verification. The work [12] even extended this toinclude alphabet refinement, a technique to infer interfacealphabets.
Another work called MACE [5] presents a method to learna state machine of a server using L* and symbolic execution.
They use L* extension for inferring Mealy state machines[14] and like our method, use symbolic execution to uncovermessages that the client may send. There are, however, twomain differences to our method: First, MACE assumes aknown abstraction function is available that can extract themessage type out of the server’s response. Second, MACE
assumes a running server is available, that can answer client
requests. We do not have these assumptions.

B. Symbolic Execution
Symbolic execution is a static method of analyzing a program. During the analysis it determines what constraints the
program’s input must satisfy in order to execute each execution
path in the program. This is done by following the program’s
code assuming symbolic values for inputs. A symbolic state isdefined to contain the current symbolic values for each variablein the program, as well as constraints that should hold in orderto reach that state.
Symbolic execution begins with a single initial state locatedat the entry point of the program. The execution happens
by stepping the set of states and generating new descendantstates. Stepping a single state may result with multiple newdescendant states, if, for example, the parent state corresponds
to a conditional branch. Before stepping a state, the symbolic
execution may verify that the current constraints of the state
are satisfiable. This verification is done in order to discard
states that represent infeasible paths, representing impossible
executions. A symbolic state can represent an execution during
which the program failed and terminated, namely exits with a
non-zero return value. We call such a symbolic state an abort
state.

2

types allowed from each state. Formally, L is regular
language. If L is not regular, our algorithm will fail orwill never complete the inference.

IV. P ROBLEM D EFINITION
Our goal, given a binary code of a program, is finding a DFA
that accepts a language L, where each word in L matches asequence of message types received and sent by the program.
We say that this DFA is the state machine of the protocol
implemented by the program. We say that a concrete run ofthe program is valid if and only if it does not finish in an abort
state.
We denote by S and R the finite set of messages that may
be sent and received by the program, respectively. S and R
are disjoint. S and R are finite because messages are limited
in length (See Assumption 1 below).
A session is a sequence of messages m1 . . . mk such that
∀1 ≤ i ≤ k, mi ∈ S ∪ R. We say that a session m1 . . . mk is
valid for the program if and only if there exists a valid run ofthe program along which the same sequence of messages aresent or received in exactly the same order as in m1 . . . mk . An
empty session is considered valid. Valid sessions are prefixclosed, meaning that if m1 . . . mk is a valid session then ∀1 ≤l ≤ k − 1, m1 . . . ml is also a valid session.
Messages are partitioned into subsets of message types
according to their semantics in the protocol and their effect on
the protocol state machine. Let TD be a partition of message
types of D where D ∈ {R, S}. Given a message m ∈ D,
we denote by type(m) the pair ⟨D, t⟩ such that t ∈ TD andm ∈ t. We call such a pair ⟨D, t⟩ a Message Type. t is finite
because both S and R are finite.
We define the alphabet of the protocol as a finite set ofpairs:
ΣL = {⟨D, t⟩ | t ∈ TD , D ∈ {R, S}}

V. L EARNING A DFA OF A P ROTOCOL (E XACT V ERSION )The learning of the protocol’s DFA is based on a modified
version of the L* algorithm [2]. We modify the algorithm’squeries in order to uncover the alphabet Σ, that is, the message
types of the protocol. Initially, Σ is ∅.
For ease of exposition, we assume here a Teacher that is
capable of answering the queries we present. However, thisassumption is unrealistic when both the state machine and thealphabet ΣL are unknown. In Section VI we propose suitableapproximations for the Learner and the Teacher.
1) Modified Membership Queries: The classical membership query returns T rue or F alse, indicating if a given w
is in L or not. We modify it as follows: If w ∈ L, T rue isreturned together with a set Cont(w) of message types ⟨D, t⟩such that w · ⟨D, t⟩ ∈ L. If w ∈/ L, F alse is returned. The setCont(w) may reveal new alphabet symbols.
2) Modified Equivalence Queries: In a classical equivalence query the Learner provides a conjectured DFA M overalphabet ΣM = Σ. T rue is returned if L = L(M ). Otherwise,
F alse is returned and a counterexample w in the symmetricdifference of L and L(M ) is returned as well. We modify it
as follows: F alse is returned if there exist w ∈ Σ∗M for which
one of the following hold: (1) w is in the symmetric differenceof L and L(M ); (2) A set M iss(M ) ̸= ∅ exists such that forall σ ∈ M iss(M ), σ ∈/ ΣM but w · σ ∈ L. In the former case,w is returned as a counterexample. In the latter case, every
w · σ is considered a counterexample. T rue is returned if for
all w ∈ Σ∗M , neither (1) nor (2) hold.
3) Handling a growing alphabet: Given a set of message
types C = Cont(w) or C = M iss(M ) output by a query, Σ
is set to Σ ∪ C. If Σ changes during this assignment, then we
say that the alphabet grows. To handle a growing alphabet we
use a modified L* algorithm presented in [13]. In a nutshell,
the modified algorithm updates the observation table to handle
the new alphabet symbols while the general learning cycle is
kept similar to the classical L* algorithm.
4) Initialization and Output: The Learner starts with Σ =∅. The first query of the Learner is w = ε. Note that theanswer to this query is T rue since an empty session is valid.
Cont(ε) is then added to Σ. The Learner continues to utilize
queries according to the L* algorithm and extends Σ and thelearnt DFA according to the queries’ answers. The algorithm
terminates when an equivalence query returns T rue. The
algorithm outputs the learnt DFA that represents the protocol’s
state machine and Σ that represents the protocol’s message
types.
5) Correctness: The correctness of the algorithm is basedon the modified definition of equivalence queries and correctness of the classical L* algorithm.
Theorem 1: The modified Learner terminates with L(M ) =L and ΣM = ΣL .

Given a session m1 . . . mk such that ∀1 ≤ i ≤ k, mi ∈ S ∪ R,
we define Θ : (S ∪ R)∗ → Σ∗L :Θ(m1 . . . mk ) = type(m1 ) . . . type(mk )We abstract all valid sessions to a regular language L over thealphabet ΣL :
L = {Θ(m1 . . . mk ) | m1 . . . mk is a valid session}
Note that L is prefix closed because valid sessions are prefix
closed. Note that R and S, as well as their partitions TS and
TR , are unknown in advance, hence the alphabet Σ of the DFA
in unknown in advance. It is the task of our method to uncoverΣL as it determines the DFA.
1) Assumptions: We assume the following about the input
to our method:
1) Message Length is limited: there exists N such thatno message in the protocol to be inferred is longer thanN bytes. This is a reasonable assumption since concrete
messages must be finite. In practice, our method allow
a message to be longer than N bytes, as long as thefirst N bytes may allow to infer its message type.
This assumption is required since symbolic lengths arecomputationally difficult to infer.
2) Protocol Regularity: the protocol can be modeled as a
DFA (See Section III-A) over ΣL in terms of message

3

Query w

Membership
Oraclew

DFA M
True/False
w, M issA (M )M(D, Pσ )Modified Symbolic Execution

True/False
ContA (w)

Binary CodeApproximated Learner

True/False
ContA (w)M(D, Pσ ∧ ¬P)
M(D, Pσ ∧ P)

M(D, P)

M(D, P ∧ ¬Pσ )Equivalence
OracleFig. 2. Colliding predicatesFig. 1. Illustration of our algorithm

we are given only a small subset of examples for that message
type.

Proof 1: The Learner terminates when it gets T rue as ananswer from the Teacher on an equivalence query. In this case,there is no w ∈ Σ∗M , which is in the symmetric difference of
L and L(M ). Thus, L = L(M ). Also, there is no w ∈ ΣM ∗ ,such that σ ̸∈ ΣM but w · σ ∈ L. This means that there is no(reachable) message type σ ∈ ΣL that has not been revealed
already by our modified Learner. Consequently, Σ = ΣL , asrequired. ■B. Handling Alphabet Changes
Recall that the exact version of our method is infeasible inour setting. To remedy this, we replace the sets of message
types, Cont(w) and M iss(M ), with their approximations,denoted ContA (w) and M issA (M ), of message type candidates.
As we use an approximation to generate the new message
type candidates, they may intersect with previously foundmessage types currently in Σ. This breaks the assumptionthat sets of message types are pairwise disjoint. Therefore,
we present here an algorithm that, given C = ContA (w) or
C = M issA (M ), incorporates C in Σ while making surethe elements of Σ remain pairwise disjoint. We denote by Σ
the current alphabet and by Σ′ the updated alphabet after thechanges. The algorithm initializes Σ′ = Σ.
Let c = ⟨D, P⟩ ∈ C be a message type candidate. We
say that ⟨D, P⟩ collides with ⟨Dσ , Pσ ⟩ ∈ Σ if Dσ = D
and M(D, P) ∩ M(D, Pσ ) ̸= ∅. In order to detect if ccollides with σ, we check the satisfiability of P ∧ Pσ . If acollision is detected, then ⟨Dσ , Pσ ⟩ is removed from Σ andthree message types are added to Σ′ : One that is based ona predicate of the intersection of the colliding message types
and two message types that are based on the a symmetricdifferences of the colliding message types (see Figure 2). The
procedure to handle collisions of a message type candidate cis presented in Algorithm 1.
Note that, if Σ originally includes only pairwise disjoint
message types, then it is guaranteed that message types⟨D, Pσ ∧ ¬P⟩ and ⟨D, Pσ ∧ P⟩ do not collide with any othermessage types in Σ. Therefore, it is only left to check forcollision with ⟨D, ¬Pσ ∧ P⟩ in Σ′ .
During the procedure we must discard unsatisfiable predicates. A predicate may become unsatisfiable in two special cases of collision: If M(D, Pσ ) ⊂ M(D, P ′ ) thenPσ ∧ ¬P ′ is not satisfiable and should be discarded (line 6).
If M(D, Pσ ) ⊃ M(D, P ′ ) then P ′ ∧ ¬Pσ is not satisfiable
and should not be inserted to Σ (line 13).
We run Algorithm 1 for every c ∈ C. After running thisprocedure for all message type candidates, the elements of
the resulting Σ′ are pairwise disjoint and are set as the newalphabet.

VI. L EARNING A DFA OF A P ROTOCOL (A PPROXIMATION )This section details how the answers to the queries of themodified L* algorithm presented in Section V are approximated. The components of the learning and their interactions
are presented in Figure 1.
A. Characterizing Message Types
Recall that a message type is a pair ⟨D, t⟩ where t is aset of finitely many messages. We represent a set t using
a predicate P describing the format of that message type.
Hence, we represent a message type by a pair ⟨D, P⟩. We
use predicates over variables {B0 , . . . , BN −1 }, representing
the message bytes. Recall that N is a maximal length of amessage (See Section IV-1). m[i] denotes the value of the i-thbyte of m, such that 0 ≤ m[i] < 256. We define M(D, Px ) tobe the set of messages from D that is matched by the predicate
Px :M(D, Px ) = {m ∈ D | Px (m) = T rue}
Given a set of messages x ⊆ D, Px is extracted using thefollowing simple definition: we hold constraints on message
bytes that have the same value for all the messages in x.
Formally, let m ∈ x, we define ∀0 ≤ i ≤ N − 1:
Bi = m[i], if ∀m′ ∈ x, m′ [i] = m[i]φi =T rue,
Otherwise
And Px is defined as:
Px =

N^
−1

φi

i=0

Note that the above definition may be replaced with a moreelaborate one, if needed. We choose this definition because it issimple and is sufficiently useful for many real world protocols.
In Section VI-E2c we explain how to generate predicates thatare sufficiently general to describe message types even though4

Algorithm 1 The procedure to handle message type candidate
1: function HANDLE CANDIDATE(⟨D, P⟩ ∈ C, Σ)
2:P ′ ← P, Σ′ ← Σ3:for all ⟨Dσ , Pσ ⟩ ∈ Σ′ such that D = Dσ do
4:
if Pσ ∧ P ′ is satisfiable then5:Σ′ ← Σ′ \ {⟨D, Pσ ⟩}6:
if Pσ ∧ ¬P ′ is satisfiable then7:Σ′ ← Σ′ ∪ {⟨D, Pσ ∧ ¬P ′ ⟩}8:
end if9:
Σ′ ← Σ′ ∪ {⟨D, Pσ ∧ P ′ ⟩}10:
P ′ ← P ′ ∧ ¬Pσ
11:
end if
12:
end for13:
if P ′ is satisfiable then14:Σ′ ← Σ′ ∪ {⟨D, P ′ ⟩}15:
end if16:
Σ ← Σ′
17: end function

Algorithm 2 Approximation of equivalence queries
1: function RUN TEST SUITE(M , T ⊂ Σ∗M)
2:
for all w ∈ T do
3:⟨w ∈ L, ContA (w)⟩ ← membership(w)4:
if w ∈ L then5:
if ContA (w) \ ΣM ̸= ∅ then6:
return ⟨F alse, w, ContA (w) \ ΣM ⟩7:
end if8:
if w ∈/ L(M ) then9:
return ⟨F alse, w⟩
10:
end if
11:
else if w ∈ L(M ) then12:
return ⟨F alse, w⟩
13:
end if14:
end for15:
return T rue
16: end function

In order to link between a sequence of alphabet symbols andthe binary code, we propose modifications, which we apply on
top of classical symbolic execution. Some other modifications
are required in order to find ContA (w) during a phase of thesymbolic execution called probing.
1) Assumptions and assertions in symbolic execution: We
simulate assumptions and assertions using symbolic execution
constraints and using the fact that symbolic execution checks
the satisfiability of states during the execution and discards unsatisfiable executions. We insert assumptions to the constraintsof a symbolic state when we want to restrict the considered
executions to executions that satisfy the assumptions. Conflicting constraints or concrete values will cause the execution
to become unsatisfiable and discarded. Similarly, we insert
assertions to the constraints of a symbolic state when we want
to restrict the considered executions to executions where boththe constraints developed by the symbolic execution and allof the assertions are satisfiable.
2) Hooking calls to send and receive functions: Hooking
calls in symbolic execution allows to replace the behaviour of abinary code in certain functions with customized procedures.
When hooks are applied and a state s represents a call toa hooked function, the customized procedure is executed ons instead of the original function. The customized procedure
should return a state that represents the program after the callto the function.
When we apply symbolic execution on the binary, we hookfunctions that send or receive messages in order to monitor
a sequence and to discover message type candidates. These
functions are replaced with customized procedures which we
describe in VI-E. For simplicity of exposition, we assume
there is a single send function and a single receive function.
However, the presented method can be equally implemented
in case there are several such functions.
We ask the user of our method to manually identifyfunctions that send and receive messages. The user should
also specify for each function whether it is a send function

If during the above procedure message types are removed
from Σ then the L* algorithm must be restarted with the updated Σ since the learning was done with inaccurate alphabet.
If message types are only added to Σ (and not removed) thenwe say that Σ grows. In the latter case the method fromthe exact algorithm (Section V-3) is used without having torestart L*.
C. Equivalence Oracle
Answering equivalence queries in real world for black box
systems is generally infeasible [2]. Therefore, we define here
an oracle to approximate equivalence queries. We take advantage of a commonly used approach in which an equivalence
query is approximated using a sampling oracle. We use the
Wp-Method [11] to generate a test suite T ⊂ Σ∗M of queries
w. In this method, T is generated using M and the alphabet
ΣM .
The procedure to run a test suite T against a conjectured
DFA M is shown in Algorithm 2. Each w ∈ T is tested using
a membership query. If ContA (w) contains symbols that are
not in ΣM , then F alse is returned with w and M issA (M ) =ContA (w). If w is in the symmetric difference of L andL(M ), then F alse is returned with w as a counterexample. If
missing message types are not found and a counterexample w
is not found in the entire test suite T , T rue is returned andthe learning terminates. Recall that, if M issA (M ) is returned,
then every w · σ, such that σ ∈ M issA (M ), is handled as acounterexample.
D. Modified Symbolic Execution
Our algorithm answers membership queries by symbolic
execution of the binary code. During the symbolic execution
we need to find feasible executions in which the binary code
follows a given sequence of alphabet symbols. We call thisprocess monitoring the sequence. To monitor a sequence, we
introduce assertions and assumptions into symbolic execution.

5

It is initialized with Ds = ∅ and set only during the first
send or receive in the probing phase.

or a receive function. Identifying these functions is mostof the times simple and require a small manual effort by
the user of our method. Send and receive functions share acommon property that they call the send or receive system
calls. Therefore, these functions are easy to find with classicalreverse engineering and disassemble tools. In case the user
cannot find these functions, he can choose to provide the send
and receive functions of the operating system.
When a send or a receive function is called within a states and our customized procedures are executed, it is necessary
to extract the message from s. Therefore, in addition to
identifying the functions to hook, the user should provide acode snippet that extracts the message from the symbolic states that represents the call to these function. The code snippetthat the user provides will most likely get the message fromthe parameters of the call. Note that inferring this code snippet
manually is considered trivial.
3) Extending symbolic states to track query state: Letw = σ1 . . . σn be a sequence of alphabet symbols queried
in a membership query. Let s be a symbolic state. Recall thedefinition of symbolic state from Section III-B. We extend
the definition of s to contain additional properties. We use
these properties to track which alphabet symbols from thesequence have been sent or received in the execution that s
represents, from the initial state and up to s. In addition, we
add to s properties that will be used during the probing phaseof the query. The properties we add are propagated from every
state to its descendant states. Properties are set and updated
explicitly in certain steps of our algorithm as we will describein Section VI-E.
a) Properties for monitoring: We extend s to store in
addition to the original properties:• A sequence ws = σ1 . . . σn . The sequence, and especially its predicates, are used to insert assumptions andassertions during the symbolic execution, to limit theconsidered executions to executions that match the query.
• An index is such that 0 ≤ is ≤ n. This index marks theindex of the last symbol monitored in the execution whenreaching s. That is, the sequence σ1 . . . σis was sent or
received in the execution up to s. is is incremented by
one every time a send or receive that match σis +1 occurs
in the execution. If is = n, the entire sequence ws wasmonitored in the execution represented by s.
When the symbolic execution is initialized to answer amembership query w, the initial state s is defined with ws = w
and is = 0.
b) Properties for probing: When a state s is executedduring the probing phase, we use two additional properties
that we add to s:• A symbolic value msgs . msgs is initialized during thefirst send or receive call that occurs in the probing phase.
It is initialized with the symbolic value sent or received.
msgs will be used to generate a message type candidate
for s as we explain in Section VI-E2c.
• A flag Ds ∈ {R, S, ∅}, which specifies whether the firstcommunication in the probing phase was send or receive.

E. Membership Oracle
Let w ∈ Σ∗ be a sequence of message types sent as amembership query. The oracle should answer whether w ∈ L
and if w ∈ L it should also provide ContA (w) – a set of
message type candidates that may follow w. By definition, w
is a sequence of message types. Recall that such a sequencecorresponds to sessions of the protocol. We answer membership queries using symbolic execution of the binary code.
A symbolic execution begins with a single active initialstate, located at the binary’s entry point. By stepping forward
active states iteratively, a set of new active states is generated,
representing multiple different execution paths of the binary.
Recall that we divide the symbolic execution into two phases:
monitoring phase, which answers whether w is a valid sessionof the protocol, and the probing phase, which results inpossible continuations of w. The latter phase is executed only
if w is a valid session. During the monitoring phase we
guide the symbolic execution to consider only execution paths
that follow the given sequence w. During the probing phase,
however, we take into account all feasible executions that aredeveloped as continuations to the executions that we foundduring the monitoring phase.
1) Monitoring phase: Let w = ⟨Dσ1 , Pσ1 ⟩ . . . ⟨Dσn , Pσn ⟩be the queried sequence. We hook the functions in the binarythat send and receive messages as we described in Section VI-D. The procedures inserted in the hooks are presented
in the following subsections. We perform the monitoring phasein n stages: We start with a single initial state se located at
the binary code’s entry point with ise = 0 and wse = w. For
each stage 1 ≤ i ≤ n we add constraints of the predicateof the message type ⟨Dσi , Pσi ⟩. These constraints restrict thesymbolic execution to execution paths that send or receivea message of type ⟨Dσi , Pσi ⟩ at the current stage. We thenresume the execution of all active states, until all active states
are restricted to the i-th message type. In other words, we
begin a stage i with states that have is = i − 1 and finish itwith a set of new states with is = i. In the next subsections
we explain in detail how we eliminate execution paths that do
not match w. Recall that states with unsatisfiable constraints
as well as abort states, are discarded automatically.
If we successfully finish the execution of the last stage (fori = n) with at least one active state, then there is at least one
valid session of the binary code that matches the sequence of
message types of w. In such a case the answer to the query is
T rue. If, however, during one of the stages there are no active
states left, then w represents invalid session for the binarycode, and therefore the oracle returns F alse as the query’s
result.
In Figure 3, the monitoring phase is illustrated in the leftpart of the figure. States that represent infeasible executions(infeasible constraints) are discarded (gray). States that represent feasible executions that do not match the query w arediscarded as well (red). The stages of the monitoring are

6

Monitoring Phase

Probing Phase

Send⟨R, P1 ⟩ ∈ ContA (w)

Send⟨R, P2 ⟩ ∈ ContA (w)

Recv
se

Send

i=1

2...n − 1

⟨S, P3 ⟩ ∈ ContA (w)i=nFig. 3. Illustration of symbolic execution during membership query

Algorithm 3 The monitor procedure
1: function MONITOR (s, D ∈ {R, S})2:⟨Dσi , Pσi ⟩ = ws [is + 1]
3:
msg ← user code snippet(s)4:if Dσi = D then5:s′ ← s.copy()
6:
if D = R then7:
s′ .add assumption(Pσi (msg))
8:else if D = S then9:s′ .add assertion(Pσi (msg))
10:
end if11:
is′ ← is + 1
12:
return s′
13:
else
14:
return null15:
end if
16: end function

illustrated as well. The figure represents a membership querythat is answered with T rue, as a single active state (magenta)
is found at the end of the monitoring phase.
a) Monitoring incoming messages: The receive function
is hooked during the monitoring phase with the following
procedure. The purpose of this procedure is to advance themonitoring of the queried sequence when the binary code
receives a message. Let s be a symbolic state during the ith stage in which the binary code calls the receive function,and let σi = ⟨Dσi , Pσi ⟩ where i = is + 1 be the next expectedalphabet symbol in the query.
If σi represents outgoing messages (i.e Dσi = S), then s is
not an execution path that can match the queried sequence w:
the execution path represented by s receives a message in thei-th stage whereas the query w represents sessions that senda message from M(S, Pσi ) in the i-th stage. Therefore wediscard s.
On the other hand, if σi represents incoming message type(i.e Dσi = R), we move s to the i + 1-th stage with s′
as its successor and set is′ = i = is + 1. We attach tos′ an assumption that a message from M(R, Pσi ) is readfrom the network. We implement this assumption by inserting
the predicate Pσi (msg) to the constraints of s′ , where msg
is the received message buffer. We acquire msg using thecode snippet the user provides in order to extract it from s(See VI-D2).
Once s′ resumes execution, it will continue as if the received
message satisfies Pσi and thus ”forcing” descendant states tofollow only execution paths that represent the reception of
messages from M(R, Pσi ) during the i-th stage.
The pseudo-code in Algorithm 3 for D = R describes themonitoring process that occurs when the receive function iscalled from a state s in order to receive a message msg.
b) Monitoring outgoing messages: The procedure tohook a send function is similar to the one used above forincoming messages. The purpose of the procedure is to perform the monitoring of the queried sequence when the binary
code sends a message. Let s be a symbolic state in which thebinary code calls the send function, and let σi = ⟨Dσi , Pσi ⟩where i = is + 1 be the next expected alphabet in the query.

In case σi represents incoming messages (i.e Dσi = R), itmeans that the execution path of s does not match the sequencequery w and we discard s. On the other hand, if σi represents
an outgoing message type (i.e Dσi = S), we move s to the i+
1-th stage with s′ as its successor and set is′ = i = is + 1. We
attach to s′ an assertion that a message from M(S, Pσi ) is sent
to the network. We implement this assertion by inserting thepredicate Pσi (msg) to the constraints of s′ , where msg is thesent message buffer. The procedure is presented in Algorithm 3
for D = S.
2) Probing phase: The purpose of the probing phase is togenerate ContA (w) for w for which the monitoring phasereturned T rue. As above, we hook the send and receivefunctions of the binary code but insert different procedures.
We describe them in the upcoming subsections. The aimof the probing procedure is to uncover all symbolic statesthat represent execution paths in which a message is sent or
received following w. For each such state s the constraints
on the message buffer received or sent, denoted as msgs , arecollected.

7

Recall the definition of msgs and Ds from Section VI-D3b.
Given a state s in the probing phase, the purpose of thesehooks is to store msgs and Ds and trigger the generation of
message type candidates. We assume that all concrete values
for msgs in the context of state s belong to the same message
type and generate a message type candidate to represent it.
In Figure 3, the probing phase is shown in the right part of
the figure. Since the purpose of the probing phase is to discover
all message type candidates that can follow the sequence w, we
continue the execution from active states matching the queryw at the end of the monitoring phase (magenta). That is, stateswith is = n. A message type candidate c is generated fromevery state s (green), and added to ContA (w). We demonstrate
the probing of message type candidates in Appendix A.
a) Probing outgoing messages: The hooking procedureused in the send function is straightforward. Here msgs is thesent message’s symbolic buffer. We assume that the symbolic
buffer has enough constraints under the current state s thatsufficiently represent the sent message type. Therefore, nofurther symbolic execution is needed. We set Ds = S andmsgs = msg, where msg is the sent message. The state s
is then passed to the procedure to generate a message type
candidate.
b) Probing incoming messages: Let s be a state inwhich the binary code calls a receive function during the
probing phase. Let msg be the symbolic received message.
Upon calling receive, the content of msg is an unconstrained
symbolic value as it is received as an input to the binary
code. Hence, one cannot extract information on the formatof the message type that is expected to be received in states. To solve this, we present the following novel approach to
uncover information regarding the expected received message
type: we clone s to s′ with msgs′ = msg and Ds′ = R. Then
we resume symbolic execution of s′ . During this execution weassume that the binary code will parse the received message,
hence constraints will be developed on msgs′ that will reveal
the format expected by the binary code. We choose to resume
the execution until the binary code sends or receives anothermessage, or until the code terminates. We assume that untilthat point the code completes parsing the received message
and acts upon its content, hence sufficient constraints areaccumulated on the message buffer to identify the expected
message type to be received. During these instructions s′ isdeveloped into possibly multiple descendant states.
Let se be a descendant state of s′ in which either sendor receive function are called for the first time after s′ .
Alternatively, se is a descendant state of s′ in which the binary
code terminates. se represents a point of the binary code inwhich the incoming message is already analyzed and its typeis determined. Therefore it has passed through conditional
branches that append constraints on msgs′ . These constraints
will give us information on the structure of the message. seis then passed to the procedure to generate message type
candidate. When se has successfully generated a message type
candidate, it is removed from the set of active states to discontinue the execution path represented by se. This execution path

has already produced a message type that follows the queried
sequence and there is no need to resume its execution.
c) Generating message type candidates: Let s be a statethat successfully probed either sent or received message –msgs . The purpose of the procedure described here is togenerate a message type candidate from s. Note that concretevalues satisfying the constraints of s on msgs represent valid
messages in the protocol. We assume that these concrete messages form a message type t. We ask the symbolic execution
engine to solve msgs and generate N U M SOL1 possible
concrete values for msgs .
Let x be the set of generated concrete messages. We
extract Px as described in Section VI-A. Then, we iteratively
refine Px by trying to find concrete values m′ of msgs , that
contradict Px in a sense that ¬Px (m′ ) is T rue. Such m′ areconcrete values that can appear in msgs in a real execution(since they were solution to the msgs ). Nevertheless, they
are not represented by Px . In case we find such m′ , we addthem to x and regenerate Px . We repeat this process until thesolver is unable to find additional m′ that contradict Px . This
procedure allows us to find a set x ⊂ t that represents thevariety of t.
Recall our statement from Section VI-A regarding thediversity of the set x when generating Px . The proceduredescribed here uses a smaller, diverse enough set x to describea larger set M(Ds , Px ). M(Ds , Px ) approximates the set of
all concrete values of msgs .
Let concretize(s, buf f er, n, C) be a function of the symbolic execution engine that returns up to n concrete values
for buf f er that corresponds to the constraints of s andto additional constraints C. In case there are no possible
values that follow the constraints, the function returns ∅. The
pseudo-code of the message generation process is shown in
Algorithm 4.
Algorithm 4 Generation of message type candidate
1: function GENERATE ALPHABET CANDIDATE(s)
2:
x←∅
3:
contrads ← ∅4:do5:
Px ← extract predicate(x)6:contrads ← concretize(s, msgs , N U M SOL, ¬Px )7:x ← x ∪ contrads
8:
while contrads ̸= ∅9:
ContA (w) ← ContA (w) ∪ {⟨Ds , Px ⟩}10: end function
VII. O PTIMIZATIONS
We develop several optimizations to reduce the running timeof the method and allow it to scale to real-world protocol
implementations. These optimizations take advantage of thecharacteristics of network protocols and the algorithm itself.
Since symbolic execution is the most time consuming part of
1 In our implementation N U M

8SOL = 10the algorithm, the developed optimizations focus on reducing
the number of needed symbolic executions, as well as reducing
the running time of symbolic executions.
1) Prefix Closed Property: This optimization leverages thefact that the protocol’s regular language L is a prefix-closedset (See Section IV). It is based on a similar technique,employed in [13]. The optimization allows us to answer
some membership queries immediately by the Learner without
having to resort to symbolic execution. Every membership
query w that was answered with F alse is stored by themembership oracle in a cache. For every membership queryw sent to the oracle, it is first checked whether there exists
x, y ∈ Σ∗ such that xy = w and x is in the cache. In such acase, the query immediately returns F alse. In other words, if
a prefix of w is not in L, then by definition of prefix-closed
set it must hold that w ∈/ L. Thus, we avoid unnecessary
applications of symbolic execution.
When, during the discovery of new message types, analphabet symbol is removed and L* is restarted, all queries w
in the cache that contain a removed symbol are removed fromthe cache. These queries are invalid with the new alphabet andcannot be a prefix of a query over the new alphabet.
2) Fast Equivalence Queries: Let w ∈ Σ∗ be a queryfor which the membership oracle answered T rue, and let
ContA (w) be the returned set of alphabet candidates. We store
w and its associated ContA (w) in a cache called continuations
cache. The equivalence oracle answers an equivalence queryfor DFA M by utilizing this cache. The oracle checks consistency of M with the continuations cache: for every w in
the cache and for every σ ∈ ContA (w), it checks whether
M accepts w · σ. If M rejects w · σ, the equivalence oracle
returns F alse and returns w · σ as a counterexample. Thus
it alleviates the need to run symbolic execution to answer
the query. Note that, the cache stores alphabet symbols after
resolving collisions, and not message type candidates. This isnecessary so that the cache can return counterexamples overthe current alphabet. When alphabet symbol is removed, allcache entries containing the removed symbol are erased.
The correctness of this optimization follows from thedefinition of ContA (w). According to the definition, every
state machine M that claims L(M ) = L should satisfy
w · σ ∈ L(M ).
3) Execution Cache: This optimization uses symbolic statess resulting at the end of the monitoring phase for w as
initial states for query wx for any x ∈ Σ∗ . All queries w
for which the teacher returns T rue are stored in a cache
called ”Execution Cache” with all active symbolic states
resulting at the end of the monitoring phase for w. Then,
whenever a query w′ is sent, the teacher finds decompositionw′ = p.s, p = p1 . . . pk such that p is the longest word in
the cache. Then, the monitoring phase for w′ begins with thestates saved for p, in the i = k +1 stage of the monitoring. We
skip the first k stages because the states saved for p contains
exactly all execution paths for sessions p1 . . . pk . The rest of
the query remains the same as described in Section VI-E. We
note that, when alphabet symbols are removed, all entries in

the cache that include the removed symbol should also be
removed.
VIII. I MPLEMENTATION , R ESULTS AND E VALUATIONIn this section we present the details of our implementationof the presented method and explore its performance. We evaluated our method against various protocol implementations(including SMTP and other non-standard protocols), however
due to space constraints we present here only an evaluation
against Gh0st RAT’s C&C protocol.
A. Implementation
The algorithm was implemented2 as two independent modules for the Learner and the Teacher. The Learner is implemented as a Java program that communicates with the
Teacher using local socket. The Teacher is implemented asa Python program that serves the Learner’s queries. We baseour implementation on two open source tools: (1) LearnLib[13] – implements the L* algorithm and its variations (forexample, [14]); (2) angr [15] – a library that provides static
analysis and symbolic execution engine for binary codes.
1) Learning Client (Learner): The Learner begins by initializing a learning process with LearnLib’s implementationof L*. Membership queries are first checked with the prefixclosed cache (See Section VII-1). In case of a miss, the query
is sent to the Teacher. If the Teacher answers that w ∈ L,then ContA (w) is analyzed for new message types which are
added to Σ. Intersections between message types are handled
as described in Section VI-B.
Conjecture DFA is checked first against the continuations
cache as described in Section VII-2. If the conjectured DFA is
found to accept all continuations in the cache, an equivalence
query approximation is triggered. A test suite is generatedusing the Wp-Method [11] and is tested as explained in
Section VI-C. Missing message type are handled as describedin Section VI-B. Counterexamples are handled by the internal
implementation of L*.
We use the following features of LearnLib: Classical L*
implementation; Support for growing alphabet in L*; Test
suite generation with Wp-Method; Prefix-closed cache (See
Section VII-1). On the other hand, we implemented the following modifications: (1) Alphabet symbols as tuples ⟨D, P⟩; (2)Handling of alphabet changes and collisions (Section VI-B);(3) Continuations cache to support Fast equivalence queries.
(Section VII-2); (4) Running tests suites to approximate modified equivalence queries (Section VI-C).
2) Symbolic Execution Server (Teacher): Our Teacher runs
symbolic execution using angr, and is the only component thatinteracts with the binary code. The Teacher initializes symbolic
execution for the binary code and setups the hooking of thesend/receive functions the user provides. The Teacher receives
membership queries in a loop, until the Learner finishes thelearning. When a membership query is received, we firstcheck the execution cache optimization (See Section VII-3),
2 https://github.com/ron4548/pise9

Learning time:
Total Membership queries:
Total Equivalence queries:
Prefix-Closed cache miss rate:
Alphabet size:in case of a miss the monitoring phase executes as describedin Section VI-E. If the query results with T rue, the probing
phase runs and generates message type candidates. These
candidates are collected and sent back to the Learner.

142 seconds
45488
1
0.218445

TABLE IG H 0 ST RAT LEARNING STATISTICS

B. Gh0st RAT
Gh0st RAT is a well known malware3 . Once an instance of
Gh0st RAT is run on the victim’s computer, the attacker has
full control over the system. This includes access to the screen,
microphone and camera. The attacker controls the malware
using a C&C protocol. The source code of some variants of
Gh0st is available on the web. We chose to work with one ofthem4 . In this variant, the RAT runs in a multi-threaded process
which connects to the attacker’s server. When a command isreceived, a new thread and a new connection are created tohandle the command and its further communications.
Initially, we applied our method on this variant. However,angr [15] is not well-suited for multi-threaded programs. In
addition, angr does not fully support Windows API. This leadto difficulties with applying our method on the Gh0st RAT
binary directly. To validate that the proposed method caninfer a state machine as complex as that of Gh0st RAT, we
opted for a different approach. We re-implemented most of themalware’s C&C protocol with a simpler architecture that does
not involve threads. We applied our method on this program.
We provided our method with two functions that the program uses in order to send and receive messages from the
network: get_message and send_message. Both geta message buffer and its length. The full state machine iscomplex and contains 27 states and 52 transitions (without
rejecting states). We show the full state machine and thediscovered alphabet symbols in Appendix B.
In Figure 4 we show a branch of the state machine, that
handles a command to stream the camera of the victim. In
this branch, the attacker sends a command to open the camera
stream ([R] WEBCAM). Then, the client sends information
regarding the stream ([S] BMPINFO) and waits to receivefrom the attacker a command to begin streaming ([R] NEXT).
From now on, the client sends periodically a bitmap of the
webcam to the attacker’s server ([S] BMP). By default, thisbitmap is not compressed. The attacker can enable compression of the stream ([R] COMPR_ON) and disable it ([R]COMPR_OFF). When the compression is on, the bitmap issent compressed (COMPR_BMP).
Statistics of the learning process are shown in Table I.
45 message types were discovered. The learner issued about
45,000 membership queries; more than 78% of them wereanswered by the prefix-closed cache. Only a single equivalence
query was issued. This shows the dramatic effectiveness of thecontinuations cache to reduce the number of costly equivalence
queries. There are no discrepancies between the learnt DFA
and the protocol’s state machine.
IX. C ONCLUSIONSIn this work we present a novel method for inferring thestate machine of a protocol implemented by a binary with noa-priori knowledge of the protocol. Our method is based on
extended symbolic execution and modified automata learning.
The method assumes access to only the implementation of asingle peer of the protocol.
We implemented and validated our method on several protocols implementations. As demonstrated by the Gh0st RAT use
case, the method can infer complex protocols with dozens ofmessage types. Nonetheless, this use case also highlighted thatthe method will perform as a good as the symbolic execution
engine it relies on.

3 https://attack.mitre.org/software/S0032/
4 https://github.com/yuanyuanxiang/SimpleRemoter

start[R] COMPR OFF[R] COMPR ON[R] COMPR ON

q0

q1[R] WEBCAM

q2[R] NEXT

q3

q4[S] BMPINFO[R] COMPR OFF[S] BMP[S] COMPR BMP

Fig. 4. The branch in Gh0st RAT C&C protocol that handles webcam streaming. The letter in the square brackets indicates whether the message is sent or
received.

10

R EFERENCESA PPENDIX[1] R. Alur, P. Cerný, P. Madhusudan, and W. Nam, “Synthesis of interface specifications for java classes,” in Proceedings of the 32nd
ACM SIGPLAN-SIGACT Symposium on Principles of Programming
Languages, POPL 2005, Long Beach, California, USA, January 12-14,
2005, 2005, pp. 98–109.
[2] D. Angluin, “Learning regular sets from queries and counterexamples,”Inf. Comput., vol. 75, no. 2, pp. 87–106, 1987.
[3] J. Caballero and D. Song, “Automatic protocol reverse-engineering:
Message format extraction and field semantics inference,” Computer
Networks, vol. 57, no. 2, pp. 451–474, 2013.
[4] J. Caballero, H. Yin, Z. Liang, and D. X. Song, “Polyglot: automatic
extraction of protocol message format using dynamic binary analysis,”in Proceedings of the 2007 ACM Conference on Computer and Communications Security, CCS 2007, Alexandria, Virginia, USA, October
28-31, 2007, 2007, pp. 317–329.
[5] C. Y. Cho, D. Babić, P. Poosankam, K. Z. Chen, E. X. Wu, and D. Song,“MACE: Model-inference-Assisted Concolic Exploration for Protocol
and Vulnerability Discovery,” in Proceedings of the 20th USENIX
Security Symposium, 8 2011.
[6] C. Y. Cho, D. Babic, E. C. R. Shin, and D. Song, “Inference and analysis
of formal models of botnet command and control protocols,” in Proceedings of the 17th ACM Conference on Computer and Communications
Security, CCS 2010, Chicago, Illinois, USA, October 4-8, 2010, 2010,
pp. 426–439.
[7] P. M. Comparetti, G. Wondracek, C. Krügel, and E. Kirda, “Prospex:
Protocol specification extraction,” in 30th IEEE Symposium on Security
and Privacy (S&P 2009), 17-20 May 2009, Oakland, California, USA,2009, pp. 110–125.
[8] W. Cui, J. Kannan, and H. J. Wang, “Discoverer: Automatic protocol
reverse engineering from network traces,” in Proceedings of the 16th
USENIX Security Symposium, Boston, MA, USA, August 6-10, 2007,
2007.
[9] W. Cui, M. Peinado, K. Chen, H. J. Wang, and L. Irún-Briz, “Tupni:
automatic reverse engineering of input formats,” in Proceedings of the2008 ACM Conference on Computer and Communications Security, CCS
2008, Alexandria, Virginia, USA, October 27-31, 2008, 2008, pp. 391–
402.
[10] M. Emmi, D. Giannakopoulou, and C. S. Pasareanu, “Assume-guarantee
verification for interface automata,” in FM 2008: Formal Methods, 15th
International Symposium on Formal Methods, Turku, Finland, May 2630, 2008, Proceedings, 2008, pp. 116–131.
[11] S. Fujiwara, G. von Bochmann, F. Khendek, M. Amalou, andA. Ghedamsi, “Test selection based on finite state models,” IEEE Trans.
Software Eng., vol. 17, no. 6, pp. 591–603, 1991.
[12] M. Gheorghiu, D. Giannakopoulou, and C. S. Pasareanu, “Refining interface alphabets for compositional verification,” in Tools and Algorithms
for the Construction and Analysis of Systems, 13th International Conference, TACAS 2007, Held as Part of the Joint European Conferences on
Theory and Practice of Software, ETAPS 2007 Braga, Portugal, March
24 - April 1, 2007, Proceedings, 2007, pp. 292–307.
[13] M. Isberner, F. Howar, and B. Steffen, “The open-source learnlib,” inComputer Aided Verification, D. Kroening and C. S. Păsăreanu, Eds.
Cham: Springer International Publishing, 2015, pp. 487–495.
[14] M. Shahbaz and R. Groz, “Inferring mealy machines,” in FM 2009:
Formal Methods, Second World Congress, Eindhoven, The Netherlands,
November 2-6, 2009. Proceedings, 2009, pp. 207–222.
[15] Y. Shoshitaishvili, R. Wang, C. Salls, N. Stephens, M. Polino,
A. Dutcher, J. Grosen, S. Feng, C. Hauser, C. Krügel, and G. Vigna,“SOK: (state of) the art of war: Offensive techniques in binary analysis,”in IEEE Symposium on Security and Privacy, SP 2016, San Jose, CA,
USA, May 22-26, 2016. IEEE Computer Society, 2016, pp. 138–157.
[16] M. Weiser, “Program slicing,” IEEE Transactions on Software Engineering, vol. SE-10, no. 4, pp. 352–357, 1984.
[17] G. Wondracek, P. M. Comparetti, C. Krügel, and E. Kirda, “Automatic
network protocol analysis,” in Proceedings of the Network and Distributed System Security Symposium, NDSS 2008, San Diego, California,
USA, 10th February - 13th February 2008, 2008.

A. Example of probing message type candidates
To illustrate how a conditional branch reveals information
on a symbolic value, consider the pseudo-code in Listing 1 ofa binary code:
Listing 1. Pseudo-code to demonstrate the probing phase

1:
2:
3:
4:
5:
6:
7:
8:
9:
10:
11:

Send ( C o n n e c t ) ;msg = R e c e i v e ( ) ;i f ( msg == ” HelloV1 ” ) {Send ( ” I n i t V 1 ” ) ;...
} e l s e i f ( msg == ” HelloV2 ” ) {Send ( ” I n i t V 2 ” ) ;...
} else {abort ( ) ;}Assume a query w=⟨S, P⟩ where P=(B0 B1 B2 B3 B4 B5 B6 = ”Connect”). The monitoring phasefor this query and this binary code is done with a single
satisfiable state in line 2. The probing phase resumes thisstate. In line 2 the binary code receives msg in a state s.
msg refers to a symbolic value with no constraints, as it
is an input from the network. A state s′ = s is resumed
with msgs′ = msg. The execution splits according to theconditional branches: a state se1 represents execution at line 4
with a constraint that msg = ”HelloV1”, a state se2 represents
execution at line 7 with a constraint that msg = ”HelloV2”
and a state s3 represents execution at line 10 which aborts
and is discarded. Both se1 and se2 represent a call to send,
which triggers the generation of message type candidate from
msgse1 = msgse2 = msg. In the context of se1 , the analysis
is tied to the constraint msg = ”HelloV1” and generates amessage type candidate ⟨R, P1 ⟩ where:
P1 = (B0 B1 B2 B3 B4 B5 B6 = ”HelloV1”)
In the context of se2 the analysis is tied to the constraint msg =”HelloV2” and generates an alphabet symbol ⟨R, P2 ⟩ where:
P2 = (B0 B1 B2 B3 B4 B5 B6 = ”HelloV2”)
The set ContA (w) = {⟨R, P1 ⟩, ⟨R, P2 ⟩} is returned with theanswer that w ∈ L.
B. Gh0st RAT Inference Results
The full state machine learnt by applying our method on
Gh0st RAT C&C is presented in Figure 5. In the protocol amessage type is determined by the first byte of the message
and some message types provide additional information in thesecond byte. In Table II we present the predicate of the typeas the prefix common to all the messages in that type.

11

MSG ID
[R:0]
[R:2]
[R:4]
[R:6]
[R:8]
[R:10][S:12][S:14][S:16][S:19][S:21][R:24][R:29][S:22][R:34][R:37][S:68][S:73][S:112][S:137][S:15][R:9][R:11]NameSERVER_EXIT
CMD_TALKCMD_AUDIOCMD_SERVICESCMD_CAM
CMD_SYSTEMTOKEN_BITMAPINFOTOKEN_SERVERLISTTOKEN_WSLISTTOKEN_SHELL_STARTCMD_BYE
CMD_NEXTCMD_SERVICELISTSERVER_EXIT
CMD_REG_FIND
CMD_PSLISTTOKEN_AUDIO_DATATOKEN_TALKCMPLTTOKEN_PSLISTTOKEN_NEXTSCREEN
TOKEN_REGEDITCMD_WSLISTCMD_LIST_DRIVE

Prefix
0xcd
0x34
0x22
0x32
0x1a
0x23
0x73
0x81
0x7e
0x80
0xcc
0x1e
0x82
0xcd
0xc9
0x24
0x7a
0x85
0x7d
0x75
0xc8
0x25
0x01

MSG ID
[R:1]
[R:3]
[R:5]
[R:7]
[R:145][S:277][S:13][R:140][S:17][S:20][R:32][R:30][R:31][R:33][R:36][S:67][S:74][R:75][R:76][R:138][R:144][S:199]Name
CMD_BYE
CMD_REGEDITCMD_SHELLCMD_SCREEN_SPY
CMD_SCREEN_BLOCK_INPUTTOKEN_CLIPBOARD_TEXTTOKEN_AUDIO_STARTCMD_SCREEN_SET_CLIPBOARD
TOKEN_TALK_STARTTOKEN_CAM_BITMAPINFOCMD_SVCCFG/STARTCMD_SVCCFG/DEMAND_STARTCMD_SVCCFG/AUTO
CMD_SVCCFG/STOP
CMD_WINDOW_CLOSE
TOKEN_FIRSTSCREEN
TOKEN_CAM_DIB
CMD_CAM_ENABLECOMPRESSCMD_CAM_DISABLECOMPRESSCMD_SCREEN_GET_CLIPBOARD
CMD_SCREEN_CONTROLTOKEN_CAM_DIB/COMPRESS

Prefix
0xcc
0x33
0x28
0x10
0x15
0x76
0x79
0x19
0x84
0x77
0x83 0x01
0x83 0x04
0x83 0x03
0x83 0x02
0x00
0x74
0x78 0x00
0x1b
0x1c
0x18
0x14
0x78 0x01

TABLE II
L EARNT MESSAGE TYPES

0

[R:7]

3

[S:12]

4[S:13]

2

18[R:24][R:24]

19

21[S:14][R:30][R:4][R:6] [R:3]

5

6[R:29] [R:32] [R:31] [R:33]

15

16

8

[S:15][R:4][S:68]

12[R:9] [S:16] [R:37][R:34][S:67]

26[R:10] [R:8]

724[R:36][S:18]

[R:9]

10

25

[S:74][R:76]

27[R:24][R:75][S:199][R:138] [S:277]

28

Fig. 5. Full state machine learnt by our method

12

[R:0]

[R:11]

14[S:22]

[R:5]

[R:1]

9

[S:20][R:75] [R:76][R:144][R:145][R:140][S:137][R:2][S:17]

1120[S:19][R:24]

22

23[R:24][S:73]

17

13[S:21]

True and uncovers during the probing phase two message
type candidates that are added to Σ: ⟨R, ”End”⟩ with predicate (B0 B1 B2 = ”End”) and ⟨R, ”Data”⟩ with predicate(B0 B1 B2 B3 = ”Data”).
A series of additional queries is issued by the original
L* algorithm [2] to update the observation table such thatthe learner has a conjecture DFA to send in an equivalence
query. The first conjectured DFA is shown in Figure 6. For
simplicity, the rejecting state and its incoming transitions
are omitted. Equivalence query generates a test suite to

C. End-to-end example
To illustrate the problem and our proposed method weutilize an example of inferring the state machine of a simple
imaginary protocol.
The pseaudo-code in Listing 2 describes a client that implements this protocol. The client first retrieves the user id,
and sends an Hello message along with the specified id.
For simplicity, we assume that during symbolic execution,
the method GetIdFromUser() returns an unconstrained
symbolic value. Afterwards, the client expects to receive a
Welcome message with the specified id. Then, the client
repeatedly receives Data messages until an End message is
received, in which case the client terminates successfully. If theclient receives a message which is not expected, it terminateswith the value of -1.

q0⟨S, ”Hello”⟩

q1⟨R, ”Welcome”⟩

q2⟨R, ”Data”⟩

q3⟨R, ”End”⟩

q4⟨R, ”End”⟩

Fig. 6. The first conjectured DFA in the learning.

Listing 2. Pseudo-code of a client to infer

1:
2:
3:
4:
5:
6:
7:
8:
9:
10:
11:
12:
13:

⟨R, ”Data”⟩

start

test this DFA against and validate the DFA’s answer witha membership query (Section VI-C). For this conjecture, atest suite does not reveal any counterexamples or missing
message types, and therefore the learning process terminates with this DFA and the set of message types: Σ ={⟨S, ”Hello”⟩, ⟨R, ”Welcome”⟩, ⟨R, ”Data”⟩, ⟨R, ”End”⟩}

ID = G e t I d F r o m U s e r ( ) ;Send ( ” H e l l o ” + ID ) ;msg = R e c e i v e ( ) ;i f ( msg ! = ” Welcome ” + ID ) { E x i t ( − 1 ) ; }while ( True ) {msg = R e c e i v e ( ) ;i f ( msg == ’ End ’ ) { break ; }i f ( ! msg . B e g i n s W i t h ( ’ D a t a ’ ) ) {Exit ( −1);}
SaveData ( d a t a ) ;}Exit ( 0 ) ;D. Scalabillity extensions
The core of our method is scalable as its complexity isdetermined by the complexity of the L* algorithm which ispolynomial in the number of states and the maximum lengthof any counterexample provided by equivalence query [2].
Nonetheless, our method performs as good as the symbolic
execution engine it uses. This may inhibit the method frombeing applied to binary programs for which the symbolic
execution engine is not applicable.
One way to alleviate this limitation is replacing symbolic
execution with dynamic symbolic execution, which combines
symbolic execution and concrete execution. This way, modeled
program may skip symbolic execution of complex parts byexecuting them concretely instead, avoiding symbolic state
explosion on one hand but exploring all execution paths ofthe program on the other hand. Another way is to reduce theprogram using program slicing [16]. With program slicing,program instructions that do not affect the network interactionof the program can be omitted to create a simple, reduced
program, that is simpler for symbolic execution. We argue
that such technique can relieve the difficulty complex libraryfunctions pose.
Our method is also scalable in terms of its target protocols.
Even through our method was developed and was demonstrated to work with classical network application protocols,
its core ideas are abstract, and as such can be deployed on
protocols of lower levels and different mediums, such as USB
or Bluetooth, as long as they fit our minimal assumptions.
With that being said, if the user of our method chooses toterminate the algorithm before L* finishes, the state machinedeveloped up until the termination under-approximates thestate machine of the protocol. Message types discovered untilthat point describe valid messages of the protocol.

When our method is applied to this client, we hook theSend() and Receive() methods. The process begins withΣ = ∅, thus the first query to be issued by the learner is w0 =ϵ. This query is answered with True since an empty session
is valid for every protocol, as found by the monitoring phase(Section VI-E1). During the probing phase of w0 , we get examples of concrete messages that may follow w0 , e.g., Hello34, Hello 213 and Hello 9102 (Section VI-E2), andfind that the predicate for them is (B0 B1 B2 B3 B4 = ”Hello”)(Section VI-E2c). Therefore, the message type candidate is⟨S, ”Hello”⟩. Since no message types in Σ collide with thismessage type candidate, ⟨S, ”Hello”⟩ is simply added to Σ
(Section VI-B). Σ grew, therefore the observation table needs
to be updated (Section V-3), thus the query w1 = ⟨S, ”Hello”⟩
is sent by the learner. w1 is answered with True. The consequent probing phase reveals that a received message follows
w1 (line 3), therefore probing continues to the next message(Receive() at line 6) in order to collect constraints for the
first received message (from line 3). In this case constraints
are introduced based on the conditional branch in line 4.
Message examples that answer those constraints are thengenerated, and message type candidate ⟨R, ”Welcome”⟩ withpredicate (B0 B1 B2 B3 B4 B5 B6 = ”Welcome”) is uncovered.
⟨R, ”Welcome”⟩ is added to Σ.
According to the answer for w1 , the learner issues
queries w2 = ⟨S, ”Hello”⟩ · ⟨S, ”Hello”⟩ and w3 =⟨R, ”Welcome”⟩ which are answered with False, and w4 =⟨S, ”Hello”⟩ · ⟨R, ”Welcome”⟩ which is answered with13