Dear viewer, these subtitles were generated by a machine via the service Trint and therefore are (very) buggy. If you are capable, please help us to create good quality subtitles: https://c3subtitles.de/talk/57 Thanks!
Mathias is a student
at UC Berkeley
and Boston postdoc
Worries.
And he's really interested
in security, virtualization,
exploitation.
And he spoke with me about using,
um, um,
symbolic execution as a powerful way to
analyze programs.
Thank you very much.
Hey, thanks for the introduction.
Welcome.
No worries, no worries.
I was perfectly fine,
good to be here. Good to be back at the
CCC last
year. Unfortunately, I didn't make it,
although I made it here to
the tenth time now.
So 10 times in 11 years.
And I really missed it last year and I'm
so happy to be back.
It's awesome. Even though the location
is a bit different from Berlin, it's
really nice to be to be back
for this talk.
If the lights work at one point in time,
I hope the debacle in the room
one doesn't repeat itself.
Can you get. OK, awesome.
Awesome.
Let me take you on a journey down
to a rabbit hole, that
symbolic execution.
So and let's follow Alice
down that down hole and
see how far we can go.
Symbolic execution has had a bad
reputation for quite a while now.
Many say it's it's overhyped,
it's oversold and
people are promising too much.
And in this talk, I want to discuss
with you what it can do and also
what it can do.
So what are the limitations of
symbolic executions?
How far can we go?
What kind of things can we explore and so
on?
What are the limitations and how can we
get around them?
This is joint work with Stephen McCammon,
who started all the amazing
Fuzzball stuff and who is the main
contributor of the symbolic execution
engine and maintainer
of the engine as well then.
And Alex, who did amazing reverse
engineering work while they were at UC
Berkeley and a whole bunch of
other students, interns and so on, that
really helped us get along and get us
that far.
So almost
all of the praise goes to them.
I'm just delivering the message
to you.
So let's start the some of the
of the preconditions when been following
down at whole.
So there are actually a large
set of tools
to help you find books and
discover books and so on.
And we all know that finding books
and creches, that's the easy part.
Right. So getting something to crash,
getting a six-fold, that's easy.
There's fuzzing, there's bound up
model checking and
test cases and a whole bunch of other
things that can help you to to get
to these books or to to actually
trigger the books.
But the hard part then comes
how can we generate an exploit
or how can we find a specific
form of input's that travels along
the path, inside the application
that will then trigger this vulnerability
conditions deep, maybe deep inside the
program?
How can we actually define all
these little things that flow through
the application that end up
and come together at the vulnerability
point where the bug is to actually
trigger the vulnerability?
Also, how can we cope with all
the transformations that the input
undergoes until it reaches the final
point?
And we'll look into how we can
use symbolic execution to
kind of trigger this point and
follow down the chain deeper and deeper
into the rabbit hole.
So on a very high level, what we do,
we assume that we have found some
vulnerability condition in inside
the application, maybe deep inside the
application, hidden behind some
form of transformation's and so on.
And what we do is starting from that
transformation. We walk back step
by step by step by
step until we
hit the input of the program.
Some input that we can control, actually,
and we will then generate a proof of
concept input that follows down the
chain of transformations until it hits
the vulnerability and for all that
we use.
So until now, abstract
form of symbolic execution, our
magic box that reverts
and inverses all these transformations
to give us the inputs that we
want to look at and
we'll discuss what kind of tools
for mystic's and optimizations we can do
to make it actually feasible and scaled
up to two larger systems so that we
can actually work with real programs and
not just little 20 line toyi programs
that some of the
papers are talking about.
So and
after Demotivation as a next step, I
will quickly introduce symbolic execution
as a technique, how it works,
what kind of tool exists, and
maybe a little bit at the
at the limitations of these tools.
So what actually
is symbolic execution?
So on one hand,
it's an abstract interpretation
of code
instead of using concrete values
when we execute individual and.
We use symbolic values and carry
these symbolic values along the execution
of the program, so we kind of virtualize
it and instead of concrete values, we use
symbolic formulas that get longer
and longer the more instructions that we
execute and with all the additional site
conditions and so on that we carry along.
Also, it's agnostic
to concrete values as every value that
we have, every concrete value turns into
formula.
And then if we have additional
constraints like an end to some values,
some static value or some
some Solectron or anything like that,
then the concretization helps to reduce
the complexity of the formulas that we
have to carry all along.
And the goal is
if we finish the transformation
and can produce a specific
condition that holds to all the
the past. Along the way, we can find
the set of concrete inputs that
will actually fulfill the condition that
we have in the end.
And we can then use this one
to trigger some interesting condition.
So let's drink the Kool-Aid
and look what we can do with it.
So for our vulnerability,
for our example, we define a
set of abstract
conditions at specific locations.
And symbolic execution is then used
to trigger an input
to generate an input that we can use
to actually trigger that's that
vulnerability at this other location.
And there are two kind of ways that
symbolic execution is used for.
And one of them is testing.
So for finding bugs in applications.
And the conditions that we encode are
a set of preconditions and post
conditions that we want
you to hold at specific locations.
So maybe a specific condition
would be that the return instruction
pointer on the stack is never overwritten
with some other values, or
we use the assertions that are already in
the code and we use
symbolic execution to ensure that
there's no inputs that can trigger these
assertions under this specific set
of conditions.
Or an other option is
to use symbolic execution
for exploit generation.
So we have a set of conditions.
If these conditions would hold, then
we would be able to exploit the
program in one way or another.
And we then use symbolic execution to
generate the inputs that triggers
this safety violation on the
on the higher level.
So.
Our goal is to kind
of revert or let the machine do
most of the work, but we only define
a set of conditions we are interested in
and then let the machine do all
the work and let us just look at the
final result.
What kind of tools are out there?
What what what kind of how does the
gang look like that? We have.
So there are three major symbolic
execution tools that all cater to
different needs.
One of them is Fuzzball, the one that
we developed at UC Berkeley, and
we are selling it as a tool for
proof of concept exploit generation.
A proof of concept exploit is not
something that is
exploited. You can shoot out and execute
your code right away, but it just
triggers a condition.
Maybe it overwrites the IP and
redirect it redirected to somewhere else
and you can then use it, use this one to
bootstrap it further on.
All these tools are open source, of
course, and you can download them and
play around and do your own stuff.
S3 and other awesome tool developed
at CPFL in Switzerland,
which offers you selective symbolic
execution on a large, large scale
system. And you can trigger these
symbolic values along the execution of
of larger applications and systems
and Clie and other
symbolic execution tool that's been sold
to or developed to find
bugs in and applications
and in source code and so on.
All of those, as I said, are open source
and many of them have
helpful information on how you can
bootstrap and and get along.
So now that you know that the concept
of symbolic execution a little bit,
I want to give you a concrete example so
that you can actually see what the what
the power is and
what better example than one of the
vortex war games.
These are
hacker games where you have to try
to exploit specific conditions and
programs and they are really good
to develop your skills and get
used to to coding and vulnerabilities
and so on. And I thought, well,
I don't like to think that much.
So let's see if we
can use symbolic execution to actually
help us solve one of these
deals for games.
And this one is one of the early ones.
I guess it's number one or number two or
something like that out of thirtyish.
And it's a program
that reads and input's transfers.
It does some stuff and
then triggers a shell and
drops you into a shell.
And if you look at a code a little bit,
we see that somehow we have to
overwrite the pointer with,
okay, and then we'll trigger
our win.
So how can we trigger that?
It's down at the default case
in the big switch where the input is loop
through and execute it and
oh let's see.
Oh, we actually have a
right winnability, but we can actually
write some
values into memory
that are protected by a guard
if he said if he cannot write after
the end of the buffer.
But luckily we can write before the
buffer and we see
that pointer is initialized as a static.
All these you know, we know the address
relative to the to that other buffer
we can using a special character,
we can decrements the pointer and
move it back and forth along
the
along to execute a code or a long memory.
And in the end, it looks like this
pointer points to Buffer and our switch
case. We have three different versions of
ternary
selection between a debug output
that commanding the pointer and
either triggering our win
or writing
a value to memory.
This sounds still very abstract and
the problem size is three to the power
of NP that we have to walk through
and we'll just look at the at a quick
demo and I hope that I can switch over.
Yeah, looks good.
So we do have
our code here instead of
dropping us into a shell.
I changed changed it into a clean
exit with an exit number.
Twenty three just makes it a little bit
easier. And I help
symbolic execution a bit
by allocating
the buffer at a specific
offset instead
of at a random address.
And in the end, we'll
just walk through the
through the buffer and let symbolic
execution handle it.
I remove the debug output.
So if Subotic execution engine would
trigger the debug, I don't want to
clutter to the
screen all the time.
So let's compile it,
compiled it and let's
see what kind of stuff it generated
a large set of conditions.
We started in our symbolic execution
engine. We assume Linux system
called model.
We virtualize the different components.
We set
six symbolic input bytes
at our input buffer that we want
our symbolic execution engine to
generate.
And we give it a start address
where we start the symbolic execution and
address where we end symbolic execution
and let's just run it so the system
initializes.
We have a set of system calls
and now it's trying different inputs.
It tries to follow all the different
states that are possible and tries to
generate the inputs that will trigger our
win at one point in time.
And you see that all these ones
that you see scrolling by are generic
inputs and it works through
the backslash that triggers the decrement
right values and
specific
print debug prints.
It removes the debug prints pretty soon.
And now we see that it's already finished
in roughly twenty two seconds on this
poor little netbook that I have here.
And it's running on the netbook, not on
the on the cluster.
And we see that it generated a set of
back slashes to decrement the pointer
it writes and see
which is two hundred and two in decimal
and then you can write any value to
actually trigger the win condition.
And we just use symbolic execution
to solve a vortex war game in
three minutes, which is kind of nice.
When I solved it the first time, it took
me like three hours or so.
So that makes it a bit easier.
But let's continue
so we now know what symbolic execution
is capable of.
But how far can
we stretch symbolic execution?
What are the limitations that will run
into it?
Looks kind of a nice tool, right?
So if we could just use it to write our
up exploits or upside for us, that would
be perfect. Right.
But unfortunately, that's not going to
work. So we're going to look at the
different limitations regarding the input
size, the amount of symbolic bytes
that we have and the amount of code
that we can cover symbolically because we
always have to execute it symbolically
using some execution
engine. It has a high amount of overhead.
So how far or
does symbolic execution, symbolic
execution scale and if so, how far
does it scale?
We start using a simple
example and we use a run length
encoding, which is one of the simplest
compression formats that you could think
of. It was invented in the 70s
for
two to encode fax images
and stuff like that, but it's still a
valid encoding in all the PDF formats
in any PDF reader has to
has to actually implement it.
In this in this back,
we assume that
the output is given and we have a decoder
function, but we want to
have a specific input that then decodes
to our given output if
we only have the function that decodes.
So we use symbolic execution to compute
the pre image to a given
given output.
And we evaluate the performance of
Cleon Fuzzball, two of the the bigger
symbolic execution's engines that we
could just run on top of it.
And we implemented our lead the same way
as it is implemented in PDF.
So let's look at how far
symbolic execution actually scales
on the X axis.
We see different configurations
for this, for the simple benchmark with
input and output length.
So three input bytes, three
output bytes, up to five input
bytes and three output bytes.
And on the Y axis, you see the runtime in
seconds. And remember, it's a logarithmic
runtime and we set a ten
hour.
Ten hour limit, so
as soon as we scale
up the input sizes,
we see that the output
of the time we need
to run, the experiment goes up.
And if we are using only
seven input lights that produce
nine output bytes,
we already run a couple
of hours.
So vanilla symbolic
execution does not scale, if you use it
that way, will run into the state
explosion and you cannot invert these
processes. So we have to get around that.
Somehow
we just run into the state
explosion that we follow
at each decision point in a controlled
flow graph. We follow
all the policies that follow this
this decision point.
So if you have a simple control flow
graph here and we start executing
from the top,
first of all, the symbolic execution
engine follows one single condition
and updates all the passes and
constraints along the way.
Then we follow we have to follow both
the second and the sixth
point. So we already have to
pass.
We continue test
on the on the right hand side.
We have more and more passes that are
trying to get her to continue.
We continue and we see that
the longer we executed symbolically, we
have to carry on all these constraints
and the formulas get longer and longer
and longer.
And that's how we how we run into the
state explosion.
And the problem is that we cannot
decide which ones are more interesting
to follow and which one or not.
So we're basically drowning
into the sea of tears,
just like Ellis did.
And we want to know what the reasons are
and how we can get around those.
So one of the reasons
for the state explosion is
there's too much input or output the
output data that we're interested in and
there's not much we can do about that.
That's that's what we wanted to scale in
the first place.
The other one the other reason is
that there's too much included state.
So we have to limit the
amount of symbolic state that we carry or
carry around.
And there's too much execute a code
in one go. So it gets too complex
for the symbolic execution engine.
And we have to use a divide and conquer
strategy strategy to split
it up into into multiple steps.
And we're going to see how we're going to
do that later on.
So let's scale it up
instead of just seven symbolic input
bytes. We want to have more.
We want to solve the problem in the first
step using some set of patristic.
So if we can encode somehow
specific conditions that
help us in the symbolic execution
process, how far can we go then?
How far can we can we scale it
up if Chote behaves according
to a set of properties that we define
in the next step?
So what are interesting input size is for
us, how far can be scale it up
in this limited space of computation that
we have available
10 symbolic input bytes?
Well, this is kind of an address,
an offset or a pointer or two,
but not much more.
We can already do that with the existing
symbolic execution engines.
Other options.
If you have 20 to 80 symbolic
bytes, we can actually invert
some shell code, a smaller chain
or something like that, but
unfortunately not much more.
And that's already the limit.
If you have a lot of computation
available that you can do with with
current engines.
And if you want to have more than two
hundred symbolic input bytes, we can
encode longer options at our
vulnerability condition or
even complete data structures that are
present at our vulnerability condition
and flow through to through the
application until we hit that stack
condition.
So first of all Ristic to
the rescue, let's use,
let's assume some properties on the code
or let's assume that the code follows
some well-defined properties for
specific transformations.
And we looked at a whole bunch of
of code blocks that transfer
input data in one way or another
and most of the transformations
are subjective.
So there exists
an transformation.
So for a compress function,
there exists a decompressed function
for encode function is the decode
function for image
decoding, there's an image encoding and
so on.
So we assume that
this holds we also assume sequential
sequentially. So as soon as that our
code transformation writes a specific
input byte, we assume that this output
byte will never be revoked.
And we also assume that transformations
are streaming. So the amount of
symbolic state inside the execution
engine is bound and does not rely
on the complete input data that's
available. And if these transformations
hold, then we can
we can do some
tricks and we can use some specific
Ristic to cut some corners.
And some of the risks that we use is
to prune early and prune often as soon
as the target becomes unreachable and
just drop this data that will never reach
our our goal.
Another one is to be greedy.
So if we see that one specific
state or one specific path that we follow
and the symbolic execution engine
produces a lot of symbolic output bytes
or a lot of output bytes that we desire,
we'll actually prioritize this.
In our search and try to follow that one
deeper into the into the rabbit
hole to get as much output data as we
can, and we do some specific
optimizations for error excesses
by combining formulas or
splitting formulas depending on the set
of conditions.
But you can read about that in the paper
if you're interested.
So if encode this restricts,
how far does it scale?
So we use the same transformation as
before.
This time we use three configurations
CLI, Fuzzball and Fuzzball
with our newly encoded heuristics
and we see, well,
it's not too bad.
We are doing much better then
than an optimized version.
So we still see some
kind of explosion, but
it's not as bad as before.
So heretics help.
Well, a little,
but the state explosion still remains
and we have to cope with that much
further.
So
let's see if we can use divide
and conquer approach to break it
up into smaller steps.
Juristic got us so far or that far.
Now let's take a data structure or data
centric approach and splits the process
of computation of computing into
pretty much into several smaller step.
And we tackle each step on its own.
So we have the same program,
abstract program, some vulnerability
condition as we had in our motivation.
And we know that the input flows through
that application to reach to
the vulnerability point in the end.
But this time
we know that just using
one symbolic execution process is not
going to work and it's going
to run into the state explosion and we're
not going to be able to produce anything
that's interesting.
So we actually have to take a different
approach.
And by following a data centric approach,
we know that input is processed
in each program in several steps.
So first, the input is copied into one
input buffer.
Then there's some transformation onto the
data before it is copied into the next
buffer.
After that, there's another
transformation and it's copied into the
next buffer.
And at one point in time they'll reach
the vulnerability condition.
So now, instead of using one big chunk
of symbolic execution to compute the
premise in one go, we use
several chunks of symbolic execution
and concrete this size to values that
each at each decision point that we
figure out.
So we use several steps of symbolic
execution to compute the
image in the end and trigger
and solve to solve this problem.
So again, that's
symbolic execution scale.
If you use this this approach
and this time we use two transformations
which are both valid for PDF files.
First, we use a hex
decoding, so we have a long hex
encoded string that is first text
decoded by the PDF library
and then our lead code to
display an image.
Imagine we have a ticket
digitalized text message somewhere
embedded in a PDF and both
hex encoding and decoding are
valid PDF transformations, according to
the PDF specs.
And we start
with the second location, so it's the
second transformation refers to the early
decoding and then the hex decoding
and the look at the different
configurations of these these three
applications again.
So let's look at the code itself
in a simple, simplified way.
We see that input is copied into
the first buffer buffer zero
and then the ASCII
code, the
decoding right into the buffer one
and then the buffer one is decoded using
RNA, decoding into buffer to where
we might trigger a vulnerability at one
point in time.
And we constrain symbolic execution to
one transformation at a time.
And the symbolic input bytes
only have to flow through one
through one transformation.
So we have to buffer zero, which goes
through hex code with buffer one, we
goes through our old code and
then we end up with our
win condition and we use two steps of
symbolic execution.
So let's try a quick
other TMO,
I guess I have a couple more minutes,
hopefully,
which should be enough for that.
Oh, that's wrong one.
Here we go.
So we have our
decoding and.
Let's just copy that part,
not all of it.
No.
I'm doing that on purpose, you know.
Yes, here we go.
And we're going to first decode the
Aurélie buffer and we want to produce
a string, Serguei
3C is awesome and
we let the symbolic execution find
out. So the symbolic execution engine
knows about the Aurélie decoding
and it's trying different, different kind
of states.
And this, Aurélie, you see, if there's
no repeat characters,
then the first bite
encodes the length of the string,
then the string follows and
then there's the specific end fight.
And in this type, the configuration
that fuzes, it's one twenty eight, which
is Oxlade and
our symbolic execution engine
successfully reverse engineered
the RLC encoding
process using the Aurélie decoding.
And we can do the same thing for the for
the hex decoding.
But I'm not going to try to copy the
other part again, otherwise I'm going to
run out of time.
So I'll actually upload
all these examples so that you can you
can try them out later on.
So let's see how far we can we can
actually go with
this this encoding.
And this time we have hex
encoding and decoding.
So two steps and we compare it again
against
Fuzzball without the configuration
as a monolithic approach and KELY
as well.
So it gets a bit more complicated
this time. So we have input bytes,
intermediate bytes and output bytes.
So there's a first transformation from
output bytes to intermediate bytes
and then a second transformation from
intermediate bytes to input bytes.
And you have a set of different
conditions that we try out on the Y
axis. Again, we have to logarithmic
scale and
again, a 10 hour time limit on
on our cluster for single core
computation.
So what we see
is, Mel, monolithic, symbolic
execution engine as used by clear
fastball, runs into the 10
hour time limit every single time
for this for these configurations.
If we use our jurisdiction
now, we're doing a little bit better.
We scale up to 20 ish
bytes, input bytes that we can cope
if we use our
our two step approach where we split
according to the different
transformations, we can scale up to
two hundred and fifty hex bytes that
we that we encode and
one hundred and twenty intermediate
bytes, which is good enough for
reasonably sized data structure that we
can carry along.
And we see that this works fairly well.
So we have one problem solved.
Divide and conquer mitigates the scaling
issues, but we now have
two problems
finding the transformation boundaries.
How do we do that and finding
the buffer locations?
How do we get that?
How do we know where they are, especially
if we only have binary code or some
some executable?
So let's see how what we can do
and let's use some binary analysis
technique for that.
So there should be splits, the symbolic
execution units, and we use a
graph based binary analysis approach
to find minimal points along
the execution graph of the application
where we have little interference
between individual transformations
that's transformed.
The data is available.
So on one hand, we have a
control flow graph, but
we combine this control flow graph with
information or data flow graph, on the
other hand, and information
flow graph encodes
how information flows from one
buffer to another buffer.
And these two data structures already
exist. But we add
additional producer and consumer access
along these these two graphs so that we
can use the combined graph to
decide what the best points are
to split individual transformations.
So we know that buffer to
buffer AVL
basic block number two will read
from buffer from buffer and
symbolic of basic
block number for Will right to buffer
seat. So we know that there's an
information flow from Buffer A, buffer B,
and we can use
these informations to know
or infer that there's a transformation
from Buffer a two buffer C, and we can
follow that one.
So
how can we recover this graph?
And we just use a simple trace
based binary analysis.
On top of that, we collect a detailed
instruction level trace of
a concrete execution that executes
functionality that is close
to the vulnerability but does
not trigger the vulnerability itself.
Otherwise, we would already have solved
the problem. Right.
So we execute
a simple version of like just a
PDF viewer and encode the execution
trace and use that execution trace
to see how the input data flows
through the application.
And using that execution trace, we can
follow all the individual buffer
exercice and concretized dose.
So we start with a concrete input.
We collect the instruction level trace,
we process the trace off-line to
discover all these the individual buffers
and set the combinations between the
buffers.
So problem
is, if we are working this
machine code, we have a huge
a huge amount
of memory accesses and
we need to organize them somehow.
And we do this using a hierarchical
concept where we have different
levels and categories of buffers.
So related memory
accesses target the same buffer.
There was maybe a temporal or a spatial
location temporal,
according to the access log of memory
access that we have or spatial according
to the codes that we have.
And in our analysis, we can actually use
both these kind of accesses to group
related memory accesses and
we assume this buffer hierarchy as the
level of buffers.
So there's a complete memory image.
There's the stack, there's an individual
stack frame, there's this struct in a
stack and there's a specific buffer in
that struct on the stack.
And we find natural boundaries
between transformation's to split up our
symbolic execution.
As a last example of
we're going to walk through the CVI,
a real vulnerability, where we have
a fun parsing book in a popular
PDF viewer. That's a fairly common PDF
library.
And if you look at the memory
axis, it's insanely complex.
It will be very hard from a vulnerability
point of view if you only have to binary
to actually follow these individual steps
until you hit the condition.
So there's IO processing, there's
deflated code that's happening,
the fun reading part
and to parse font parsing parts
and debug actually happens in a fun
parsing. But how do you generate such
an input? How can you actually produce
that?
And we ran our
magic python script on the trace
we collected and splits the symbolic
execution along these these paths
and came up with a set of several
symbolic execution processing
steps to produce that that image.
First, it's the meme copy that copies
from for a buffer, B from the input
buffer to the parsing buffer.
Then we are able to decode
the flat
encoding.
We read the front into a buffer
and in the end in the front parsing
part, their woman ability,
and we're actually automatically
able to produce input that triggers that
vulnerability, that
follows along these different steps
according to the split's that we have in
our in
our graph.
So selecting the individual parts
from the graph that we have is
still still need some manual
work, but it works fairly well
and you can actually try it out for
yourself.
So what did
I show you?
First of all, symbolic execution
is no pennachio for every problem that
you can just throw stuff at it and let it
solve it. You have to be aware of
all the structural differences.
And due to all these additional overhead,
it doesn't scale that far.
But if you look into the individual
transformation, the kind of code you're
trying to reverse and you're aware
of some graph based analysis on top of
it, then you can actually scale it up
to real data structures and do real
things.
You can trigger, as
shown in this example, you can trigger
vulnerability conditions that you find
that are deep inside the program and
hidden. And you can actually construct
some proof of concept input that will
trigger this ability in the end.
And you can explore how deep the rabbit
hole goes for yourself.
You can download all the software from
the website.
I'm around on a C.C.C..
Just talk to me.
I'm happy to discuss anything in more
detail.
Thank you for your attention and I'm
happy to take questions.
Thanks.
We have around 10 minutes for a question
and answer if there is any
gap.
Microphone one
high.
Excellent talk.
So my question is
in relation to
the ease at
which one can recover these opaque
predicates that you
seemingly recover automatically.
So another developer related project,
Bapi, came
by Noisebridge San Francisco hackerspace,
and he showed
a demonstration of VIP, which is very
similar to bikeways
recovering the Aurora vulnerability,
which is I think, like get Phonte Icon.
And it seemed that a considerable
amount of the work that he did
in Bapi
and Microsoft Internet
Explorer was actually like writing
some Tlaib code, which,
you know, like you can feed into Z3.
And it seemed that a considerable amount
of the work that was performed actually
had to do with
a lot of knowledge that he had
about the vulnerability.
Well, well, after the vulnerability of
being published.
So it seems that the majority of the work
was done by like Z3 or
some other equivalent SMPTE solver.
And then Bapi kind of had this ancillary
role that,
you know, didn't
seem to be recovering these these
neat things like, you know, tracing a
return code as it gets
passed through the program.
So I guess what is your opinion?
If I were to ask a concrete question,
what is your opinion on the limits of,
like execution or Bitlis
on truly generating
exploits automatically without a great
deal of knowledge about the nature
of a vulnerability or the program that
runs? First of all, I'll be very happy
to talk with you about this offline for
hours. But let me give a very short
and brief answer.
So in this talk,
I gave the motivation that we already
know the vulnerability.
So we know at which instruction
that vulnerability is cost.
And we know to the code we
can look at the instructions prior
to that access and we can actually encode
these instructions so we know what kind
of conditions happen at this
this vulnerability. We just want to
produce
reimage that flow through the application
that executes that that
one ability.
And you are perfectly right.
Symbolic execution has a hard time
encoding these properties
and it needs a huge amount of manual
effort and work if you use
it to find the vulnerabilities.
So I'm not 100 percent sure if
symbolic execution is a perfect
tool to find the vulnerabilities.
You can use it to generate images.
That's what it's here for.
But you will have you will need
additional logic and manpower
to encode it for
to find the vulnerability conditions
itself. Just a quick follow up.
I'm sorry.
Let me give a quick, blatant
commercial interruption.
So there's bound a model checking
and you can use Bonnett model checking to
infer a nice set of
vulnerability conditions.
And we're using we are moving more and
more to t to use bounden model checking
to actually come up with the actually
vulnerability conditions that it can then
feed into the symbolic execution engine.
On the other hand,
you have
other questions.
Yes, here, please go to
microphone to
just I was just trying to
refer to the guy who is talking about
and that is very interesting
and he's very, very
intelligent programing in a sense.
But to be honest, I'm not really sure
it's the best topic to talk about in a
conference like this, because it's called
source development Microsoft.
And they really are ranting about
said, sorry, sorry,
what are you ranting about that.
Yeah. Yeah.
So, I mean, this report said three
and stop so you can use to any sulpher
you want. Yeah. I suggest you use S2P.
Yeah.
The drawback is STP is half as fast.
Right. So yeah.
Uh, could you handle, uh,
it's, uh, arbitrary
state explosion added by,
uh, obfuscated code or something
like that?
Do you have some way to detect that some
court has no influence in the result
of.
You're talking about the obfuscation
of so let me let
me rephrase your question, if I if I got
it correctly. So you assume that you have
some obfuscated executable
and you want the symbolic execution
engine to get rid of all the superfluous
computation not
to get to it, because sometimes
you just don't,
uh. But is there some
way to
crash this space to,
uh, to
eliminate some part of
it, cost us all the
heavy or a lot of the heavy lifting is
actually done by the constraints.
All right.
So if
under specific conditions,
no computation happens to
the constraints, should simplify
the formulas and throw away those
so that happens intrinsically
in the in the hole for itself.
So we don't have any additional checks
that help in that regard.
And we focused mostly on
binary only code, but not heavily
obfuscated or packed code.
You can try out and tell me about
it afterwards.
And just a quick question.
How much memory does it take
to keep track of all the
parts you went through
for popular?
I guess we used something like
12 or 16 gigabytes,
so not too big.
Well, rent is cheap, right?
Oh, OK, I think we're on
the rise. So if you have other
questions, just catch me somewhere on the
CCC.
Thanks. Thank you.