[Music]
Thanks
good afternoon everyone my name is
Laurie I'm a cooperative cable network a
decentralized you know it changed for
the cryptocurrency and tokens but today
I'm not going to talk about Kaiba
I'm going to talk well Oriente the work
that I did before Khyber and Ont is now
maintained and supported by melon pot
right so what is int I think it's not
working
right right so what is int orient is a
smart contract analyzer that you know
based on symbolic execution so basically
you know given a smart contract event a
can just you know scan oh you know went
through the contract and you know find
all the possible vulnerabilities in your
smart contract so we released the first
version of int back into the 2016 you
know with my team from National
University of Singapore and I first
present-oriented DEFCON two in Shanghai
last year and after after my
presentation
Mellon port you know Rachel and they
wanted to support the development
appointee so and today o enter is
available online at this URL if you are
if you have your laptop with you you can
check it out so here's a github URL
Oriente as well is I mean Oriente still
under active development so if you have
you know you wanted to contribute feel
free to go to github and start exploring
right so first of all what is symbolic
execution the techniques Baha'i Oriente
so I will use a simple function here
that you know get the bonus given some
you know contribution amount in some
token sale right
so if the amount is like greater than
hundred Eater then the bonus is 15%
otherwise you know if the mouse is
greater than 50 Eater then you get 10%
bonus otherwise there's no bonus for you
so if you look at this function there
are three means there are three main
branches in the entire function you know
H is greater than 100 and you know H is
greater than 50 and less than 100 and X
is less than 50 eater so symbolic
execution allows us to explore the
possible parts of the program of your
functions and
it will record all the you know contract
behaviors in its part right and it will
summarize all the behaviors in something
called a part condition here you will
see that for every part we will have the
condition for the input to drive the
contract or the program to that part
right so with this summer right part
volition with this summer right heart
condition we can we can easily check if
some prob some property is violated so
for example we can check whether if you
know H is less than 50 and you know the
bonus is still greater than zero so the
way we do it is that we encode or the
part condition and also the property
that we want to check in some Terim
proofing language and and you know we
use some tour improver or server to
check the feasibility right so we can
check we can use the theorem provers
over to check the feasibility of you
know the you know property violation
right so this is the main architecture
int so our intake works with you know
the EVM by code and it also detect the
interim state into account so given the
by code it will generate the control
flow graph of the contract and if we use
simpler execution to explore the
possible part and you know for every
part we will just analyze to see whether
you know some properties violated and of
course we use the theorems software here
to check that and if if I want a flux
and above then there is a validator
component to check whether the buck is
you know found positive on our so what
is the main difference between int and
you know other formal verification
technique so Oriente basically you know
try to find all the possible part in the
program and see whether you know some
buck or some
property is violated on the other hand
you know form of verification allows you
to formally prove that you know if you
know some the the correctness of some
runtime property of your contract a
program right so orient it doesn't
orient it doesn't guarantee the the
absence of some buck right it to say you
know I have checked you know this many
part in the program and you know these
are the bucks that I found on the other
you know eientei is easy to use and you
know goes for most of the existing smart
contract but for form of verification
you know sometime you know it doesn't go
automatically so maybe it requires some
people like Joey or you know some other
people's presenter to - you know
configure the program and you know run
it with a tool and right so what are the
new features that we support in Oriente
after the DEF CON presentation I will
quickly walk through all of them so the
first one that we support is you know
checking the assertion violation in in
the program so you know developers they
you know sometimes they make some subtle
mistakes right they are not even aware
of that so for example this is a simple
function that transfer the token from
you know the sender to the receiver so
any of you can detect you know the major
problem in this function
oh oh sorry this is this will be - sorry
yeah right that so I can just quickly
fix it but there's an right right
sorry this is the naive but right there
is more subtle but sorry what right this
is another naive box sorry yeah um
another naive buck
mmm not really
okay right so what happens if sender and
receiver are the same so this guy can
just you know print more token out of
thin air right so this is really subtle
and you know it happens in one of the
contract that we have audited before so
with int it can check you know the this
you know if we add some assertion there
and Oriente can check whether this
assertion is violated before you even
deploy the contract on the main air or
test net so I can just quickly show you
the demo right this is another no bug
right so this is the the live version of
int it's a you know oriented Melander
network so you can just click to compile
with right click to int and analyze
Oh something's wrong sorry I get back to
it later but you know right
but basically you know you can with
oriented you can shake you know whether
some assertion is violated before you
know you evenly deploy the contract to
the manor or test net another another
feature that we support is you-know-who
loop handling so if you ever you know
work with you know program and analysis
you will know that you know handling
loop is you know a nightmare
right because basically you know loop
can just force the analyzer to run
forever and you know did make the
program termination non-deterministic so
this simple function here can just make
you know eientei run forever because we
have like no idea like what is the land
here right what did the lands at the
value X array X so in Oriente we handle
loops in different ways so first of all
we allow the user to specify the gasps
limit so oriented we just keep exploring
the program until the gasps limits is a
rich we also like allow user to specify
the number of iteration that they want
they look to be to run right so here's
the argument that you can use orient a
user can also like specify the time out
that they allow wanted to run so after
that time I oriented with this you know
stop another another thing that we added
after the DEF CON to is you know making
Oriente more dynamic so so when you when
you analyze so Ont is based based on
static a similar execution so that means
we only care about the contract itself
we do not care much about the
environment outside of the contract
right so for example if the contract
cost
another contract then we do not like
analyze the the contract that you know
this contract is calling
so with Oriente we allows user to set up
a customized blockchain or environment
so you know so you know when this
contract Co another contract then
Oriente will go to that contract SQL and
analyze it so this is how how you can
specify the environment to work with
Oriente so it looks complicated but
basically you can specify the gas limit
the difficulty of the block the channel
data that you know you want to send to
the function you can also specify the
archive state including you know the
balance and the storage of some of cloud
so there are a bunch of new features
that we are planning to air the first
one is to generate all the test cases
because you know Oriente visit order you
know all the possible parts of the
program right and it records all the
behaviors of the program so it is
possible for oriented to generate the
corresponding input that drives the
program to the same part so basically
you can you know use all the other
generated input as a test guy for your
smart contract and use it in other
framework like shuffle we also plan to
like simply simplify all the constrain
in the park condition so for example if
you you have to condition like you know
actually it's greater than zero and Isis
small less than 2 then we can simplify
it to you know X equal to 1 so that will
reduce the term that we query the server
or the theorem prover we also Li want to
reduce the number of font positive
reports in order to provide more helpful
feedback to the developers so these are
all the other new features that we are
going to add in the in the near future
right so with that I want to conclude my
presentation
again this is the URL to the github repo
and eientei is available online
these are automated developer volunteers
that have you know been contributing to
the project and again thanks to Mellon
port for sponsoring and you know further
supports over
[Applause]
[Music]