okay cool
so today I'm going to talk about a
recent project in smartphone check
security namely eientei making smart
engage smarter to see the joint project
with my team from NUS and yo and us
college so okay so we all know that
programming security is hard because
especially for you know complex program
because your system or your program may
have you know multiple components and
the adversary or the attacker can choose
you know to attack you know any
component and to exploit your system so
that's well you know people say security
can be no stronger than its quickly you
know component so programming smart CQ
smart conjecture is even harder because
because of several reasons
so I myself you know smartphone jackass
on short programs because you have only
cha only one chance to make it right
once you deploy it you know it's really
hard nearly impossible to you know
change it if if you find any flaw in the
you know contract and secondly you know
the execution model of this mark inject
is a little bit different it is executed
by the consensus model running on the
blockchain and the third reason is a you
know we use new language with a little
bit we we have a pretty much similar to
the existing language so often people
you know make some assumption about the
language which exists in JavaScript and
Python but do not exist in solidity and
answer pen so that's why you know we
have seen a lot of you know problem in
our smartphone checks for example you
know the Dow with our tree engine see
work you know eater dies with a gas
problem can you be thrown with the same
you know instruction so the question
that we asked before we started our
project is you know others others buffs
that we don't know you know you know
existing platform and secondly you know
how many smart contracts are there are
vulnerable
so surprisingly you know the number of
smartphone checks is increasingly it
post it potentially starting from you
know 2015 so right now we have roughly
120,000 smartphone jars and we want we
really want to quantify you know
among these con smartphone choice how
many of them are vulnerable so there are
several challenges first of all you know
contract costs are not always available
see see what we see when we write a
smart contract but what is eventually
stall on the blockchain is a binary code
which is compiled from the high level
code and you know you can use some
disassembler to you know to translate
the binary code into the by code but
it's still really hard for you to make
any sense of this and secondly we have
so many smart contracts to and analyze
and you know if we have someone really
good who can you know read the bytecode
is still you know takes them several
years to analyze all the 120,000
smartphone charts so what we contribute
in this project is first of all we
identify new smartphone check box namely
generation Auto independence and tons
time dependence and we talk about them
shortly
second we introduce Oriente the new the
analyzer for smart contracts which is
beyond simply execution so eientei can
detect all the popular box including the
known and their new ones so we one
oriented with almost 20,000 smartphone
charts and we were able to flag you know
roughly night of Zen of them as for
narubu okay so what is generation order
independence so I will use a simple
smartphone check to Allah to illustrate
this problem so here we have the the
puzzle solver contract break you know
allows the owner to set up some puzzle
and you know anyone can and and then he
deposit some ether so that anyone can
submit the solution for the Paso to
collect the reward
and you know if the owners see that the
prewar is a little bit low and the
pizzoli is so hot so so he can update
the reward to attract more more uterus
so now let's consider this scenario
where you know some users submit the the
a solution would include their some of
the same generation would include a
solution to the to the contract so some
miners they include the generation in in
his block and then the submit solution
is trigger the others received the
reward if his solution is correct so
this is totally fine but let's consider
this scenario where you know we have the
owner saying a different generation at
the same time to update that we were to
0 so now the miners can you know see
like a set of generation in his block
and he can freely decide which
generation to include and which an
adjacent to it know and which order
between the generations so for some
reasons he includes the generation which
update the reward first and then the
submit solution generation later so now
there appear reward is executed first
and the Ballon is set to zero and then
the submit solution generation is
executed now although the you to submit
submitted a correct solution he still
get 0 reward for his solution but he's
unfair so the problem in this generation
are independent dependence Bob is a you
know they're the state that the the
either observed when he when he submit
the generation is different from the
actual state of the smartphone check
when the connection is executed and this
can be a you know coincidence because
you know to generation can happen at the
same time or the term right but it can
be a malicious scenario because you know
if the owner saw the targeted generation
from the victim which includes a you
know correct solution for the puzzle he
can you know on second letter saying a
different
Chanin to abate the reward and now the
to generation until enter the race and
you know the owner has some non zero
probability of winning the race so
that's it for their generation or
independence next thing you can spend
time stem dependence so we know that
interim allows this mark on check to
access the block times time within the
contract and really we we have seen two
main use case of these thumbs them first
people use the thumbs them as a random
seed to generate the random number and
secondly they use the timestamp to to
simulate the real time and the problem
with with with these two Eve's case is
that you know the tough stem can be many
manipulated and the miners they can vary
their block times them to you know the
value of weight by us them so they can
totally buy out the output of the
execution to their benefit you know
either
in both of their use cases so in our
papers we propose the solution for both
of their problems so I think you can
take a look at the paper you are
interested next I will talk about int
their analyze analyze that for smart
contracts so here's a high-level
architecture of int which is based on
symbolic execution so eientei takes the
bike or as an input and then based on
the bike code we generate the control
flow graph and from the control flow
graph we pass it to the simple Explorer
and we will explore the possible part of
the program so for every part that we
can explore we we said we forgot it to
the core analysis which will be take
whether the part of the program we
detect whether the part has some you
know prop some problem that we want to
be take and if there is we will forward
to the result to the validator to
validate whether the the Rizal is
positive so
a little bit more about symbolic
execution so this is our control flow
graph we will visit every single
execution choice at the program so given
some input X we will you know collect
all the part condition which eventually
we essentially summarize or the
execution characteristic of that part
and for example we want to check this
property whether Z is equal to X plus 2
with us you know most other condition
together into one which simplex formula
and the rest is used to ask whether
there exists any instant of the input
that satisfies this formula so in order
to answer this question we send the
formula to the theorem prover which ec3
in int and this theorem prover we say
whether there exist input or not and if
there is it will generate an example for
us so what can orient they do Oh aunt
they can detect but in existing smart
contracts as Isis described and we run
eientei with you know almost 20,000
smart contracts back in May 2016 and we
were able to detect all the popular box
back then this is the number of box for
each category and second orion taken you
can be used to prove the test generation
because symbolic execution allows us to
cover all the possible paths of each
program understand we can based on that
path we can generate one example input
that drives the smartphone check to that
I secrets in part and I thing is open
source business really believes it two
days ago you can go to that to that
github repo - you know clone to and
contribute to the project there are a
lot of future work that that we can do
to improve their you know performance
and functionality of their project us
for example we can support more of
course right now we discover you know a
large fraction of the EVM of code but
not all of them
we can also handle the loops precisely
or we can combine you know static or
dynamic a simple execution to reduce a
rate of fun positive so with that I want
to conclude my presentation thanks
thank you very much light