[Applause]
myself and videos so I use this
decompiler saying that when it goes to
the website in the contract name and put
together this for almost every contract
the source code that is kind of human
readable which i think is a new thing
because they weren't that many compilers
that could allow you to create sources
like to view the source of most of the
contracts and I really build this whole
thing out of frustration with either
scan because it's only like doesn't
allow you to access all source codes
easily and a lot of source codes are not
open there so I said I will just
beautiful compiler that anyone see any
source and it will be open so anyone can
start their own thing and work with it a
little bit so so that was one of the
main innovation behind us so you go to
the website and most of the constructs
you see the compiler right and the
second school thing which is I think
even cooler is that for every contract
there is this intermediate form so this
is the same thing as this but but it is
alright you can write the others all
right so so anyway there is this
intermediate form which is quite cool
because it's I know that it's looks like
gibberish but this it's really a Chinese
100 percent
every single contract out there and it's
quite nice because the way it's
constructed is it's constructed in such
a way that is very easy to analyze by
machines so we can write very simple
merciful analyzers or source codes and
you can get like you coming you can do a
lot of cool stuff that I will talk about
it in the end do it
so anyway again the decompile forum and
this right and there are of course other
tools that are yeah that are in the same
thing so there is mention for example
that that is doing symbolic execution of
every contract and and tries to figure
out what are the potential backs there
right there is magic or that does a
similar thing from from 12 bits and
there are some other decompilers but
they have to solidity and I don't like
curly brackets even though here also
what I am that's anyway mmm in this in
this quick talk at workshop talk a
little bit about what symbolic execution
is because that's the basis of the whole
compiler and that's a basis for a lot of
security tools and contract analysis
tools
so I will explain how exactly it works
and then I will explain a few different
things related to simple execution and
how various tools solve them
so it gives you a better understanding
on well essentially how these things
work and perhaps
your own thing or or the seal those
things better then I will talk about
some crazy stuff that I have to do to
make make the results so pretty and yet
I will show you a little bit more about
the broader context of the whole like
the compiler slash contract analysis
space I think it will take care of I
don't know an hour probably and then we
have some more like a lot of time for
questions and answers and more products
that one atmosphere and all right so
symbolic execution how many of you know
what simple execution is alright alright
so
so they're here with somebody education
is that we never like we're securing
your honor it's always the beginnings of
the presentations people coming in now
so you have the assembly right and and
you have the Santa code and the
beautiful machine of gear you works by
executing that code and now it sees I
know
put something on static and then it
pushes that thing on the stack right
Linc's Pulsifer static and post on from
stuck and just executed comment by
comment right and that's how the whole
information works symbolic execution is
essentially the same thing but you don't
deal with complete values so you start
the program and you know if the program
says push number one on stack we also
have the static and English number one
stack right but if the program says food
call data or some something that you
don't know because you're you're not
writing an actual transaction you push
this this is variable or this symbol on
the stack right so here for example this
function has access and assembly come on
same core value right so it wants to
push cold value on the stack regular
virtual machine will just push that
concrete value that was you know value
on the call on the stack and my face
which was just you know we try to the
stack there is some value I don't know
it is just I push it right
what happens then is you know there are
other things that operate on the stack
so so easy o command for example you
know grab something from the stack make
it sit and then puts it back on stack
right to put swanee there is if it's
zero and it's zero there's it's anything
else
so we checking our virtual machine it's
easy because you just have regular
arithmetic with symbolic virtual machine
you have to
you know abstract especial expression
and you would be put on the status value
saying oh is zero compiled exam right is
this kind of clear because I don't want
to know some of the people that I want
to be I want to be dressed so so yeah
another example here and you know
pushing this value on the stack so now
we have stacked with two values 0 and 60
91 and then the fun part is when you
have jumps because regular virtual
machine might see something like this
damn right it just checks what's the
value of the stack if it's it's higher
than zero that it makes the job it's
zero that it doesn't make the job and
it's quite straightforward it just
continues execution but when you are
running as a bullet execution even if
there's actually more to help you toward
machine and now running in parallel
right because you don't know the jump is
performed or not because the knows the
finalists a because it's easier kabadi
right so it can be anything so you have
to kind of fork the stage and then
execute everything below authenticity
right so so you're just you know call
here and
Frankie from this month on right so so
you kind of executed the execution and
yeah if you just execute one line by
buying enhance and at the end which is
oblique at the calculation whatever they
do to erase whatever it is something
interesting to the user that changes the
state of the contractor involved require
receive this redefine phone right so if
someone the contract rights to a storage
somewhere to the storage and all your
eyes it's just removed right and well
the decompile code is really like this
trace of execution of the symbolic
machine and and that's wrapped it so I
know there is some kind of storage right
right and I just write you know right
it's the storage and that's the part of
the program that actually gets up to the
user so at the end of the second
function let's ignore it is we had fight
a series of ease and we went deeper here
so so we not perceive the receivers
so this is the new copilot form so
essentially I just executed the whole
program symbolically and I quit about
all the storage drives all the eaves of
rebirths everything and this is this is
it right and to ease to build I started
that by the way I absolutely no idea
what I'm doing so I just grabbed the
crypto keys my contract that I said I
will don't know of going out there I
didn't know that it's called spotting
execution actually so the problem with
this is this is doubtful that you will
actually see on some of the compilers I
think recently other decompiler this
society like it is way way simpler right
it's just yeah
the function is really much much simpler
just the executions of so many paths
that depend of speed here so there are
other algorithms unity it's mighty
compiler that emerged is right later so
the whole function was like this so we
went from assembly code everything
identified by I so this huge tree of
execution right and then we called it is
something much simpler that's the
function yeah
[Music]
okay it's it's difficult with the slides
I yeah you have to come cause they're
sorry because I cannot like on three do
decide right now
you killed stole like you have to see it
yeah there are some I didn't know yeah
so the other thing that that is done is
for any contract that you figure out all
the fashions that I can figure out what
are the other factions for some storages
and based on that I can say oh this
functional internally storage
dysfunctional name is Diego address so
so this storage is my CFO address and
then I end up with very nice code that
just doesn't care right that's readable
so that's it
yeah that's mm-hmm
that's like the outline of the compiler
does and how simple execution works and
then any questions here I will concede
what proportion of the
routines you have to collapse into
smaller oh that's like I noticed solve
an immersive South Korea in England war
on the polarity looted class like I
would say most of them had some kind of
things to the to meet collapsing it's
just like super nice super nice
experience to work on this folding
algorithms because some of the functions
usually were less of screens and screens
and screens in land and then you write
it with algorithm and they fall to this
so I yeah so it's not Q by okay I'm
street I was gonna ask how you handle
area stuff that Pfeiffer doesn't
normally do yeah so so in general like
that's a question of commonalities and
you think I'm part of something that can
be recompiled and feely like it's very
hard to do something that it's not just
some kind of a pseudo code because
exactly the stuff that like either a
viper or sewing it easy think of like
it's hard to really compare to something
so it's just yeah yeah how do you do the
mapping for the function names and the
function identifier I mean they're there
libraries but you don't know all your
function names I will talk about the
baldhead all good quality morally the
same as optimizing no I mean that is it
like correct translation oh yes it is
yeah what I mean where I'm having with
this question is you weren't partly on
the youth talk by saying so they have
this intermediate language high cap and
it doesn't seem you know to hide ever
but what they do is that they have this
optimizer which is like collapsing
greedy and also stabbed right and maybe
viper or say disease not the targets for
you know this mighty you is yeah I think
it's always best to try and work with
existing tools right I mean that's an
exerciser I mean I use people switch to
my intermediate forums
it's like they got 15 play yeah okay so
those two questions will be answered
later on anyway
so there are others willing execution
energies and then sort of them and we
can both get solicited for Gant about
about other teams working but like two
significant ones the team I doubt it
though
oh no thanks material from consistently
a chance right so they use a very
similar process so whenever you have to
work with material like you know they'll
be that's what they do that's what
actually does and so we execute the
whole cold and right like one of the
things that we did our strategies say
execute the whole called symbolically
and then month or from trade trade of
beads they in do analysis verification
of the software right and they use very
very similar problems to the mother I
just described so they execute the whole
program and and they just volley so if
you understand this about execution part
you really are like you you really
understand how like the most significant
tools on the market right now
right it's worth spending some time to
work with that know somebody game is
between is like this is the double
dating right and there are few super
super difficult things most of the tools
don't so properly sometimes either one
of them to sauce and I would say of I
don't know eight months
that's like eighteen time working on
this whole thing I spent probably half
of the time doing memory handling
process
explosion that was this folding thing I
do that in an afternoon but it's like I
don't understand how it works something
good answer so a little bit about
Memorial and me now and then another
processing and then move to they're like
tiny things that we have that you asked
about so when we are handling I told you
how somebody execution engine execute
the program right and it's easy when
it's just I put somebody on the sky to
get some value from the stack there's
some APIs plead to stay don't but what
happens if someone pushes some variable
of this time and then try to rights to
the memory to the body right like the
question is I know as long as as you
write to program rights to a very
concrete number in memory so if you try
to do the number I know 64 right the
virtual machine can just say okay at the
end is 64 there is this volume right
later on or operates from 64 it's just
this value and executed right that's
that's very easy you'll just create an
array that represents the memory and you
just try the question is what happens if
the program takes some unknown variable
I would say X or whatever it says you
know right to this memory at the
position X right and then it says read
from memory position X plus 1 and you
have to figure out your whole execution
and who now has to figure out this X
plus 1 is really like what's there right
is it the thing that was written in X
and just move slightly awesome like
perhaps overwritten by something else
like how how do you deal with that and
quite quite a difficult challenge right
so you can imagine for example and are
very
cases the program says write to the
memory position eggs okay so you
remember that there is something at the
solution X and then it says write to the
memorial position 60 bar so remember the
64 right and then it says read from the
memory position X but you don't know if
64 was X so this memory was operated or
not right so so you make its target some
somepony and it's quite like seriously
difficult challenge so I looked in
January it may perhaps they improve it
at material so the poem it really
happened it was a true gentleman so
again perhaps they tasted like whenever
it reached some symbolic memories so
memory where it was written in just know
so some variable which I'll get out so
that was my whole execution and then
okay super Maria I give up I don't know
I think next action please and that's
why you didn't have a full coverage and
mr. Elkin tanks Manticore what they did
was and that was a very similar way a
diamond ring in hand with that is they
use like some very very like complex
structure and SMT solvers which which
help with the kind of managing this
algebra rights also assembly solvers
help you to figure out SMAP signals
roughly so so multiple rhesus SMT
solvers and has this complicated memory
structures and I had never begin to the
problem was that little bits so many
times and I think
Manticore and the second problem was
that sometimes the programs get so
complicated that we need them that
doesn't cut it so I spent like two
months rebuilding the whole memory model
to it all right that that's something
that I will show you which is I think we
need so okay this is the demo time
Can I grab a char yes all right
they are not locked so actually open
source TV two days ago so any one of you
it's an MIT license and one of you kids
we can see it and you know if you might
sell the sources are testament to the
power of duct tape engineering and
Kowboy call being like the best
practices in those those if you're
serious programming are all implemented
so it works quite nice but it's being
battled us at a lot of times so it works
quite nicely you just you know typing
the contract name or a short path for
crypto kitties you can't be compared so
it is around eight seconds to become
pilot fully which I think maybe like
it's way way faster the manticore it's
around the same speed as as material so
anyway you get does the sources
everywhere like for all the contracts
right but now this time I implemented
just for dead calm if you fetch eating
from from github you have this parameter
called explain that shows you how works
exactly and I can increase font size
right so so I have this one pension and
this is what you saw with the previous
step right so so there is assembly there
is stack and you can preview stuff that
is happening here right so so we have
here push right and then you have memory
load and this gets stored this as
something soaking up all the assembly
right it looks like this whenever I
encounter work whenever EDM encounters a
memory read it doesn't try to analyze it
at first so it just pushes out to the
single assignment variable oh there was
read from memory 64 like I don't you
know like I don't care like how exactly
it's tied to the rest of the thing it
was just a memory to memory 64 it's
number one variable number one whenever
it uses them this memory just puts into
the code underscore one so that's that
the first iteration that comes out of
the initial depopulation process and
then what it does is sorry I get a
little bit
so yeah what happens then is you toss in
a loop and in a loop it tries to
optimize the whole thing clean it up
simplify it as much as possible and in
case of this function for example first
thing that it does tries to inline all
the variables so it can see here you
know there is variable underscore while
it's being used here so it can mean like
it so you can put it here right easy now
it doesn't put it here and then idea why
yeah like it it's a like there's a lot
of things to analyze when you want to
invent something so this variable and
being like here because it doesn't get
overwritten for sure in the mean time
right like for sure it's not overridden
but here right now like we don't know
because perhaps this this overrides this
this memory right so I will just put in
memory 64 like it would be incorrect
because memory 64 we would mean this
power 64 this one right so so right now
we told the algorithm so for the way it
goes is that perhaps everybody involved
and then post find by line and tracks if
if the value of the variable was
overwritten in the mean time because if
it was potentially was it has to stop
the process is doesn't inline anywhere
anywhere further right so this was the
first step it went all the variables
inline them wherever possible and and
then the next step is of course in
lining all the memory the same process
right so it grabs of the memory and so
it grabs this memory and first this
memory right you can put it here
right they also sees know if thanks
everywhere where you can put it and kind
of we have it already something that
sighs listen there it goes like this in
the in circles and also tries to
simplify it whenever it can the whole
thing right so after the next iteration
we don't have the variables here because
we we could finally no replace this with
this because this is a complete value
then you can simplify things so it also
goes there and tries to figure out what
are the expressions that can say goodbye
so you can see here that this is 96
minus 64 so it's 32 then it sees that ok
this program vectors memory many 6 32
bytes so so this is essentially is so
you can also put it here and then ends
up with this super super nice very
simple thing right so we went from this
complex thing to this very tight in one
liner function and like it's super
rewarding working on that becomes a
header by the way because like the way
it is it's like almost entering this
crazy battery room or whatever which is
crazy crazy huge function and then you
you see that the compiler simplifying a
lot of stuff and then you try to figure
out alright what are the other rules
that are not given to the system that I
can implement correctly speaking and
that would also simplify the program
right and because because helium is so
so fast like like a like a festival on
thousands of contracts so so
before every release I can just look for
contracts that were it simplified enough
and just find all the missing rules and
try to simplify that and just in a work
with that and end up with something that
so one more thing that he does is no I
thought you about this intermediate form
it's also quite nice because it's it
allows us to really analyze the program
very well so you know we took it just a
few moments to write this from a figure
out what kind of partner what kind of
stuff can definitely terror right so we
can see that the function returns this
story
for example right it's very simple to
see if the function is payable because
we'll just check if there is a require
at the beginning looking for that we can
check if the function is resolving
because we can see if it gives us some
storage rights or some calls right and
if we have all of those things we can
figure out that this function is really
a gather so it returns only value for a
certain storage in this case storage too
so we know the name of the function
and we know that it's read-only it means
it's together for a different storage so
we can figure out o this storage name is
we can name it after the pension and
it's okay right we probably more or less
correctly that without you know okay
that's right
any questions
yeah also there's like a meeting on edge
cases right so negation is one simple
thing but then actually for bully hacks
I you I already put that for very
specific action names because there are
so many for such cases that I usually
don't think storage factor the bullion's
example will sometimes the bully has
returned already in Texas of our eyes so
because there's a factual code are there
any focus right they try keep the tokens
size is higher than zero so I cannot
really name the whole storage are there
any tokens the storage thing is to be
focused right so so in this case before
anything is they like very few cases
where we're actually it makes sense to
name storage after and after that well
it's funny that people ask about the
meanings and the patient's because like
that took like the least amount of time
the whole be compiler I remember
teaching soda really like you know first
question people ask and that's what this
is pirate master anyway there's the
second part and that's the move
processing and I I don't think there is
another tool on the market correct with
like there are some other people from
other other other security things but I
don't think there is at least an
open-source tool that actually handles
looks properly
that means that the last time I checked
either a materialman car or another I
think the compilers figured out loops
and I will show you what they mean so
the problem is we have some kind of a
semi right and the way it works in
virtual machine right the code that is a
loop iterates over something in solidity
because compressed to get some ties to
this so you know put some index jump if
the synthesis bigger or smaller than 0
right and then subtract come back and
just go in circles so essentially this
is now when we do a Samoan execution the
problem is that if we don't discover
what the books are we'll just see a
series is so we'll just see because the
0 increase X x0 decrease X and just go
and not be deeper into that's all as
well continue the execution or whatever
right this is super figure out it was
following do you figure out oh this is
I'm really in a loop like I'm just
throwing you know I'm executing the same
code it's not as simple as figuring out
that this equals the same line in code
because sometimes for various reasons
but you know turning this into something
like this on the fly is really like
seriously
explain exactly deliberately because I
don't fully understand around there but
it works I kind of you know like the
craziest stop by every row because I can
understand bits and pieces of it if I
hope is very hard so I think I know that
I know that it's correct but my mind
that fails to grasp the whole complexity
of what's going on there like I cannot
imagine it's go down there but anyway
it's turn here and I think some other
it's going to look like so they don't
handle this at all so that's when their
place will where they would right so for
example they will just go deeper after
they experience a timeout and they will
say okay I give up I don't analyze stuff
and occurred so this is how the reason
why I think again half a year ago with
me that Manticore they couldn't they
didn't make this connection to drive
here so I will not explain exactly how
this works but the sources are public if
you can clean up the code and understand
how the concert explained method and
then I go ahead and appreciate that it's
possible that perhaps it is but after
the first iteration then the comparator
figures out much you can say but there
was some kind of a loop here like the
program encountered so some kind of a
loop and there was this one
he takes variable that starts with zero
okay so this was that in this variable
and then who's this
here the hook through the ends so
degrees and gets back here and kind of
execute and then sometimes it goes these
paths so essentially against the program
so far unreadable right so it's it's
hard to understand what's going on here
so after the first stops that's that's
what we end up with and then crazy
awkward like terms or to not send it to
something like this which is still not
not nice enough we can also hear out pay
this is the condition because if this
doesn't get fulfilled we continue and if
it does there is some other program for
the repair nobody is here right so so
this is a condition of the road and what
we can do we can do is we just look at
the program and you say alright this
looks like the wire loops we can replace
some of this with something simpler so
there is a wire here right continue and
then the rest of the program so like
this is relatively simple compared to
like the blue protection also shows all
the power in just working and rewriting
the whole the whole the whole the
compact program because if this for
whatever reason fails like they say is
that we end up with something like this
which is still kind of writable right so
there is this graceful graceful graceful
degradation one when then the compiler
fails to understand something right so
so we you know and again inside the
variables we can we can again convert
into oh yeah so we unite variables and
then what we end up with is this loop
and I know the text is barely visible
from there like for you know like might
make you slightly happier if you are in
here
iq them understand it's very well show
there's many letters anyway so it
doesn't really about so the thing that
you have to believe but there is this
will is really a memory come you look so
it what did I see it copies this memory
from this index this memory in a circle
right so now the compiler it sees it has
so the pattern is that it kind of
recognizes have been let's say it could
prove but thematically that they're
really remember loops and they only
think that those hoops do is just move
memory from one place to another so of
course it can remove those or better and
we end up with some is just a statement
saying copy this memory in this land is
this memory to this memory and you know
like the goal when I was in the other
was really to get rid of all the loops
because who knows make it's crazy
difficult to analyze nice smart
contracts so you know like I think 495
thank you 9% of the loops we can really
replace them with some other statements
that are very easy to to analyze with to
analyze with other other programs so
like a lot of statements was removed and
you will not actually see loops in the
output code even though sexual okay it's
like there is no solidity head loops so
so it's simplified it even more that
weren't enough but if this is still not
really low enough like this is some
crazy numbers and whatnot so we continue
all the united reading so we can have
variables you can see us text okay after
some more learning you can see more text
and actually there was a lot of these
decisions here because sometimes like
what they would say they're simpler but
they would still more human readable
where should you stop right so my idea
here was okay I want to unite everything
at the start like you remove yeah in my
everything possible rings all the loops
and then kind of just for the human
readability and clean it up and perhaps
add some variables here and there so
it's more readable and yet it's kind of
different from many compilers that
that's just yeah so anyway
this is this is not the best again this
is the same code now it recognizes that
this is really an area return statement
so this oh this could be really
represented by s so this is kind of
adorable still not not as well
unfortunately this is the best there is
but it's a part of this function and the
bad thing is and I can honestly tell you
that I think it's not just amazing the
single faction I spent probably like two
weeks full-time work if not more I was
you know almost making up screaming at
night and saying ah God the world needs
to know how simple dispassion is because
this other contract and repress whatever
this contract returns so it's like this
shouldn't be here it should be not
return this what gets returned from this
code this should be this release appear
oh really and it should be like four
lines and you know the problem is that
this single function actually breaks
under certain
visions so if I just put this right here
like a like I cannot simplify further
and maintain the correctness of their
program of the translation like you know
it hurts me so much and simpler but I
would lose this correctness sorry on the
outside what it means also is the very
sick cool thing about the compilation
processed the way it's perform right
here is that sometimes infections don't
be compared correctly that means is that
really you should look deeper and figure
out what's going on there because
perhaps you know there is a reason why
it wasn't simplified perhaps just by
certain rules but perhaps there is some
edge that if that's there that's an
expert for profit as a back-end know
it's all about giving better tools to
blackhat so they exploit contracts
sooner so you can use less money but you
know if it's probably contracted $50
then like people who know something else
right anyway the cool thing is so this
was the original function right
so it really is squash and very
simplified and again super rewarding
process when you see this huge juice
function you wonder what the hell is
going on here and then you end up with
something that's almost as simple as
possible yeah so here hands like the
question is when an amenity compilers to
do systemic analysis thing where they
try to figure out they kind of try to
look at all the compiler leave use some
of the hints to speed the program into
trance and then create a graph and try
to work from that graph right so I think
that's what these do and here I I don't
do that I try to avoid any compiler
specific patterns like looking at
comparisons figure patterns and often
you know this come from you oftentimes
you know assumes there are certain
things on the stack or the very certain
structure and here there are other
things are easier like this right where
the programs were much more context
[Music]
agent Ranson although there is a part
they will talk about in a moment where I
try to analyze this chapter of the
storage but that's mostly for the naming
purposes but but you know there are
there are no assumptions about what the
executive storage structure or the sort
variables are at that point but I think
that the output could be then analyzed
and like some cool stuff would be would
be possible there I hope that this
answer is the question I noticed in your
out there there's things we're like you
have storms for your player and ask
address right yeah and it's like have
you determined that sort of thing okay I
would look up all that in a second okay
well okay and that's let me ask the
other question which is where do you
think is it possible at all were you
good an animal like jumps to like a
variable location
save women from storage that's that's
one of the benefits compared to the
control yeah this actually handles
handles this kind of stuff quite
smoothly yes because like you executed
actually that the current version is not
as smooth as the previous one but but
you actually you know you're just
executed all the jams and whatnot so
like with other tools that are more in
line with with static analysis they
oftentimes the lost or the respective
prefer results when someone calculated
the dark location or the knowledge I
hear it just calculates it also on the
fly right and exact with you know proper
jams but the question is what happens if
you like a some good examples you like
from the other compilers but anyway what
happens if you jump to allocation from
the storage right so yeah so right now
the way this handles it
it's does well it will just always talk
to a storage location of another all
right I don't think I'm encountered
do that actually yeah I mean I don't
think it's a common thing but yeah I was
wondering it's like you can't do that in
celebrities so you can this summer this
one one example
no yes yes there are other examples that
are closer to that for example dark
tables right so in my current quarter
break but interpreter yeah yes so this
approach can be used to have a laugh and
original products are used it's quite
nice to go and get some Java patients in
the memorial but not the current version
doesn't work with them as smoothly but
you know it also needs by together as a
pumpkin used to the end of that I kind
of try to work on the examples of real
contracts but keep in mind know if there
are long contract that engine sputtering
then again it can be extended to handle
death as well there was question from
here right yes so you have like a bunch
of girls my sorry
you to think carefully about having over
all that baby stuff southern Oklahoma
my name is the real implementation and
by applying one to greatly doula take
the pattern on match yeah I was afraid
to go into this kinds of roles because
like if you simplify a little you
simplify to write if you had some other
role perhaps it simplifies to something
that brings the other girls turn so
fortunately there there were that many
cases of this so so somehow it works
without putting these products there
were some cases but then you can you
know steps so it's not like I will
combine the pros where is things figure
out which part should be by which they
do some we evolutionary algorithm
something
on top trying to pick the family or part
and they can combine English maybe later
attributed by drizzle fury
maybe I mean I think what happens really
is people just use dry and embarrassed
by pedestals and see which one's the
river the best outcome for a given
function and what not so so I think
that's that's really good like the
practical practical mystically it will
be cool with this this approach like the
way I implemented it at least like it's
really like it doesn't work well with
the state exponent but but there are
like there are ways to make this
approach work just as good even in these
cases I think that from your perspective
maybe not I did not work or you can fill
out of work whether you can manually
like compiler to another yeah yeah
because I think you need to integrate
into policies it is very compact yeah
it's very complex so there are other
things that would be more able to do
you know yeah actually happening well
there are a few ways actually at the
energy perspective that so or I will get
back to that yeah you know in a moment
as well all right okay okay I try to
remember everything
I thought the president didn't come so
like a lot of things tonight okay so one
more thing that they wanted to talk
about before I come to the part where I
titled it answers to all the questions
over here I mentioned already the Jason
with your presentation at the beginning
and first talking about the table like
why these or someone else would make
something very similar it's very very
cool so like the cool thing about this
series of small letters that people from
the back don't see is extremely simple
life so compared to just you know
grabbing solidity or the stuff that
people do
hello this doesn't have for example
recursive functions or anything like
that but usually kept loose doesn't have
memory access this is almost a
functional representation of every
function in that you can use smart
contracts and this this makes it very
very easy to analyze by ultimately
ultimately tools so so there's a lot of
cool use cases of order trying to know
that all these all this in in a big
query database so we can search it with
JavaScript even a seconds and there were
some cool use cases so Constantinople
intensive greedy when there was the
content they don't perform for example
the question was no some changes in the
protocol may affect some of the
contracts but how do we figure out which
contracts will be affected by some
changes we need to figure out we need to
find and search for that right so the
way you actually found contracts that
are really affordable to a certain
exploit was by grabbing on that from the
database and searching in JavaScript all
the contracts that mattresses in pattern
and I think this was one of the two
tools that actually managed to do
content of them without help and
cooperation with a change cleansing
vehicle so so you know a huge potential
also for by some other stuff that it was
finding all the tokens that don't check
transfer function properly and allow
anyone with
that was like five lights of JavaScript
to analyze this thing and there were
like hundreds of contracts where you fit
their own vocals because they must have
decoding those skill areas if I put them
actually valid contracts that someone
had a smart young so I have to try
before releasing that if they are still
online so there were some like the sad
stories you know don't use this concept
anymore like this this approach each
other of the copulation and and this
intermediate forum and working like this
like rewriting the code it's very
important for auditing and I would say
that it will replace solidity called
auditing in full because that gives
external memory still but really working
bottom-up and taking the virtual machine
and and just monitoring it this into
some intermediate form language that has
a lot of benefit and also make very
various tools for auditing and I would
see not necessarily might be paying and
if you check the sources you will see
one of my English but it's something
like that I think that's that's really
mad for for the community to go we
support of the Northern Pass
they mean like level girls like I know
this one election looks place murder
that reasons like I didn't know that one
okay no I think it's yeah was like with
the original course that because it's
very less being less kinda like this
actually
yeah like felling off in the less doctor
after I died from her that's very very
Somalia so so so yeah I like it tomorrow
was the world so I have to take it out
yeah I would about one more thing before
I get to the questions okay that was
supposed to do anything
okay one more thing so there is a lot of
math going on there in every compiler
organizer store and most of the tools
use the same two solvers so this black
boxes were including mathematical
results and they're very nice because
first of all they are solve enterprise
like they've been written by smart
people but they listed for a long time
and they cover all the cases so so they
weren't very nice but I think surprising
really
like telling a set of rules that were
handwritten health problems and other
problems but can be sometimes faster and
and I want to talk a little bit about
how math is handled my case crosses a
comparison and I'm not saying this is
better
perhaps it's worse but I just started
doing this this way because honestly a
year ago I didn't know what the second
servers were so I just throw that my way
but perhaps it's not the best way so in
my case I think that I don't buy
information like I don't use passes for
represent a representing a long program
when you stop us so this is very similar
to like actually like the way these
represent so you know every operation
like if I could
on the stack I don't know the value it's
not the class of something is in just a
double so that is are so nice because
they're very easy to compare for example
so if I want to catch some computations
I just know like like it's it's it's
very like in Python at least it's like
one operation to to compare two doubles
if they're equal one time so it spits up
a lot of computations because I cashed
like like crazy the second cool thing is
working with this is I have to print out
form that's human readable but when I
want to test it in vitam I just pop into
the code it's already there so I don't
need to create the contractors and
whatnot so this is very very nice but
but sometimes like when they are getting
used to that it's you convert your eyes
now
the other thing is I also try to flatten
and say goodbye all the forms of
expressions so I think solvers also do
that so I can simplify stuff but I have
a very special like canonical latin form
that for a human it may not be the same
as well but but like a lot of math
really assumes that there is this form
so it's safe so the processing time is
not rules I don't want to go to duty to
that but for example now when I multiply
something the concrete body is always as
a first argument or there is a certain
order of operations so if I see multiply
something multiplied we always are
moving like this and not the other way
around so because of this like the whole
math library can
we have like a certain very small set of
rules
I've analyzed of them he doesn't have to
worry discover it involve the whole yeah
and he's faster in some cases the cost
of generalization perhaps and then I
have to invent my custom operators so
anyone that worked with with the
bytecode knows that she'd left happens a
lot of times in the contract to I shift
all the staff and move things
bit by bit by quickly by and you must
get out so so you know let's say that's
going to be number you want to top of
this center here because that's where
some something is and you move it to the
left or to the right right so like these
operators are used a lot and I simplify
like also like I simplified all the
multiplications divisions first these
operators so the local stuff would be
way way simpler and special operator
mask and shift left which is like super
difficult to figure out understand and
memorize but through the like please
so essentially essentially this special
operator that was invented that handles
a lot of operations that otherwise would
be dis complicated threesome expressions
and I think that's another part were
worried about where the compiler gets
its speed because between Acastus one
operator words the regular analyzers
have like a huge tree of operators and
they would have to figure out your
single time
together I'm not 100% sure I'm not like
a safety specialist number like this
stuff is fast so so uh that's my bad
well that went way too soon now
obviously yeah this is no because it's
home homebrew like the code is
absolutely bad so we kind of the factor
that we like and yeah it's for them like
all the rules or the match rules were
really done a testicle on all the
contracts on the maintenance so so
really like it was a very quite fast and
cool thing is that this kind of
transparent compared to ANSI developers
which are often this kind of black boxes
but the code quality is so low that
admins read so transparent and yeah okay
the next slide is the answer to the
questions hmm so I'm voting in Python
and I thought doesn't have pattern
matching at that size because a lot of
the competitors is three pattern
matching so we're trying to figure out
there is this pattern in the now
they sit with some other brothers so for
anyone that will want to try out the
code fix Python and in custom statements
until and then you know best programmers
know that this is not what you do
usually right they don't change the
language to match your purpose like if
you go into the sources you will see a
new operator that sexually pattern
matching the colors but imagine quite
them and they wanted to do that without
fixing the interpreter so you just wrap
around plain vanilla item three one day
and you can this pattern matching in
your own programs so that's that's why
even really simplifies a lot of things
why don't we point eight requirements
for this services next week they didn't
want to move Thanks so we have to wait
released anyway yes so now it's a few
answers finally to the questions then I
will talk a little bit about about the
other tools and then we have a more
relaxed way I guess some people warm
with impatience
so yeah first of all there was a
question about the national identifiers
right because there is this so the way
it works for anyone that's familiar
solidity and and the whole like VM or
the contracts use identified night runs
by four bytes so you take the function
name give a and you grab the first
or bytes of the hash and the identifier
so that every contract as dysfunctional
and only those four bytes as an
identifier fortunately someone with the
database of 4 bytes
directory called so so it's kind of you
know it has all the function names and
all the identifiers
unfortunately it's not that good it
doesn't have a lot of staff and some of
the
I think someone brute forced to fight
collisions so you can find a lot of
common passions that just have other
definitions that are total rubbish so I
had to build my own my own format
directory especially I just grabbed all
the api's that were there and I
absolutely hate spray painter stamp and
this was the only one situation that
they had to do that so I grabbed all
daily is I use them the box and they
beat my own directory so if you download
the sources like on the first round it
will download because it's a huge by
little it will download all the other
formats into into your drive SQLite
database so so there is anything like if
you're playing with contracts and you
want to have a really good library of
function definitions that's that's for
you so like the taste I love these
transfer function transfer transfer from
because success like if the modern
things were completely different like
that could be handled quite easily right
but in case of transfer the problem is
that Erie 20 tokens transfer the first
second parameter is value and air system
Antoine is item number or token number
90 right so it's different different
names and that's quite irritating
because there is no way you can figure
that out from the source
it requires human not so that's why the
fire which provides directory like the
way I know that is so weak I kind of I
look for correlations so I see oh this
is the function usually abuse me these
are attractions and disappears because
other functions and then includes which
which are more similar and tries to
guess based on that
- that is great this would submit
everything to you all right
not at the same problem and I
perspective I'm actually trying to view
more tight title arguments I see and
then yeah so okay yeah yeah I like
really like this this project of
frustration or interest I'm not
providing the idea it's like we were so
dependent like it was all the contracts
published on Facebook like people will
be like pitchforks right now all the
contracts are on the private companies
several brands that don't have easy
access and not these ones so I kind yeah
so again thank you and he said all that
the pension doesn't work properly so I'm
actually done distinguish that very well
it should be approved
like it could be improved they died is
they're just not active kind of that
there's other good thing or
interesting thing that when I decompile
are trying to figure out the storage
Isis the storage where when they have to
access arrays or or mappings it's like
you know a cache of a number that's
something right so when so DD or like
contract once taxes are a number are a
storage number two
something it has to manage number two
and add something right
so usually I just see you know hash of
this had something that's easy
understandable good unfortunately in
some cases like the compiler and the
Machine advanced everything so it was of
course a big number there and if you
know the output this big number that
breaks everything and breaks
understanding of the contract because
you just see read storage number one
right super irritating so I do do a
rainbow thing about that so to speak so
I just for some courage like I just
pretended some of that so so I reverse
engineer at fashion I just have called
the function reverse reverse 883 right
so that's the thing Thanks yeah various
other is the contract search so I can
put all the data there of the inquiry
another fun thing that I am the
hackathon I probably will really release
that sometime tomorrow next week like I
actually indexed all the contracts and
this instant search for contracts so we
can sell contract by coordinating so it
takes like a hundred milliseconds and
you can say only contracts that don't
check for owner who is calling them
before clicking the owner instantly
spite of the contract right method and
it will be super fun to raise your hand
when I release them because it's like
you know you're like I want to write
this prove that just checking just
contracts owners of you know contracts
one another
and we know that you're responsible but
if someone does it that I think
okay okay so testing how I estimate
whether this whole thing is valid so
first of all if there's no body like
don't trust 100% a doubtful that it
provides that you know wants to keep
them brief like no drugs but both
finding parts in the contract doesn't
mean that the contract is fine like
again involved I'm quite sure that the
approach is valid and again focused you
are working on a very similar thing
because formally verified so I hope one
day we'll see this approach but it for
my verified basis or like very very
solid so folks who are really interested
in that thing
heading said that the way I destitute
values I have a few cases so few
contracts with edge cases crouton Jesus
is always a must for me and it has a lot
of nice edge cases and just few basic
constructs that I check how they compare
between various versions of the compiler
and then the second thing I do again I
pushed for speed a lot right so I like
it's possible to become buy the whole
block train with invalid one day I think
right and go
so cryptokeys takes eight seconds it
used to be - like really imposed a speed
so so for release or after every update
I can just go through campus of
contracts and kind of see what's changed
or or see some patterns and it would not
and also when there is some new stuff I
can I can say oh let's throw me some
contract that kind of certain pattern
and that's
they're so so it's kind of you know on
the perfect testing mechanism but but so
far it's it's been kind of successful
like the idea that both standards would
be to have a recompile from the
decompile source right and recompile all
the decompressed contracts run the whole
block trading history and then see how
correct it is right so the transactions
return the same thing and that's it so
very nicely how how you know how much of
it is is correct like most of it perhaps
again not on the educators but that
would be super super nice mmm and yeah
this is battle tested so if you get the
guitar source like come online I played
with some other tools it was like oh we
have to download this binary and it has
to be real runtime and then you ran it
and there are some bars like really like
the common line is a simple and it works
as smoothly as possible assuming they're
quite a few more time so that's that's
the problem
okay I won't commit all this much
storage but there were a few questions
about storage right so so can you repeat
your question okay
you know yeah actually yeah I mean I
feel like superb so this is not super
because I mean they're not gonna need
like the numbers that are getting
plugged in are fairly small so you know
you know what your range there is you
know if you you know if you're not you
see enormous array of it and then you
know maybe you this be level down yeah
but then there's mappings and that
things you know you could maybe see huge
numbers put in or you know you know the
domain doesn't have to be numbers in
numbers that's enough to expose
developments but I was I was wondering
since you didn't thank you Matt is there
no problem bathrooms because they don't
pre-compute informatics or do they
pre-prepared imagine that you have to
expand your technique unfortunately
fortunately usually the like there are
mostly dead okay usually you might want
to do also it's not being similarly you
know they have to be completed them to
die because the mapping depends on song
is or whatever right but sometimes yeah
I noticed some contracts for example
notice storage number two they use the
person from decorating just plant a left
but they have some proxy contract that
the college is storage that doesn't have
a number inside like it's not expect
number about the tree or the sentiment
something has that right so so in that
case I also cable I think one or two
cases and the cool thing with working
with this approach is actually what I
did was I was I was running the
decompiler and saying okay show me all
the big numbers that are used the
storage in cases that are not yet
you know reverse engineer
you know I took a look at some of them
so this is very neat working in this way
because you just say okay let's see what
what I still didn't take into
consideration right and I'm not saying
that this is perfect like once for a lot
of things and it's easy to extend my
service when there is a new pattern you
can solve that I think yeah it starts
working in turn around some crazy stuff
there if you go into the source code of
this like that's was done right before
the release like you know you don't want
to imagine my mindset when I was working
on that but like some crazy gangster but
essentially like it's very difficult to
map storage if you want to become packed
properly you have to figure out this
storage is no storage number two it's an
already and this is the apex of the RA
and this is really a structure ER I
would not like very very difficult
well it's kind of been solved so if you
want to see like I would not even
attempt to explain how it's done but
what it's done and not perfect but the
alleys I asked you about the open
challenges to 312 well okay I will
briefly mention the folding algorithm so
I told you that there is this pain
exponent like you have a lot of these
and then you want to follow them so so
it's really like a very short thing so I
will try to expect algorithm because
it's it is like right next time
so you know how you have leaking like a
deal between two files right so now the
way I do it is I did called execution
paths I split them into linear forms
right so I do something like D but for
not 42 but like 400
time right so I married that kind of a
tree and then I do it deep on the trees
more people trees inside and they kind
of work them together so that's I dunno
I I cannot really like imagine how it
works exactly what's it's roughly that
so so the code is super handy
transparent like if you can figure out a
nice way or if you can improve using
some knowledge from the other from the
other fields go ahead and yeah so
finally a few do and now I'm getting to
the ctmc
so this is the edge cases first so there
is not that much abstraction of don't
try to make the code that is unreadable
that's much I found some of the code
that was super easy is big powers that
obviously enforcement is some kind of
security practice and some other code
was used to you can block some of the
money from being with robot so like
that's not been good like security
possibilities not removed long right
like from practice and I wanted to say
when it comes to CVS you know I liked
when I started tracking yes I was kind
of sad because he didn't work well with
yet and then it hits me
perhaps the CDF creator so you have to
check with idiom before releasing a CDF
I hope they knew by now right so so I'm
not that sad anymore because I think
there was this guy that had to check for
that and actually I spent a lot of time
some weird edge cases
thinking about guy that will be doing a
CDF one day even think that he's so
smart
and then he will solve it smoothly and
then I will in my mind say to him
in your face right so so I called there
was this mass situation where someone
trying to create this Kiev and and there
was that in-your-face moment we're going
smoothly so anyway that's that this is
the air time and I try to not spend too
much time on them because like there's
you know difficult right yeah so Castro
I'm giving a as a cooler because they're
doing awesome thing and very few people
know about them so you Larry if you
had the chance
yeah that's that's Ari so they like the
holy cities about programs in the
society created 13 years ago in a
mystical Valley and they did very soon
our staff does way much better in delays
i co2 for my oven and it works for way
more difficult started smart contracts
so for java programs right and yet and
for for cryptographic libraries and and
i hope that they get the grants or not
3d 3d push that into into our space
second thing is concepts library so it's
not everything on fire
I love the guys their website looks like
crap but it's really good underneath so
in theory like it has about some
technology underneath like similar in
spirit they just use more declarative
languages so so like if you want to work
with
like there are very good guys material I
mentioned Authority like perseverance
period and very nice penny laughs so I
guess most of us know here okay laughs
and promote verification and and stuff
that was done around maker like the
stuff that is symbolic execution and the
stuff that they are doing kind of kind
of similar in spirit against so if you
get small in execution it will be easier
to get what Caleb's enjoy although I
still don't get it fully semantics are
fails bits again now shops will be
queried because it's like I put all the
stuff there and should be there is a
theme from bigquery that is very much
into blocked any material and they are
very easy to eat so if you want to play
with required are people from Google
that that's really you know that and
there are two cool volcanics polymers
proxy for and by Alex Lee like a lot of
cool data analytics and whatnot very
open to go to cooperation and it works
I'm actually talking to box count and
there may be integration so they may
show sources from eating over there
because I think like the problem with
eater scan is that they there are no he
was on a diffuser that that don't have
the function the content resources and
gather sector scrape from them better
decompile sources and of levels the
ground because other books and explorers
can also show sources for Oregon's
highly trained security I can see the
t-shirts here yeah thanks a lot for the
convention
heading into the very article but also
like very good part and also very good
project and yeah that's why I think I
think that's released next week so
anyone can production so I want to say
like a few words like what's what's my
approach with the project what are the
next steps so really like I mean over
the last year to a separate outfit so to
speak so I just wanted you know I was
frustrated not knowing what the
contracts do it was filled with anger
like a lot of anger just put into this
finally together now and there was no
business purpose there there was nothing
outside you know I did of course some
time to just go deep and see how how far
I can go with that
attendees and all that like I kind of
accomplished in this aspect so I hope
that the community will use all of this
knowledge that can help other projects
really with with with adding some some
better stuff to the blockchain and
yeah that's why I'm super open about the
MIT license anyone using the algorithm
month but for me the purpose of the
whole project is accomplished already
and you know I'm happy to see a broad
here and I'm happy to open you know
answer any questions and just help out
over again and yeah I hope that someone
will reuse the sources so yeah thank you
[Applause]