PISE
PROTOCOL INFERENCE USINGSYMBOLIC EXECUTION AND AUTOMATA LEARNING
Ron Marcovich, Orna Grumberg, Gabi Nakibly
Technion – Israel Institute of Technology{ron.mar, orna, gnakibly}@cs.technion.ac.il

What is protocol reverse engineering?

What is protocol inference?
R: HELO

start

S:250 OK

R: MAIL FROM

R: RSET
RCPT TO: ??????

S: 250 OK

R:RCPT TO
R: RCPT TO

R: DATA
S: 250 OK
S: 550“R:” – Receive“S:” - Send

Mail Server

Motivations:Finding Bugs

Finding Backdoors

Analyzing Malware

Manual Protocol Inference is Hard!
• It can take days or even weeks!

Research Goal
• Automatically infer the protocol• Our input:• Binary code of a program• Our output:• State machine of the protocol• Messages formats

S: 250 OK

R: HELOstart

R: MAIL FROM

R: RSET
RCPT TO: ????

S: 250 OK

R: RCPT TO
R: RCPT TO

R: DATA
S: 250 OK
S: 550Assumptions
We assume:

We do not assume:

Protocol Regularity

Past traffic captures
Active protocol peer
Source code
Messages’ formats

Under the Hood

Overview

LearnerState Machine

L* Algorithm

Alphabet = Message TypesQueries
Answers

TeacherL* Algorithm for protocols• {R:init,S:start}• {R:init, R:init}
R:dataR:initS:startClientinit

start
data
finishR:finishServerAnswering Membership queries• Let’s assume for now that we know the message types

Is this sequence ofmessage types valid
for the protocol?

?

Learner
L* Algorithm

Yes/NoTeacher
Symbolic Execution

Symbolic Executiona > 3 ,b = 2789

Answering Membership queries• Is {R: Init, S: Start, R: Data} valid for the protocol?

R: Initmsg ß Receive()if (msg is Init)
false

ClientServerinit

Error()

R: Datatrue

S: StartSend(Start)
Msg ← Receive()
If (msg is Data)

start
data
finishfalse

Send(Error)
.
.
.

true.
.
.

Answering Membership queries• Is {R: Data} valid for the protocol?

R: Datamsg ß Receive()if (msg is Init)
false

ClientServerinit
start

Error()

trueSend(Start)
Msg ← Receive()
If (msg is Data)

false

true

data
finishSend(Error)
.
.
.

.
.
.

Discovering message types• As said, we do not know in advance the protocol’s message types.
• We update membership queries to discover it little by little.

Is this sequence ofmessage types valid
for the protocol?

Extend L* tohandle newmessage types

L*algorithm

Symbolic
Execution

Yes/NoIf yes, here are message
types that can follow thesequence.

Probing for following message types• What message types can follow {R: Init}?
msg ß Receive()if (msg is Init)

ClientServerinit

Error()

startdata
finishfalse

R: Inittrue

Send(Start)
Msg ← Receive()
If (msg is Data).
.
.

Getexamples

Probing for following message types• What message types can follow {R: Init, S: Start}?

R: Initmsg ß Receive()if (msg is Init)

Clientinit

Unknownsymbolic
Servervalue???
start

false

Error()

true

S: StartSend(Start)
Msg ← Receive()
If (msg is Data)

false

true

data
finishSend(Error)
.
.
.

.
.
.

Probing for following message types
Resume Execution:
Wait for message to beparsedConstraints aredeveloped
according to theparsing logic

Get concrete
messages thatmatch constraints

msg ß receive()if (msg begins with ‘data’) {// Constraint: msg begins with ‘Data’} else {// I can’t parse this message, error}

Concrete messages -> Message type
Example Messages

Find features ofmessage type

RCPT TO: email1@blabla.com
RCPT TO: user2@lalala.bbb
RCPT TO: person3@nana.ccc

RCPT TO: ?????

Tying it all together
Is this sequence ofmessage types valid
for the protocol?

L*algorithm

Symbolic
Execution

Yes/NoIf yes, here are message
types that can follow thesequence.

An illustrative example
R:initS:startS:startR: data R: finish

R:dataR:initMessage Types
M={}
M={R:init,S:start}
M={R:init,R:data,R:finish}
M={R:init,R:data}
M={R:init}
M={R:data}

L*algorithm

valid ?
YesNo JL

Symbolic
Execution

mnext= {R:init}{S:start,R:data,R:finish}{}

R:finishEquivalence Query• Approximated as in the original L* work, with a test suite• Probing is also in use for the test suite• To discover missing message types

Example - method’s output

Caveats• PISE is as good or as bad as the symbolic tool it uses.
• Currently, PISE uses angr.

- Trouble supporting multiple threads.
- Does not fully support windows API

L*algorithm

Symbolic
Execution

Summary
R: HELOstart

S: 250 OK

R: MAILFROM

R: RSET
S: 250 OK
R: RCPT TO
R: RCPT TO

R: DATA
S: 250 OK
S: 550QUESTIONS