foreign
[Music]
secure contract using fuzzing
before we start just to get like a sense
how many of you have used the kidney in
the past
echidna it's a what we're going to
present
okay
okay so who are we so Gustavo Greco and
myself Rosner Feist we are both security
researcher at trail of Beats if you
don't know us we are a company where we
specialize in high hand security
technology we have expertive in
blockchain but also another topic for
example we do a lot of cloud native
application or we do a lot of
cryptography with like weaker stuff and
so something that I think differs from
other company is that we spend a lot of
time trying to apply research and
program analysis into like our daily job
as a result we have built a lot of Open
Source tool you might know slitter which
is a static analyzer for solidity a
kidnap we are going to talk about it
today but we have a lot of other tools
for example tiller which is a static
analyzer for algorand armana which is
static analyzer for KO and so on
four techniques the first one is using
unit test the second one is using manual
review and the two last technique are
using fully automated or semi-automated
technique
I'm assuming everyone here is familiar
with unit tests you should use any test
and they are good usually to cover that
the system is working as expected in the
happy path something that we have
learned over our audit and I know those
analysis that we have done is that there
is no correlation between the quality
and the quantity of the unit test and
the likelihood of having high severity
vulnerability and this is we actually
have an academic paper on this where we
have looked over like all the audits we
have done and this is a correlation that
we have not found and the reason why our
intuition tell us that when you are
going to write unit test you are going
to try to cover happy path things that
are supposed to do in the correct
execution while vulnerability usually
lies in the edge CAD in the things that
you haven't considered
an example of a unit test the second
technique that you can use is manual
webview so you can go line by line and
try to understand what the code is
supposed to do what is actually doing
and if there is like a difference
between both doing manual review
requires specific set of skills it's
time consuming it's it's it's kind of
difficult to do usually you are going to
go through a security company to do a
security assessment um to have people
that have this specific set of skills
the next technique that you can use is
using a fully automated tool these are
like the two that are going to find some
of the common bugs you're just going to
click on the button and the tool is
going to tell you there is this type of
work or not for example you might know
Theta which is our static analyzer for
solidity this type of techniques might
give you forth running
um but they're also really powerful
because I might cut you know like a
critical bugs
you
oh yeah
okay
okay so first Rita like the best
technique is spend one hour like the
first time you try it uh there is a
triage mode so once you have triage like
the ways you as I won't show up like in
the next execution and if it takes you
like one hour and at the end of the day
you might be able to catch critical
vulnerability I would say it's worth
going for the first result
and look we are we have like a list of
trophy for uh Twitter that demonstrates
that we have found a lot of like actual
bug using it so yeah there is like a
false positive pass for for false alarm
but it's not going to take you so much
time and it's going to provide you value
for example we have a git abduction with
Filter when you can connect it to GitHub
on every pull request commitment
depending on how you are going to
configure it it's going to run if to see
if you are introducing new new
vulnerability yeah perhaps sorry perfect
perhaps next uh Year we will do a
slitter workshop on you
and this is open source and it's free
okay the last technique that you can use
is using semi-automated analysis so
these are going to be tools for which
you are going to provide some
information for which you are going to
have a human intervention to explain to
the tool what you are looking for
and this is a bit more difficult to use
because it requires like this
interaction from you know from the user
it's a Technique we are going to see
today with property by testing with
action now
so what is property-based texting
to understand how it works I have to
introduce fuzzing so first thing is a
standard program analysis technique that
is used a lot in traditional security
the idea is basically you provide a
one-time input to the program and you
try to see what's what's going to happen
you try to stress this with random input
the most trivial uh further that you
convert you just go on your keyboard and
you know you patch random bottom and you
see what's going to happen on your
program
um again it's well established in
traditional security we have a lot of
tool if further go further and so on
however most of the traditional feather
are going to look for memory corruption
for crash in the program
we don't have a lot of memory corruption
on solidity there are some but they are
not that common what we are going to try
to look for is a property of the system
that can be broken and this is why we
call it property based testing basically
the way it works is that the user is
going to define invariants the further
is going to explore one Dome is a
program and it's going to try to save
the invariant odd or not
you can think of you of feeling really
as like unit tests on steroid well with
unit test you try one specific value
with the program while first thing is
just going to try randomly a lot of
different value
I've been talking a lot about invariance
or what an invariant an invariant is
something within your system that should
always be true it's something that
should never be false or that should
never be not possible to check if it's
actually holding
so I'll talk also about ekina so echina
is our further for smart contract
interpensers we have been using it for
like four or five years even now uh in
all our audits you can see a list of uh
match your code base actually using and
I've integrated Echidna in their process
for Aquino we are focusing on the you
know ease of fuse so the invariant are
going to be
describing solidity we have a GitHub
action similar to slitter
and we support all the compilation of
framework if you use Foundry are that
Bernie travel whatever we're going to
support it because we are using it in
every of our audit and every now and
then someone comes with a new
compilation framework
okay I was talking about invariant so
let's say you have a token you have a
Neo C20 token it has you know a balance
you can transfer token what would be an
invariance
an environment could be that if you have
a total Supply
no user in the system should have not
talking to the total Supply right if you
have 10 million of token if a user of 20
million yeah something is wrong
the way it works is that you're going to
take the contract in solidity you're
going to Define invariants which are
going to describe what you are trying to
check
one way to do that is to create
functions that are called echina
underscore some name this function
should work on a Boolean is a Boolean is
true the property or if the Boolean is
false or the property is broken you give
both to Akin now Akinator is going to
explore one Dominator program and it's
going to try to see if it hurts
foreign
for you
so we have we're going to have a couple
of theory of exercise where you're going
to try to apply again now and to Define
some invariant on the system you can go
on this repo or you can scan the QR code
to object repo
check out the Defcon branch and open the
first exercise
if you have any problem to install Akin
now if you have any question let us know
we also welcome everyone who is not into
the exercises just to see even even if
you're already uh know how to do how to
do testing or even if you if you use
fasting every day uh it's it's totally
fine we will happy to take uh any
questions simple or more advanced about
how Echidna work so please feel free to
to do it
and we will take 15 minutes for this uh
for the first one
okay so the question was what are the
benefits of using Echidna other Foundry
um so first I think echina has more
features than friendly at the moment
they were developing Foundry for like
six months we have been using a canine
like four years
we support any compilation framework so
let's say you are using r dot because
you want to do integration test and you
need some complex setup using like
typescript or whatever
if you move to Foundry you're going to
have issue because it's more difficult
to you know create this type of test so
you end up in a situation where you need
to have a setup with two different
compilation framework if you use some
Advanced options then you have to need
to have like both Advanced option in
both compilation framework if they
support it and it's a lot of you know
like maintenance
um here we are like you know agnostic to
the compilation framework in that sense
we have we're going to talk about that
later we also have like a couple of
advanced features that the others I
don't have for example something that
you can do with echina is that instead
of trying to find
in there that are broken you can look
for functions that consume most of the
gas so you can list the further one and
give you a summary of okay I can learn
this function with this parameter and
it's going to Output this amount of gas
and if you are looking you know for on
this type of things uh it's very nice
hey there uh Brock from Foundry here
um I'm curious uh how
do you go about benchmarking uh a fuzzer
right so how do you
um because it's something like for us
it's just a black box yeah and yeah okay
that's a really good question and even
in like traditional Feathering you know
like if you go like in the literature of
whole feather or benchmark
I would say that most of the benchmarks
are poor or one of the issues that when
someone does a benchmark to you know
benchmark their own tool
there's a bias all right so we we have
Benchmark we have our own Benchmark to
try to see you know like in our past
audit and everything how it works and
everything but obviously we have a bias
like it works well for us because we are
you know building the tool on our
example
um so I would say like the best place to
have like a good Benchmark for fuzzing
should not come from to level
yeah yeah it's it's also an open
question what is your benchmarking like
if you if you are if you're saying well
this is faster than this sort of thing
but it could be executing just always
the same thing like you know calling a
constant function over and over again is
going to be faster than calling some
deep deep part in the in the call uh on
top of that you have like bugs what
about like finding bars how much bugs
you found and there is there are a
couple of academic papers saying that
some people uh like to compare this but
you have a like um like a plot saying
how many Bucks you found and let's say
that one faster is better than the other
but you don't know if the next hour you
will have a a peak saying well these
found a lot of things so there are all
the things that you can do so you can
use coverage but also coverage is not
going to give you like uh uh it's not
going to be the the ultimate answer so
it's it's still a debate how long you
should run faster for a benchmark or
even for you know testing something
it's also a debate what you what we
should use for benchmarking uh should we
use like complex defy applications like
but how many of them we have like 10 or
20 we don't have thousands of different
device so it's it's uh we we definitely
are interested in a deeper discussion on
how to have a good band merch set for
for touring and we have the same problem
for example with Rita well how do we
Benchmark it our static analyzer provide
good weather and it's tough
um we usually tend to have a practical
approach in the sense that if the truth
provide value during our audit if it
helps us you know to find bugs and we
make us faster
that's good enough for us
yeah and at the end of the day also
depends on the invariance if the if the
if the developers don't know how to
write good invariants then no tool is
going to provide some magic
um value so it's it's it's tough
okay okay and I'm happy to discuss with
with The Foundry team or any other team
doing doing fasting we will will be here
uh today so please let us know okay my
other question is regarding like the
tool is only for passing for its support
like symbolic execution or something
like that so yeah you want to yeah it's
it's only for first thing we have
another tool for symbolic execution
which is called Mantika
however and something actually we're
going to discuss later
I think in practice any formal base
method approach is going to have a lower
return on investment at further if you
have two weeks three weeks to work on a
project you know and you want to invest
some resource to increase your
confidence in the project first thing is
the best solution yes and uh and also we
found that so Echidna is a tool that
works with our static analysis leader
that gets value so you have in some
cases like let's say that you have a
test that says if x equal to some some
value some uh traditional fossil
techniques have hard time to deal with
this but what we what we do is constant
mining so we scan all your code look for
these magic values and we will play
these magic values and some mutation of
that from time to time so or fossil
should be able to get inside the inside
this if you if you if you have a test
case that is not that is not working
please let us know and we can try to to
see it but in practice it seems like
some of the typical use cases for
symbolic execution in which you have
constant uh Magic values to to look for
they can be replaced by uh constant
mining extraction
how many of you have issued to install
Akin now to one like the exercise
how many of you have issue like
installing akina or opening like the
different exercise
okay
uh no you you you you you have to open
your terminal and a kidnap will
deploy the sort of unit is still
installed the tool and when you put like
equipment you cannot test some contract
it will compile it running inside the
simulated blockchain and give you the
answer so you don't need to connect into
something
uh so yeah going to them into the
repository and it says like yeah
yeah so yeah this is like your
traditional one but if you go into the
Devcon branch that is sorry
yeah so it's it's it has more specific
yeah so so over there you said like if
you're using Mac you can do that that or
you can download
okay yeah
okay yeah so I wanted to highlight one
one little feature that we are testing
on Echidna that is
that is also used in fasting but instead
of testing a property where we are doing
minimization or maximization of some
value so this is an a new thing that we
are that we are testing it is not
property based testing but it's it's
something it's something that we are
trying that we are trying to push so if
you want to know if a user is it's
capable of uh extracting tokens from
your system without you to realize you
can use that feature just saying uh Hey
Echidna can you maximize this balance of
this account so it will try to generate
you the maximum sequence so it's it's
it's a little bit outside this but uh
it's something that we wanted to mention
okay so
our Target here is a token
um it has a transfer function like a
classic Crosshair function you enable it
from a possible contract which is like a
basic possible system
and what we want to try to do here is to
create the invariants such as no user
should have a balance above the total
Supply
test the tokens where we are going to do
it is that we are going to inherit the
token or Target we are going to create
the contract test token we are going to
initialize the balance of the colors of
the first user to 10 000
and this is an initialization so you are
creating a token there is 10 000 in one
address
and no the invariant is simply that
um no user so the user should not have
more than 10 000 okay again you deploy a
token 10 000 token to one user this user
should never have like 20
000 token all right
and if you want this with a kidnap a
Kina is going to tell you that this
invariant is property on total Supply
was broken it failed and it's going to
tell you how
and the answer is that you just call the
function transfer with the destination
address 0 and
1093 token so what happened here
this was compiled with solidity 0.7 so
there is no overflow and underflow
protection
so there was an underflow problem here
where if you try to send more more
tokens that you have a new balance the
balance is going to render flow and you
know you have a really large
balance something which is interesting
here is that we Define the invariance
you know
without looking at the code without
looking at the function we were not
looking is there any issue in the
transfer function we just Define an
invariance and by doing so we can
realize that there is a bug in the
transfer function
um so this is a kind of a nice
a way of trying to find bugs because you
don't look at the individual function
necessarily you can just Define
invariant and the further is going to
try to break the environment for you
does that make sense any question yeah
okay
so
okay so the question is does it execute
a specific function or how does it know
which function to curve the answer that
is going to call everything
so in this token if you look at like the
word source code you have a transfer
function possible function and like some
additional function so the federal is
just going to call everything
and
everything external or public like
everything that a user can call
okay the question is if you have a very
large token or very large contract you
have a lot of function
so here you can take different approach
either
um you want a keynote to call everything
and you just do nothing and you let it
now when uh which might work no it
depends on what it is if you know that
some functions are more important and
you want to Target you can change in the
configuration configuration file of
echina and tell him call only this
function or don't call this function so
it depends what you are trying to look
if you want to increase your confidence
you should call everything if you think
there might have an issue in a specific
function and you want to focus on that
you can you can Blacklist on white list
depending order
okay so the question is can you define
the order of call
you can Define the order of the
initialization but not after that
I think it was another question
no okay
okay
so the question is
um can you have like a better log
because obviously this is like a simple
example uh and when you do want them you
know exploration you might call a lot of
functions that are not necessary for
what you are trying to to call right and
the answer is yes
um so Echidna does what we call
shrinking where once it found a way to
break the invariant it's going to try to
reduce the choice so it's going to
continue to First more or less on the
seminal iteration uh and trying to
reduce like the size of the of the trace
foreign
[Music]
Target so you're going to try to have an
invariant
um on the same token
the first invariant was that
no user should have a balance above
total Supply here as we kind of hinted
before now this is a possible system so
it's a system where the owner can pause
or unpause the system and what we want
to verify the environment we want to
have is that
if there is nowhere now and the system
is pause can someone unpose a system and
this is what we're going to try
and yeah let's take 10 minutes for this
one
I'm going to show the solution for the
second one
so it's the same Target that for the
first exercise but here we are going to
focus on the contracts that were
inherited by the token you have two
token now you have two contracts right
ownership and possible and here you have
a system where your owner and you can
pause or resumes as a contract
and what we want to check is that if we
drop the ownership and we pause the
system
is it possible to unpause it so here we
have a bit of initialization to do what
because we want to drop the ownership
and we want to put the system we are
doing this in the Constructor so we are
calling pause and oh no from now on the
system as a contract is deployed it's
pause there is no no
the invariant is then just if the
variable that you know tracks the
possible state of the system is true and
this should hard work you pause no
ownership it should be always post
and I cannot tells us that it actually
failed and the reason for that so this
is kind of like an old bug that were
really frequent and common in old
version of solidity
there was no constrictor keywords and
where you were doing the Constructor
that you needed to have the function
name which was a match with the contract
name and here you have the contract
ownership and a function owner and
because of that the functional is a
public function and anyone can call it
and become the owner this does not work
anymore with more you know modern
version of solidity but the type of bug
that we are finding a bit more a bit too
much in the past
something which is interesting again is
that you know we did not look at the
ownership contract we did not look like
at the implementation itself we just
Define an invariant and without the one
of the further one and you found the
environment for us
so now bring the question on how to
define it okay
foreign
okay
so the question is is defining invariant
part of the auditor you know work uh yes
like we are using a Kinder in our audit
and during our audit we are going to
Define invariant and something we are
going to do that we are going to discuss
with the developer because the
developers know you know better than us
what the system is supposed to do so we
are going to have this collaboration
with them to understand what the system
is supposed to do and to Define this
variants
foreign
how to define invariance
because you know like
if you have bad invariance it doesn't
matter what you are doing you know if
you are using further if you are using
like formal method if your invariant are
not good you're just going to check for
some things that you know doesn't matter
the best approach to writing variants
is not to start with a tool it's not to
start with you know writing down
solidity invariant is to start with
English
open a file and markdown file or
whatever I know a format you like and
write in English what the system is
supposed to do start simple start with
invariants that you know you know are
true start with things that are not
working
once you have 5 or 10 simple invariants
buy them in solidity and when the
further on top of them
if the invariant are all holding then
you can go back to thinking about the
event of the system and you know go more
deeper into into the environment
themselves if something is broken then
look if the invariant is incorrect or if
there is an actual bug
and iterates go over
um yeah in in our experience when we
work with uh with um with clients when
we ask them to do step one
undefined invariants they are actually
uh they they realize about bugs so it is
already a good a very good thing to
start thinking into that even if you
don't if you're not testing yeah
okay okay so if I understand correctly
the question is that can we connect this
to mainnet okay
okay how to use it with other contract
so you can just in the Constructor
deploy the contract uh something that we
are not going to cover here but we have
a tool which is called itino which is
basically going to take your unit test
take like your suite and we play them in
Echidna so for example if you have like
a complex integration with like you know
you are deploying in your unit test 10
different contracts you are deploying
like a knockoff unit swap or whatever
you know you need and you can replay
this in the keynote so that everything
is going to be set up
yes yes I I uh I think there's some a
little bit something else there that you
want to what if you want to Define an
invariant on a uni swap contract right
that you that you are using that your
contract is is is using so you will need
to know how Unison uh Works in order to
put it in your environment like if I'm
swapping something then I'm getting
something else right and in that case
you need to realize that it's difficult
to write invariants with other people
called right despite despite this is
working and everyone is is using it but
every time that you use a third-party
contract then you have you are
importance on risk and you need to
completely understand the other contract
in order to know what is going to the
effect in your own country I
so there is case was we have a special
uh I'm from gearbox protocol and we work
on composable Leverage and we have
adapters because we just provide
leverage for some other contracts so
when you combine gearbox with uni swap
you get immediately
um margin trading and in this case it
has adapters and these adapters
incorrectly Parts path to make check
after uni swap however they integrated
and may call to existing uni Swap and
guy who were on immuneify problem he
write a small test and this test show us
that if you really add some additional
part of call data it could be
interpreted incorrectly so we have two
different ones our system could be
fooled check not
Z balance which should be checked and in
this case it was a fault of the system
and the funds could be drained and in
this case I think we could find some
fuzzing testing to really provide any
information but this test should work
with uni swap because we behave in
different way and we shouldn't cover
that because we run with mocks and MOX
of course was created with the same bug
so MOX was okay but real implementation
total different and I definitely believe
that fuzzing should found this mistakes
yeah yeah definitely definitely when you
are creating a mock you are assuming how
everything works and if your assumption
is not precise enough it will it will
you won't be able to detect something
and we as an Auditors it's it's common
that we have to audit contracts that
will interact with other other contract
let's say compound so when we go into
compound we have all the documentation
and says well compound word like this or
like that when we look at the code and
see some things are not documented and
we go back into the developers and look
look if you're if your contract is doing
this so that it will revert and you're
not testing for that so it's when you
when you are using a third party uh
contract you are importing the risk so
either either you have really good tests
or you even uh make sure that you
understand everything otherwise it will
be difficult to catch the uh but yeah I
think this type of work can be found
with fuzzing like the most like the
difficulty is going to find
initialization that makes sense and then
that makes sense
um that's why that's why you know we are
kind of in putting like the infances
onto defining environment because this
is like the key component of this
technique yeah
uh
in terms in terms of speed is it okay to
put all deployment script into
Constructor because of course if you
deploy such a huge system and you deploy
some contracts from external
repositories like uni Swap and so on it
requires time and of course when you
want to test million operation if you
redeploy each time holds the system it
could require hours or days I know yeah
so so so when you use Echidna you
deploys only once and then the when your
test finish it will go back to the
states after the contract is deployed
there's no need to redeploy it and that
is why we have we we ask the developer
to have fixed amount of parameters in
the deployment right on the on the on
the Constructor otherwise we will know
what what we should deploy yeah I think
there is a question over there also
um I'm just wondering as you uh once
you've kind of defined your invariance
um and I imagine you guys in your audits
you you run through these and
um
basically I'm not trying to understand
when you guys have confidence that yes
the this is a good invariance uh from
and and if there are any metrics that
you guys use uh internally like I see
it's outputting Unique instructions and
unique code hashes those sorts of things
that uh give you confidence in in what
you've done
so in practice you know you can look at
the coverage but usually coverage is not
a good indicator and In fairness like
you know when we do that we do this in a
time box manner so we have two or three
weeks to do it and we're going to do our
best in two or three weeks uh that's the
best that we can do yeah it's it's it's
we there is no
uh Silver Bullet for this
um it
we when we do a report we list the
invariance that we test so it's it's
clear what what we tested and what and
everything else was was not tested with
all so we will perhaps did Manual review
or use all the techniques like Slither
to check some some other things uh but
yeah unfortunately there is no uh good
way to to Define this uh but perhaps I I
personally think that talking with the
developer early on the invariance it's a
really good thing it's usually the case
that we think an in barrient let's say
that some some value cannot be zero and
we go into the into the client and says
is this an invariant we don't know
because we have not designed the system
and they don't know and if they don't
know that's that's an issue right we
should we should absolutely know what is
the behavior of the system and and if we
don't know if anybody should should if
something should be an environment or
not then we should go back and rediscus
that and yeah Security in general is not
binary it's not you know yes or no it's
really a matter of how much resource you
want to put into it and moreover social
put more confidential
thank you
thanks I have a question actually more
related to the earlier question which is
a big
uh class of bugs that's been occurring
recently and for a while now are
re-entrancy bugs right how do you deal
with finding
um violations of invariance that
correspond to external contracts in that
way
okay so this is a really good question
and in my opinion the best tool to find
way on Transit is static analysis so the
question is more to find which technique
you should apply for which problem and
for things like Korean transition static
analysis is just going to be better
you can use further you can create like
random callback and things like that but
in practice static analysis is just
going to outperform any further this
work uh that's why like for any any
class of vulnerability which is kind of
a pattern base you can use static
analysis and it's going to be better in
my opinion
foreign
one more question what's your addition
for example we have a complex system
and we want to make a classical fuzzing
with the kidnap and it seems that to
really cover many cases it requires a
lot of computational power so maybe can
you advise some cloud provider or how to
do to run it maybe for a week with very
powerful computer to get something
achievable because of course this pretty
simple contracts could be found on my
MacBook but if we go a little bit
further many contracts many setups maybe
it requires more computational power
um so
do you want to talk about the kinapad
so the question was um if you want to
run a key down the cloud or on a lot of
you know a large like system how can you
do it yeah yeah so so so the first thing
that uh you should know is that uh
uh very large contract it can take some
amount of memory so first first thing
get a good server with with a good
amount of of memory and CPUs
um so the second thing is uh every
um we have a python companion tool
called in a parade that will run echina
in any number of uh any number of uh
concurrent
um uh instances so you can run 10 at a
time uh but we're not only going to run
it 10 of the time but we are going to
randomly Shuffle parameters because in
some cases there are some there are some
issues that can be easily found with
let's say three or ten transactions and
some other issues are going to be more
easily found with two 200 transactions
in a in a in a row right so what we do
is we run the tool in different with
different random parameters and in
different let's say Generations so we
run we run akina for an hour 10 times
then we save the Corpus and you can get
you you can see all the all the all the
code that was covered and then we
started again but taking the the the
output of the previous generation so you
iterate over and over again so you can
see how your code is explored right or
if there's some part of the code that is
not explored with 10 different uh
instances you can go back and say no I
need I need to change this because it
doesn't depend on the on the actual
execution so we can we can give you the
link uh for that it's just a python tool
so it's it's it's easy to use um yeah
it's also open source like everything we
are doing is open source
okay so yeah like it's really about
spending time and thinking about our
invariants
and it's not simple like it's the first
invariant that you are writing leads to
a bugs there is something wrong about
your approach uh you should not have
like simple invariants that you know are
going to work the system so we'll start
simple and iterate over them
okay to give you some example let's say
you have a now with magic libraries what
environment can you have
um you can have commutative properties a
plus b is equal to B plus a you can have
identity a one multiplied by two should
be true our inverse if you add something
by its opposite it should be zero this
is not always true right but depending
of what you are building this might be
like the type of property you are
looking for
for token we already talked about the
first one no no user should have a
balance above
total Supply let's say you want to look
at the transfer function and patsync
transfer function what does it do
I'm transferring token to someone so at
the end my balance should have decreased
by the amount and the receiver should
have see uh its balance increased by the
amount and let's say you try to write
something like that
once you might quickly realized that
what happened if the destination is
myself so if I transfer token to myself
my balance is not going to increase or
decrease quite awfully so this is an
example where you might try to Define an
invariance on transfer it might seem
simple you might write like the the
thing in solidity and if you do that
again is going to tell you that there is
an edge case where if you transfer to
yourself like the event is going to be
to be broken
and in this example if you go through
this um
it's not the code which is bad it's an
invariant that was bad so that's why
having this iterative approach uh is
really important because sometimes we
are going to make assumption about your
system and you might actually be wrong
and as the system gain on complexity
it's more and more likely that it's
going to be more difficult to refine the
invariance
something else which is also important
to to consider is
um patterning first uh reverting for
example an environment you can have is
that if you don't have enough phones the
transfer function to the revert or a
return first depending on how you
implemented the token
once you have this list of invariants
usually you can split invariant into two
categories function level invariant
system level invariant function over
invariant are usually stateless
they are things that you can just you
know look at a specific function and try
to see if it holds so it may take you
know environment I mentioned are
stateless and our functional leveling
variants
here you can craft simple scenario just
by calling the specific function
then you have system level in there
system level environments are usually
more complex but they're also more
powerful and here you are stateful you
are going to change the state of the
contract and you are going to try to see
the environment no matter the state and
here is why it's important that echina
is calling all the different function
because it's actually what you want to
try
the balance being below or equal to the
total Supply is an example of a system
level invariant
one thing that you can use
is a different modern incidence of
calling Akinator underscore something we
support a session so you can just create
function put assertion and try to see if
it holds
a SIM for system level environment as we
kind of already like discuss it might be
more complex depending on the
initialization of your system uh if it's
a simple initialization you might be
able to do everything in the Constructor
if the Constructor is too large for like
the bytical size or for whatever reason
you might have to split it and here is
where you can use a kid now 18 outside
okay
all right so let's let's see this uh
particular piece of code let's take
um
uh half a minute to read it
um it's it's basically a buy function
that will uh call an internal function
valid by uh so what we are going to do
is we're going to think uh what are the
type of invariants that we can have here
and what what is what will they are
going to test and what type of
guarantees we're going to get from this
so let's let's take a few few seconds
for this
foreign
yes so we have questions
okay so the question is uh testing
timestamp dependent so it's clearly not
not the case here for timestamp
depending code uh
um a kid now when it runs it
automatically increase either the block
number or the block timestamp inside
some range right because it it happens
that some code will fail uh when the
timestamp is increased into a really
really large number but yeah 100 years
or like the end of the universe so we
don't care if if the smart contract has
a bug that can only be triggered in the
end of the universe will be the least of
our problems
um all right so yeah any any idea what
are the type of things that we can test
here
first one
the first one we can understand that how
much token how many tokens we can get as
a result follows our expectation when
we're sending message value because as
you can see it's a hard-coded rate is
around 10 so basically it's a pretty
simple formula we can change different
values we put into the function we have
totally prediction how much we can get
and then we can try to verify that it
works
yes exactly so the the property is
related with the amount that we can get
even the number of uh weight that is
sent
so
um yeah uh we can so the first thing is
this this code will depend on the state
uh we don't have the mean function so we
don't know what is what is inside where
we have the valid buy function that is
actually abstracting the thing that we
want to that we want to test so we will
start with valid by which is a pure
stateless function
um
yes so we were thinking about invariance
here related with
um the amount that we can get so this is
these are very simple without going into
specific uh this is a very simple
invariant if the amount if the Wayside
in C is zero then the user should
receive no tokens at all right so so
that's it's it's even simple and
thinking how how much well I a user
should receive but it's a Concrete case
and it's it's kind of a corner case so
it's it can be important to test
all right so how we can test this so
there are a couple of way to test it
this is
um this is one so we we can write a
function that will take uh one parameter
so again I will put any any number there
however we're going to restrict the
number uh the input of this function to
be non-zero
uh then we're going to execute valid by
um and
then we want to know if echina can reach
he can reach the
um the statement after that because
valid by Will revert if if the uh if the
inputs are not uh the one expected
um so we want to know if we can get if
we can get tokens despite sending no
um no value right
and
so perhaps you're wondering what if what
if the ceremony is zero uh then clearly
this code will not do anything
interesting so she was just is going to
revert
uh when you're writing tests you need to
so you can put any any amount of
requires or preconditions or people
usually call it however if you put uh if
the preconditions are too restrictive
and your uh your function reverts most
of the time it means like you're not
going to get value from the execution so
every execution reverted in a test in an
invariant let's say that every every
case that you don't uh that you don't
use it's going to be an execution an
execution that you waste so in this case
you only waste one one execution in a
range of in the full range of uh uins
256. so it's not a big deal but if you
have if you put a lot of requires that
only a very small small amount of uh
values well satisfied and it will be
difficult to get randomly or even even
with the with the techniques that we use
you will need a slightly different
approach but yeah we will we will uh
then go later into that so any any
questions
yes
yeah so as you mentioned uh in this case
that we are basically sacrificing only
one uh one case which is when it's zero
uh but is it gonna run over the whole
range of un256 because that's a really
large range and and it doesn't make
sense to test all of that in some cases
yeah exactly so it won't
there will there is no tool in the world
that can run for all the all the range
uh it is always either either uh
symbolic I mean you can do it
symbolically but it's it's not it's not
going to test all the values it's
another thing
um and uh fasting techniques are going
to sample let's say randomly from the
from the input or with hubs right
um it's in the case of Echidna since we
are going to compile this code and it
will run through or static analyzer we
will detect some interesting values
in this case
um 10 for instance 10 10 is an
interesting value there it's a it's a
constant and it's going to be used
somewhere so definitely we want to we
want to test with that constant okay so
let's see what happens if we if you if
you run so this is uh uh so kinda will
run a number of transactions it will
eventually detect that assernal free
token has an assertion failure however
this is going to be in a context of 100
of transactions random transactions that
perhaps will do something that is
completely unrelated but what we'll do
is input minimization input minimization
is a very old technique referred to
testing in which you have a list of
bytes that affects a bug you want to
remove that bytes
um one by one or in some random way in
order to get a
um a list of bytes that will still
trigger the bug but it's going to be
minimal or or either local or a global
minimal depending on the type of tool
that you're that yours so in this case
uh we can uh a kidnap will try to
minimize any any uh parameter here we
have only one parameter and the
parameter is actually is actually going
to be useful triggering about if we have
more parameters they are going to be
minimized towards zero so if you have
units uh then it will be reduced until
zero so zero is the simplest
um uh value this is arbitrary defined on
the uh on the code you can you you can
change it if you want and but in this
case the parameter cannot be zero
because if it's zero the the test will
pass
right
so in this case the minimal amount is is
one it's not guaranteed that you will
always get this smallest uh set list of
transactions to trigger uh this is an uh
an MP complete problem it cannot be
solved on on linear time so it's it's
all going to be always a sample but in
in practice uh even randomly sampling
removing transactions or reducing the
complexity of each uh value will will
give you good answers
all right so a little bit about ekina
apis maybe we can just explain
um yeah just explain why it's happening
[Music]
um
yeah so yeah so the issue here is that
if you send one desire token
what's going to happen is that you do
one divided by 10
and 1 divided by 10 is 0 because you are
winding down and other results uh the
required amount to be sent is zero so if
you ask any number of tokens below 10
you are going to get them for free and
this is again again an example where we
Define an invariant we don't actually
look at the formula we are not looking
at how this formula works we just Define
an invariant that if you don't send ETA
you should receive not okay and by doing
that akina can find you know how it
matching issue and we actually evenly
using Akinator for bonding for you know
mistake in the formula and and so on
yeah
oh yeah yeah I gave that this function
is for testing purposes but um in a real
situation where Cent is not part of the
of the signature of the function right
you read that from the message yeah yeah
yeah this is happy like like deeper into
the code right right so how are you
doing that okay you read that into the a
certain function how you do that so yeah
uh uh if I understand it correctly so
this this could be an internal part and
you can have like a lot of code that put
like gets the value from them from the
message value and then do something else
ah you can do that uh yeah I mean I mean
is this depends on on your code here we
are testing an internal function right
using using some some defined yeah yeah
yeah and if it was using message that
value um yeah exactly
and if you have a constant in your code
saying message value should be uh 42 42
42 it will use that constant eventually
so you should be able to hit that
particular that particular case given
the fact that this is random something
of course but can you uh moving back to
the previous slide to the function
what I'm really wondering because we
talk about this error whoever
tokens less than is uh so way less than
it's so small amount and the same
problem which could be here is Overflow
if I provide a huge amount of ease
because we have a multiplication to
decimals it could be done on the other
side we all of us know that the quantity
of s is limited
you can't even take a flash loan and get
more ease than it produce so what is the
best practice follow this formal
execution when you write fuzzing tests
or take some real examples as
limitations as there is no match as
zeroom as it exists at the moment and we
know it's a deflation so we can simply
assume that in the future nobody could
take so much to get overflow here yeah
yeah exactly so yeah this is is an
interesting question and it goes into
the fact that what are your assumptions
on the test right if you if your
assumptions are like I have this token
with this limited Supply that should
never go over something then you you can
just say I require that that the value
sign cannot be more than the total
supply of something right but in the
case of interest is a bit more tricky
and and in fact in in Echidna what we do
is we have we have externally on
accounts that are simulated we loaded
with eater every at every transaction
because you can have a very large amount
of feature you can take a flat loan uh
you you probably cannot have as enough
eater to overflow uh you into 256
because that will be a real issue for
the AVM uh in in itself but
um we can we can Define in the Kinder
config which is the maximum amount of
value that we send per transaction right
so if you put like I don't care if the
attacker has more than than 10 000 liter
because that will mean that they can do
other things then Echidna will happily
uh take that limit and will never put
something more however it's still the
case that over several number of
transactions the accumulate number of
features can go over that that barrier
so you should you should be careful with
it and there is also no project you can
take here so basically you are building
an invariant and the invariant of which
we thought as like a value
so either you start where the invariant
has really limited Twitter like really
with chain one and you try to see if it
hurts if it's working with like a you
know like with one meter okay it's
already working so you can continue like
this if it's not breaking then you can
increase this with time from time to
time or you can take the opposite
approach if you define an invariant
where the threshold is really large
it's working because it's really large
and then you decrease this result so
that's how you start really limited and
you know depending on the result you
remove the limitation or you start
without limitation and you reduce like
up up to the point where you have a kind
of like a value for which you feel
comfortable with yeah yeah and and that
is also related with
the if we start with very large values
we we could have false positives but and
if we start with very small values we
can have a false negative but which are
the ones that are going to cause you
more trouble that is something to to
think about it because if you miss one's
false positive your your protocol can be
you know destroyed and if you miss one
one false negative then it's okay
all right
hey there in terms of fuzzing mutation
uh do you do any clever things like uh
say this function has a constant of 10
so would you then uh see the constants
in the the function and use that as
input yeah we reuse the constant forms
of function and we will first I want the
constant also like if you see 10 we are
going to use 10 we are going to use 9 11
and you know like uh around
uh yes there are some there are some
techniques I can show you a little bit
after a few lines of the code of
Akinator that shows all limitations we
have mutation interesting mutations on
list of transactions in which we Shuffle
we do uh we do like
splice as well so we take a list a list
of Interest transaction and another one
and we splice it on a random position so
there are a couple of fun things to to
look at but uh yeah I think we should
move on a little bit
um all right so as I was saying we have
this uh failing even if you don't
understand what was what is the failure
um well that is that is a different
there is a different Beast sometimes you
you you have you put your your
um your invariant and your invariant
feels and then you start the journey to
understand why it fits so that's we are
not going to talk about that you uh some
people like to re-u run We Run The
failure into a unit test to make sure
step by step what is what is going on
but yeah that's that's a completely
different uh type of Beast that is
related with what happened after and how
we can fix how we can fixation
all right so a little bit about ekin
apis this is
um a topic that
um
it's uh it's it's still an open debate
in some in some cases so what are the
best way to test to create properties so
Echidna supports a couple different ones
it's about Boolean properties in which a
function uh is executed
um and then it will it should return a
Boolean true or false and if the
function reverts for any reason that is
the same as returning false right so if
we go back a little bit we can see over
there error and recognize op code that
is going that is related with the
assertion failure this that is how
um on version of solidity used to uh
have
um this uh assertion failures but if you
use Boolean you will just say return
false right so you know exactly how how
everybody fail uh or it could be a
revert so you you say over there you see
over there it revert okay so either you
do Boolean properties which are the
classic way to define invariants and
these come from uh uh some some real old
techniques uh in particular quick check
which is which is a property based
testing tool for Haskell and then a
couple of other languages uh which was
an inspiration for for for this then you
have assertion failure so every time you
see uh every time uh the the assertion
is called with false that is uh that
will fail however if in the context of
your function you see a revert that will
not make the function
um the property fail here we can see
that if valid by reverts then the this
Kindle will not report that because we
are using assertion mode
fine so you you should be careful if you
are using if you if you cannot rewards
uh you should have to uh either use the
um the type of
um the Boolean type or what you can do
is if you care about reverts invalid boy
and if it's an external function you can
do a try and catch and you can check
which type of reverse and you can even
fail in some type of reverse and not in
other because you want the user to get a
good message of of alert and perhaps
other type of reverse you don't
you you want to know so
and finally we have the DAP and Foundry
API in which
um you will uh you will have
um a function that if it reverts uh it's
going to it's going to fail and
otherwise it's not and I hope The
Foundry team
agree with us and it's uh is correctly
implemented
um all right so there is testing modes
um in the in the
um in a repository so we can
um you can go there and it's explained a
little bit more this is very high level
overview so yeah
yeah yeah so so so yeah again that's
something returnable Boolean uh it's
easy to Define uh no side effects that's
that that is so interesting when you use
Boolean properties all the side effects
will be reverted uh before the execution
of the actual invariant right but if
you're using assert the side effects so
everything you change in the blockchain
will will remain so this can be really
useful for testing some some complex
code but yeah we're not going to well
um yeah assertion is can be simple to to
um Define
um and it's it's it will also
um it will also be easy to see on the
code coverage if it's not if it's not
covered or or not however some code
especially some old piece of solitary
code it's going to have assertion as
required and that is a really bad thing
you should not be doing it use require
if you want to if you want to actually
um have a precondition in your call and
use assertion for for testing
okay
um yeah and finally we have the The
Foundry and up uh compatibility the only
thing well uh the thing that we don't
support is pranks so we don't like to
prank people so we don't we don't
support pranks however we support some
of the some of the
um uh havm yeah the havm the original
ones uh cheat codes
you should be careful using it uh we uh
we know that there are some uh catch
with that especially related uh with
what the solid compiler expects and what
you're doing in your in your transaction
so please be careful because you could
have some uh
um some some issues so we in we rarely
use cheat codes uh we try to keep all
our code as close at the solidity
possible so you can easily Port it to
another tool there's there's little
Akinator specific uh but yeah we are
also open to discussion if if the
community agrees that we need a specific
cheat code or we need to avoid some
specific chicken then we are open to
discuss it
all right
um so exercise four we're going to deal
with uh
um one of the
um one of the exercise for dumb
vulnerable defy so how many of you know
this uh
um amazing uh CTF
um
ah yeah sorry you you yeah we're going
to keep it up yeah yeah we can yeah we
can skip it this is term so this
exercise was exactly the same as the
first one but instead of using function
uh we were using assertion so it's
exactly the same invariant exactly the
same setup but with a different API just
as an example yeah so we will go into a
more interesting example
um but before that
um there is uh something that you
wouldn't need which is called the
multi-aba mode
um so we usually usually testing tools
take a specific contract as your main
contract to interact so in in the
default mode echina will only target a
specific contract that you can put in on
on your command line or if you have only
one contract you will use the first one
right but there is something called
multi-avi that would call every every
contract that is deployed after the
Constructor that you have Avi right so
if you deploy something in bike in by
code directly and you don't have Avi in
the won't be able to call it because it
doesn't know what is what is there but
if you if you deployed a couple of
tokens and several contracts and you use
multi API Echidna will call any function
in any deploy contract uh after after
the the end of the Constructor so we
will need these in order to deal with
the next example because sometimes the
the the the debug that you want to
detect it doesn't depend on the state of
one contract it depends on the state of
many contracts and in that case you can
you can be surprised by the fact that
changing the state in another contract
can break your your property and
definitely we want to avoid that
Okay so
uh again how many of you know about them
vulnerable defy
okay a good number and did you actually
well this is these are the first
exercise the first the first two uh so I
hope that uh uh people know so if you
know this this how to solve it you
should uh it's going to be even easier
uh for you what we're going to do is
we're going to uh take a look of this
um sample so yeah
I assume that we already you already
have a code
so
um is the
exercise the the naive receiver one
um so what we want to do is
we want to be able to drain
um the the funds in Flash loan receiver
right just to give like a bit of
description of the of the challenge
um here you have two contract you have
the naive
um we see the Orlando pool which
basically yeah yeah it's it's over there
um I can allow you to take a Flash run
for a fee and you have a second contract
which is a user uh contract that is
going to interact with a pool and the
contract is going to be the user
contract is going to be deployed with
some fund inside and the girl is going
to try to see if it's possible for this
specific contract from the user to be
joined
exactly so
uh we we want you to review the the
um the exercise if you have already did
it it requires you to send some some
some some number of transactions so in
this case we are going to prepare
everything for a kidnap to ReDiscover
this without telling it what is what uh
how how it can be uh sold so we will
need two things we will need to
initialize the
um the code to have
um too much what the what the
initialization is it's
um is actually showing us let's see
okay so this is the The Flash loan uh
the part of the or the flash loan so the
the interesting part about this is we
don't have to care about specific
details in the code we want to we want
to
um give a kid now the same scenario that
we have on the on the actual uh
Challenge and we want to know if it can
actually find a way to drain the
contract
so yeah we can uh we can see uh how the
reciprocal function
um works here but um yeah the
interesting part perhaps is the
initialization what we are going to do
is we are going to deploy in the
Constructor of our
um test we're going to deploy the the
contracts that we have here and prepare
everything and then we're going to use a
suitable
um uh invariant which should be really
simple you don't have to overthink and
we want you to uh run a kidnap uh with
that in order to see if it can drain the
contract uh with the of course with a
suitable
um uh with a suitable invariant so yeah
we will take
um 10 minutes I think yeah yeah we are
running out of time but uh let's take 10
minutes so the first step is really like
this is a initialization from the test
case of the contract the first step is
really just to reply like this into a
solidity Constructor and then provide
the environment
yeah so happy to take question questions
or any technical issues
that's a goal actually we are going to
do exactly what he's doing here but in
serenity
there there is an alternative way to do
it but the solidity approach is is
easier to to avoid
um because well the other tool is called
atino that can replay this
in a simulated blockchain like ganache
and then send it to the to the tool so
uh in that case you don't need to
replace on solidity manually but you are
still I still know still need to know
where is everything deployed right so if
you want to interact with the pool you
need to know where is which is the
address of the pool and you can you can
then uh a kidney cannot actually call
the Paul functions uh automatically
because it has everything but in this
case we're going to go into simple route
uh that is going to uh take us to uh
rewrite it's just a couple of and this
kind of much what we're doing here in
order we might look at the existing
unique tests to understand the
initialization and we might translate
them into solidity if needed to assign
credit for the invariants
so yeah the the previous exercises are
on the easy side this is a bit more
difficult but still shouldn't require
more than a few lines
um
so yeah but please let us know if you if
you need some some hints there are some
hints in um
in one of the one of the branches in the
hint Branch but yeah Heather uh hello
yeah sorry no worries
um is there any thought or current
support for mainnet forking or
um State forking of some sort
not yet yes so not yet havm has support
for that but that will that will need us
to put uh that requires to do like input
outputs on on transactions so we need to
check if that will impact on the actual
um on the actual
um performance on the call
um so yeah that will
um
yeah
um I have kind of high level questions
so I'm trying to think about what the
limitations are in terms of
expressing properties as invariance
right so for example let's say we have a
temporal property that we want to
express like we have a wallet contract
and we want to be able to say that any
user who deposits their money is
eventually able to withdraw it is that
just like a fundamental limitation of
Echidna or is there a way to so if you
can
so the notion of eventually it's you you
need to have some definition on the or
on the blockchain right So eventually
cannot mean like in 100 years right so
if you if you find say I will only allow
increment of time up to some limit yes
you can you can call it as a bounded
version of that property but you cannot
you cannot use it as a theoretical thing
like you know I have a state which I
don't know what it is and then I will
transition to another state which I
don't know which uh what it is and in
that case you will need to know if the
original state was actually possible and
and things like that so it kind of works
on on a concrete on on concrete States
so you always have concrete data and you
need to put like boundaries on the
things that you that you can do so if
you say a user should eventually uh
receive this amount and eventually means
like in a number of transactions and a
number of blocks or timestamp then yes
otherwise it's it's more like a
theoretical proof that you're doing and
you probably need another type of tool
yeah I guess I'm curious even if you
took like the bounded case because
that's fair that you're dealing with
like concrete traces here it seems like
that's not or it's not intuitive to me
anyway how you would Express that as
like one of these invariants so you you
will you will do something like this you
will put a function that says uh and and
you will need a
state to track down like uh you you do a
deposit and you will need a user to
eventually receive something right so
you will need to have a state that
tracks deposit like a mapping right and
you have a function that is your
invariant so if
um and then you receive the address of a
user and you check in the mapping uh if
if the time
um between the last deposit is in this
range then you were going to check
something and if if the time in this in
this other range you're going to check
some something else so it will be like
randomly checking in in transactions
um and with that you will be able to
cover
uh given the fact that you're going to
generate enough transactions and enough
time times right so it seems like the
answer is it's capable of doing it but
it requires some like kind of manual
adjustment of the code almost to add
state of it so yeah you will you so if
the if the property that you are testing
requires to add State yes you will need
to add whatever state is needed it won't
be able to track state outside
right the only thing that will be
tracked outside is the increment between
between the uh different blocks
for instance so that that will be
tracked uh outside a new Aquino will
show you from in between this
transactions and this transaction I have
10 blocks that will be tracked uh
outside but everything else if you need
to do a mapping between users and and
the time between
certain operation you will need to keep
that in a different in installation in a
different bio I see great thank you
all right so we have
some other questions
hi
um is there any feature that allow me to
guide the future or the domain of values
that I want to try
um so in order to in order to guide the
the faster into a particular State the
easiest way to do it is to add
um is is to add a small piece of code
that will be auxiliary code in order to
uh move the state from your contract
into something else like for instance if
you have if you have a contract uh the
protocol that requires a deposit with a
particular uh property let's say that uh
you have three parameters and you need a
deposit that has uh that has digital
parameter in in in the Sim in the same
number or in numbers in which in which
are difficult to find you can have this
piece of code
but it's important to let the kidnap to
explore freely at the same time that you
are allowing information so it's it's
actually important to know that as an
auditor or as a developer you are adding
information into into not just using it
as a black box right so every state
transition that is non-trivial to find
or is really really important you you
can have it and make sure that it can
eventually execute it because it's going
to be another another transaction to to
execute but at the same time you want to
allow the tool to explore things that
you don't expect because if you just
restrict says I only expect users to do
these type of deposits then you can you
can be surprised later because there
there is a way to break your your
property using things that you don't
expect
okay thanks
and it comes down to the previous
question where either you start with a
lot of requirements and a lot of you
know restriction in what you are trying
to explore and if it odds you are going
to remove some of the restriction or you
start this opposing Direction you don't
have any restriction and you know you go
more and more restricted
foreign
yeah
thank you
okay
so did anyone manage to at least uh
Still Still start to create the
Constructor or even run it uh to have
some
some invariant
or even think about the invariant that
you need
thank you
so in a couple of minutes we'll go over
the conclusions and I will show the the
solution
um
but yeah happy to take any additional
questions
thank you
just from an implementation uh side I'm
curious what
um what actual like virtual machine do
you use to deploy and execute contracts
so we we use havm uh which is the
Virtual Machine written in Haskell I
know that it's in the process of uh
improving and rewriting so it was moved
from the adaptable into the ethereum
repository so we are eager to test new
features
but yeah um if you use the Tino
companion tool to deploy your contract
it's going to use ganache
um and you will serialize into a Json
file and you can then load it into into
that
[Music]
okay
[Music]
uh solution okay yeah we're going to
quickly go over the solution uh so we
can have a couple of minutes for for
this so the solution requires first to
uh deploy have a contract with enough
amount of heater uh to to match what is
deployed
um and then
um you can see here uh in we we deployed
all the contracts that we need and send
um the amount of eater that every
contract needs and then what is uh what
we're going to use we're going to use a
simple very simple property that is
going to say that the balance of the
receiver is at least 10 liter so we
don't actually need to follow exactly
what the exercise says about draining
completely the contract if we have one
transaction that allows you to reduce
the balance of the receiver then then
it's then something is wrong and uh
definitely uh it will it will eventually
be drained so
yeah so quickly if you run it you will
see something like this
um in which well the uh deflection has a
has a parameter that is the the borrower
and we can control this to in order to
um reduce the amount of balance
all right uh so yeah you want to go into
the conclusion okay
um yeah we're the second exercise on
them ruinable D5 but uh we are running
out of time
this idea was the same we are defining
an initialization
which was a bit more complex and if you
go through this exercise with something
a bit more specific is that there is a
callback from the contract to the caller
so on the Kindle test you need to have
like also the Callback to implement the
flashlight
but yeah
[Music]
so this is something we kind of touch on
a bit during your discussion what about
the other tools so there are a couple of
other further out there there is Dub
Brony Foundry at least this one are open
source
this funnel might be a bit uh better for
simple tests and for like you know ease
of useful uh like the first invariant
because they are integrated within the
compilation framework but in the long
run they might not be as powerful as a
Kinder simply because we have you know
user Kinder for a couple of years and we
have tuned it you know where that it
provides the best value that we can do
I'll get finished okay sorry um yeah
okay so I hope you enjoyed the workshop
um we have more exercise in building
secure contract
something that I would recommend for you
is to try to write invariant you know in
your next project and actually who is
going to try again now on his next
project
nice
and thank you
[Applause]
So today we're going to talk about
storage proofs I want to introduce this
app
yes
I'm gonna present you storage proofs and
explain why they're cool how to work
with them why you need to link to work
with them
and yeah a bunch of other things why is
it even possible all the complexities
behind the trade-offs and so on so a few
words about storage Crews why I really
believe that they are cool especially uh
nowadays so might as this is that
ethereum is pretty sharded nowadays and
with storage truth we can essentially
read the state in a almost synchronous
manner which is a pretty pretty nice
thing to do
given the circumstances
um yeah and maybe also let me explain
why is it even possible so story is
essentially this idea that the entire
state is committed in a cryptographic
manner
um using some data structure like
Miracle trees Marco Patricia trees and
so on
um and yeah we can essentially verify
any specific piece of State at any point
in time on any domain which is pretty
nice and does introduce additional trust
assumptions you just rely on the
security of like the base chain
um so yeah that's like storage proofs
tldr where they're cool
now a bit of like sponsored section of
sponsored sections so uh what we're
doing at harvardus so our like goal is
to make smart contracts sell for in a
way by providing access to historical
state
uh we like I said might as this is that
ethereum is pretty short that nowadays
we want to unchart it by using storage
proofs and we want to enable synchronous
data reads because today we do not have
really nice ways to make synchronous
data access without introducing New
State uh new trust assumptions so yeah
that's we do and how we achieve that we
achieve that by using obviously storage
proofs we use snark Starks and NPC I
will get why we even use all this
tooling but first a few words about
storage rules what these are and and so
on
it's so tricky actually I I need to be
multitasking okay so uh what we're gonna
cover in today's Workshop so all the
basics required to like understand
properly this primitive how to like work
with it uh how you can generate these
proofs why they're pretty useful and how
actually you can access this commitments
I'll get later what we call the
commitment in a process manner
and how we make smart contracts software
and enable historical data reads
cool so
um
it's pretty that's pretty tricky
so about the background that I want you
to have for this Workshop so we're gonna
like start from the biggest Basics so
what is the hashing function just a very
quick reminder I hope it will take less
than a minute uh like generalized
blockchain Anatomy how I ethereum header
looks like why ethereum they're not like
pretty on only like ethereum focused uh
however I think that for the sake of
this Workshop it's the best to like
present on this concrete example Miracle
trees explain me like on five I will
just quickly explain the idea how it
works and what is America Patricia tree
without really going too much into
digitals
um yeah finally no not finally uh the
anatomy the ethereum state
it's pretty important to like deal with
this uh with this primitive and finally
how to deal with the storage layout
cool so touching function essential is
this idea
essentially it's this idea that I can
have a function that takes some input
of any size and it always always return
an output of a fixed size and now what's
also important there is no input there
are no two inputs that will generate the
same output and you cannot reverse the
hashing function so it means that given
the output you don't know what is the
input and this is not what we call like
Collision resistance pretty useful
primitive like used in blockchains uh I
will and I think that's that's pretty
much what I assume that everyone is like
familiar with like yeah okay why is it
important
um so generalized blockchain
Anatomy so why we call it a chain
because we have a bunch of blocks mined
together like linked together because
each block contains the reference the
parent hash and the previous header
contains the reference of the parent
hash which is pretty cool and let me
remind what the hash the parent hash or
the block hash of uh on ethereum is it's
essentially the hash of the header uh
pretty important to deal with this
Primitives and make smart contracts
software so accessing six Oracle state
do you just keep that in mind
let's get to the next part so
um no
ah I think I'm missing one slide
no it's the correct one okay so uh this
is an ethereum block header uh as I said
we're gonna go through the example of
ethereum concretely so a bit of anatomy
so to access State obviously we need the
state route what is the state route is
the root of the miracle Patricia tree of
the ethereum state
we also have the transactions rule which
is pretty useful if you want to access
historical transactions like their
entire body and receive truth so it's
really useful to access any events logs
and and so on and all of these are like
root of the American Patricia tree
America Patricia 3's America 3 just
think of it in that way and most
importantly we have the parent hash and
with the parent hash we can in a way go
go backwards I think that's it let's get
to Miracle tree so essentially it's this
idea that I can take whatever amount of
data and I can commit it in a
cryptographic manner by using this data
structure so on the
left side we see a standard Merkle tree
so essentially all the data goes to the
bottom and we essentially hash it you
know what the hashing function is then
we combine these two hashes together
with hashtag we keep doing that until we
get to essentially one hush and this is
what we call the root mark up to three
shot three modified Miracle Patricia 2
to be exactly the data structure that we
use in ethereum
um what you see here I hope you see on
the top we have the state route
and essentially the state route is the
root of this tree and now how it works
and how you should think of this of this
it's a pretty complex data structure I
don't want you to bother with it today
but essentially we have three types of
like notes we have Leaf nodes extension
notes and Branch notes so Leaf nodes
contain data Branch nodes contain data
and extension nodes like on the high
level just help us to like sort of
navigate in that tree but to be honest
to deal with storage truth you don't
really need to understand this part but
to like build on the low level as we do
obviously we need to we need to do
pretty pretty a lot with that with that
part
okay
so ethereum State how is it constructed
most important takeaway it's a two level
structure so I mentioned that the state
route is the commitment of the entire
state but it's not really true because
ethereum is a
does it still okay it works it's uh it's
account based
um and essentially the state route is
the commitment of all the accounts that
exist on ethereum and what an account is
made of it's made of a balance
like the if balance it's announced
transaction counter storage route the
storage route is like the root of
another America Patricia tree and this
America Patricia 3 contains the key
value database that holds like
the mapping from storage key to its
actual value
and finally we have the code it's
essentially the hash of the of the
bytecode
so main takeaway first we access
accounts and once we have the account
storage root we can access is it's it's
the
okay
um
cool so to sum it up like the background
so main takeaways given the block stay
true to you can recreate any
any state for this specific block on
this network
and given an initial trusted blockage
you can essentially recreate all the
previous headers which is pretty pretty
cool and important to get the ideas that
I will explain like pretty soon
okay so as it's gonna be a workshop it's
a short one so I won't let you code but
I will show you some concrete examples
so what I want you to like go through
with me today is how we can prove the
ownership of Alliance profile on another
chain
so
a bit of background lens profiles are
represented as nfts and lens is deployed
on polygon I think that's it how do we
get to this so first of all the question
that we need to answer to ourselves is
how does Polygon commit to ethereum L1
because if we want to like let's say
prove the ownership of a lens profile on
optimism we need to know the state route
of polygon but there is material one in
the middle so how do we actually access
this on each terminal one primarily so
uh polygon is a commitment commit commit
chain
and it commits to to ethereum a bunch of
things every
some amount of time and essentially on
L1 we do not validate the entire State
transition but we just verify the
consensus of polygon and this
checkpoints how they call it essentially
contain uh State routes and so I mean
not directly but we can access them and
let's get to this to this part
so this is taken from polygons
documentation and this is how a
checkpoint looks like so as you can see
the checkpoint is made of a proposal so
who proposed The Block
start lock and block give me a second
I'll get to this and most importantly we
have the root question so the root hush
is essentially a Merkle tree not America
Patricia tree that contains all the
headers and which headers the headers in
the range of start block and end block
cool
so now
if we get back to the previous part we
can essentially prove with this
commitment that we know the valid state
route of polygon
first even block
okay A bit of Hands-On so we want to
prove that I own a lens profile on
polygon forever
so
number one we go to the contracts we see
a contract
we go for it and we see that essentially
there is a bunch of logic on top of this
erc721
this is like the basic erc71 as you can
see it's an abstract contract and it's
slightly modified
instead of having like a standard
mapping from like token ID to its owner
we have like token ID to token data
token data is a struct distract is 32
bytes in total 20 bytes is the actual
owner and the remaining 12 bytes
represent one the token was minted
okay but how do I actually prove it oh
and also very important thing when
dealing with storage layout we have
something that is called like slot
indices so each variable has a given
slot like in the some sort of meta
layout I call it like that it's from the
right way anyways
this mapping it has like the slot index
too I will get to this part in a second
why it's two and we have a mapping from
token ID so you win to 32 bytes of data
represented as a structure just think of
it as some bytes
okay
so uh I guess most of you use heart hot
so I'm gonna present on on hard Hut
there is a very very cool tool to deal
with storage layouts it's called
obviously hard hot storage layout this
is how you install it it's literally
yarn install hardcode storage layout you
add one comment to your heart config you
write a new script that contains
literally eight lines of code you run
the script and you get this weird table
and what does it what does it really
tell you and oh and by the way why this
tool is pretty useful as you see this
contract is abstract so some other
contracts
then does it still
yeah some countries can inherit from it
and obviously why we inherit the storage
layout I mean this does this in
synthesis can can get more trickier
because it also
okay so that's
it's pretty hard to coordinate like one
hand with another hand even though I'm
Italian okay anyways
um yeah we know this slot in the in the
index and that's how we get it we have a
column that is called
storage slot and as you see underscore
token data is marked as two and that's
it okay but what do we do with it how do
we get this storage key
and yeah that's that's it let me check
the time okay
um so
a bit of Hands-On how do we get the
actual searches it sounds scary and it's
meant to be scary so
we know the slot index the storage index
I want to prove that it's like 0x35
owns with ID 3594
how do we get the storage key
we essentially do this operation so we
concatenate the slot I mean the key in
the mapping which is 35.94 because this
is the token ID as you know we have a
mapping from token ID to token data
token data contains the old okay so we
concatenate this with the storage index
we hash it all together this is the
storage key that we have if you're
interested how to deal with it for like
more complex mappings and like
layouts
back the solidity documentation it's
explained pretty well so
now that's to make sure we got the
proper storage key let's just check it
how we can check it super easy let's
just make a one liter PC call
to get this storage at some specific key
please
if get storage at so the parameters we
want to access the storage of what of
the lens Hub lens cap is a contract that
essentially is the representation of
these profiles and its address is 0xdd4
and so on and this
oh is it better oh it's much better and
this is the the storage key is 0x1 so
essentially that's the hash the 2E got
and the result is 0x000.
and we know that it's 32 bytes of data
where we have 20 and 12. so let's split
it into 12 and 20 bytes and what we have
is
some number like you can see Zero x a
lot of zeros then 62 till D and this
looks like a small number so apparently
it is a timestamp and the second part is
like 35
7 and it's literally our address so we
got it correct we have the proper
storage key cool
foreign
but how do we actually get to storage
proofs so blurb standardized method in
like the Json or PC standard for
ethereum clients and this method is
called eth get proof which essentially
given the contract address so I'm better
call it account address in this specific
case allows us to generate a state proof
and the last argument I mean the sorry
the second argument is an array that
contains all this Storage storage keys
that we want to prove uh there is
another argument which is
0x1a it's essentially the block number
for which we prove the state
um yeah let's call this method oh by the
way uh you might have a question how do
we deal with this method on non-evm
chains because for example on some
specific Roll-Ups this method is like
not supported actually it's not a big
deal because if you think of it we just
need the database and on top of this
database we can literally build this
method we just need to know how the
storage is constructed
okay this is the proof it looks scary it
is scary this entire object is four
kilobytes of data and now I mentioned
before that the state is like a two
level structure first we have a proof
for the account itself and then we have
the proof for the storage I mean for the
actual storage slot it is scary it's
meant to be scary one proof is like more
or less 600 bytes 700 bytes it really
depends like bigger the storage is than
bigger the proof is and also more
accounts we have than bigger the account
proof is
so that's a lot of cool data if um if
you can imagine you can imagine uh and
yeah that's that's pretty bad why
because we need to pause this proof on
the Chain so it's a lot of cool data but
okay let's let's try
what's going to be the cost on like an
evm chain that's the cost it's like 600k
of gas that's a lot that kills almost
every single application that you want
to build on top of this nice primitive
so it's pretty bad and why is it that
bad so I explained on the high level
what Merkel trees are America Patricia
trees are on ethereum we use Marco
Patricia trees and essentially there is
a trade-off that when using Miracle
Patricia trees the proof is a slightly
bigger it's like harder to decode it
because actually we need to do some a
bit of decoding there
um but we need to do less hashing so
this is a trade-off but depending where
we actually verify this proof it might
be more feasible to verify like prove
that is based on record Patricia trees
or Miracle trees
okay but there is a solution
and the solution is what if we snarkify
such such a proof and we verify this
proof inside the Stark why is it cool
because we can like let's say that I'm
gonna verify this proof inside the craft
craft 16 circuit
um and yeah the verification costs more
or less like 210k gas the proof is like
way less than 600 bytes so it's good so
essentially get rid of the cold data
because the proof itself can be the
private input to the Circuit
um yeah we can like use multiple proving
system depending on the on the actual
use case and now why is it like very
very cool so first of all it removes
call data
second model it allows us to deal with
very UNH unfriendly hashing functions or
the evm is the ones that we don't have
pre-compiled for like let's say Peterson
um so it might be like super expensive
to verify such a proof on the evm
because first of all that's a lot of
cool data and the hashing function is
pretty like unfriendly but what if we
can like do it inside the snark and just
verify snark and yeah so another
benefits this really really helps in
obstructing the way how we verify this
proofs because you don't need to have
like one generalized verifier for each
type of of proof
but you can essentially obstruct it
behind behind the behind the snark which
is which is great uh these numbers were
taken from a very nice article written
by a16z like a bunch of uh a few a few
months ago
um yeah and I think that's pretty much
it let's get to the next slide so
synchronous cross layer State access so
how can actually a control deployed on
some layer access the state of another
L2 or L1
so I mentioned that we always need the
state route but because all of these
systems have a native messaging system
we can send the small commitments like
for example the blockage to like L1
usually it goes off-road one and and
yeah we can like enroll it or send the
state through directly and also we don't
need to rely on messaging but we can for
example uh rely on the fact that polygon
is like a commit chain and all these
Roll-Ups like commit from time to time
they're like batches and and so on so
this is like pretty important and we
sort of can get the commitment from
which we'll recreate the state directly
on on another one and then send it to
another
um so if
let's say polygon commits another one I
can send this commitment then to start
and I'm starting to do their actual
verification
cool so now how do we actually do that
so let's break the entire flow into like
smallest pieces
so the flow is the following we need to
have access to the commitment which is
either a block hush or a state route
and again we can get it or I either by
sending a message relying on the fact
that
is this chain commit so in a sense it's
still a message we can relate in an
optimistic manner or we can go even more
crazy and verify the entire consensus
okay so this is Step number one we need
to get the commitment step number two we
need to somehow access the state route
so the commitments of the state from
like a previous block or the actual blog
because keep in mind that these
commitments are only block hashes and
with block hashes we can recreate
headers but we cannot access the state
okay so once we have the state route we
obviously need to verify this state
storage groups okay and there are
multiple pictures to do that all of them
come with some trade-offs and let's go
through all these approaches
so approach number one messaging
so I can send the message from let's say
optimism to
Eternal one I can get the optical I can
get the blockers by just calling the
proper op code and and I get it take
some time but still I get it this is
approach number one so we rely on the
built-in messaging system which is I
think Fair because the security of it is
equal to the security of the roll up and
if you're deploying an application of
the scroll up it's a fair assumption to
do so
um yeah it doesn't oh they don't know
about the downsides so the message must
be delivered so it introduces a
significant delay especially when
dealing with the withdrawal period in
the in in the middle uh and it requires
we it requires interacting with multiple
layers so first you need to send a
message and then actually you need to
consume it
so it's
it's not ideal
but the trust assumptions are pretty
occasional
another approach consensus validation
by the way this like Gremlin is supposed
to verify a bunch of BLS signatures I I
hope it's self-explanatory uh okay so
maybe a few a bit of an intro
um right now we have POS as the native
like consensus algorithm on ethereum
which is pretty great because verifying
the consensus is finally doable because
before like verifying the hashing
function eth hash which was used for
proof of work was very memory intense so
not possible to do inside the snark
um on chain directly so it was almost
impossible to do so
um so now we also have this Workshop
called lmd ghost which is implementable
but doing all of this like directly is
pretty expensive so we need to ideally
wrap inside the snark but there is
another downside so a few words about
the trust assumptions
you well you verify the consensus
directly so it's it's fine
he do you introduce any trust
assumptions not really but the biggest
downside that generating the proof
actually takes some time so to be honest
this approach is feasible but comparing
to messaging like quite often is like
almost the same and you pay a lot of
improving time
and requires like having more advanced
infrastructure okay last approach that
we actually use is something that we
call like an optimistic relator based on
NPC MPC stands for multi-party
computation maybe before I explain how
it works let me explain the the image I
hope it's self-explanatory so it's an
NPC protocol we have multiple parties
it's multiple parties attached something
then we have an observer that can
challenge it and then we have finally
the commitment given to a specific chain
in this case start net once everything
is fine
how does it work so we have a set of
trusted three layers validators however
and they attested a specific commitment
is valid so how does it work if we want
to get the commitment acreated block
hash of block number
X on startnet then instead of sending a
message that will be delayed with a like
slightly delayed we can essentially make
an offshing call just get the latest one
and essentially relay this message
directly to start net but it comes with
a few downsides because while we
introduce some trust assumptions uh but
still it's okay okay how does it work so
it works in a way that we have a bunch
of off chain actors who essentially make
this calls and it works more or less
like a multi-seek but the reason why we
have NPC is because more validators you
have than obviously
more Securities but
more validators you have in it like
standard multi-sig approach you have
more signatures so
more in a way decentralized it is then
it's more expensive to verify because
you need to verify multiple signatures
and you need to like pause the
signatures it's a lot of cool data such
approach is not feasible on chains
Oracle data is expensive so at one
optimistic rollups and yeah
okay so how does it work uh what is uh
actually NPC part doing the MPC part is
very simple it's essentially signing
over like a specific curve some specific
payload and the payload is the
commitment itself and that's it okay so
this is how we actually attest but now
how why this approach is called
optimistic and why it's still secure
so first of all we just posted some
something on the actual L2 and as you
may know we can send messages from L1 to
L2 and such a message can contain like
the proper commitment so essentially
even if the validator set will lie L1
will never lie so you can just challenge
such a message and now to participate in
verifying this validators it's super
easy because literally two RP sequels
one call is gonna check the actual
commitment on the actual chain and the
other one checks like what is the
claimed Commitment if you disagree
you just send a message it costs roughly
60 K of gas
and that's it everyone can do that
um
and again the fraud proving window is
pretty short because it's essentially
how long it will take to generate like
the proof of consensus if it's possible
or how long does it take to deliver the
message and what is pretty cool in this
approach it's not gas intensive we
verify just one signature so that's
about this approach
let's make a recap and let's identify
the trade-offs
so we have three approaches the first
one is messaging the second one is
validating the consensus and the third
one is having this optimistic layer so I
categorize it in four categories the
first one is latency the second one is
the gas cost the third one is trust and
the last one is what is the off-ching
computation overhead why do I even list
it because if we do some sort of proving
then obviously it takes time because we
need to generate the proof
so messaging in terms of latency we are
quite sad because well the message needs
to get delivered so once the message
gets delivered to some specific L2 L1
will be able to generate already new
block so we don't have like access to
the newest values
in terms of gas cost it's not bad but
it's not perfect because we need to
interact with two chains at the same
time so first we need to send a message
and consume it
in terms of trust we are pretty happy
because we trust the roll up itself and
it's a fair assumption
option computation overhead we're very
happy because there is no computation to
do off-chain verifying the consensus so
in terms of latency we are side because
we need to generate the proof
that we've done it it takes a bit of
time in terms of gas cost we are I would
say sad because we need to verify the
actual ZK proof which is way more
expensive than just
consuming a message or verifying a
signature in terms of trust we are happy
because we verify the consensus itself
and computation overhead it's
significant right because we need to
generate the proof
Final Approach
this optimistic layer so in terms of
latency we're happy because we simply
make a claim and we post it on the other
chain that's it gas cost we're very
happy because the
well we just verify a signature
in terms of trust well we are not that
happy but also not that sad at the same
time because it still can be challenged
in an optimistic manner using a fraud
proof
computation option computation overhead
are pretty happy because we participate
like an MPC protocol so essentially the
overhead comes mostly from communication
not computation itself
cool so this is part number one these
are the three approaches obviously I'm
not gonna say which one is the best
because all of them come with some
trade-offs
um okay accessing the headers I hope
it's self-explanatory because we
literally unroll something from The
Trusted input
and The Trusted input is again a block
hush for a specific block X and if you
follow the initial slides that's
essentially each block we given a
blockage you can recreate the block
header and knowing the block header we
can
access the parent question by knowing
the parent hash you can recreate the
previous block header to essentially go
to the Genesis block so given this very
small input we can essentially unroll
the state or whatever was present on the
chain from this block till the Journey's
block
okay so as I said I'm gonna explain
everything on on the example of ethereum
and today all the block headers together
are like roughly seven gigabytes of data
so it's quite a lot but okay this is how
we actually do that this is the high
level concept and what are the
approaches
so the first one we call it like
on-train accumulation so essentially we
do this procedure this computation
directly on the Chain so we provide all
these properly encoded block headers
inside the call data
and the blockers that we might receive
as like The Trusted input by sending a
message relaying it in optimistic manner
or validating the consensus
and yeah like recursively go through all
these headers and and verify them but
there are many many downsides because
first of all it's very cool data
intensive it's very computational
intensive and now we can store all these
headers on the actual chain but you know
even storing
on an L2 storing 7 gigabytes of data is
still a significant cost because the
state on an L2 is reflected as call data
on L1 so it's still expensive either way
but the cool thing is that I have direct
access to like State router or anything
that I want to access
next approach is unchain compression
so we can still use the same approaches
previously so literally unroll it and
process this seven gigabytes of data but
instead of like storing then we can just
update the miracle tree it's a nice
approach but comes again with a few dump
sites it's very computationally intense
because if we have like millions of
headers we need to perform millions of
hashes on the Chain that's that's
expensive but at least we we save on on
storing data and also we need to update
the miracle tree which is which is
another cost
um
last downside is that we need to index
all the headers that have been processed
why we need to index them because if I
want to
up the access a specific block header I
need to provide a miracle tab because as
we update the miracle 3 and we just
store the root in the contract itself
then I need to know the path right so I
need to index the data and essentially
once I it's the moment that I want to
access it I need to provide the miracle
path
this approach is okay it's
I wouldn't say way better than the
previous one but it's way cheaper
last approach
so there is a very cool primitive called
Merkel mountain ranges
love it and the idea is let's do the
same
that we do previously inside this Arc so
we can provide this tremendous amount of
data as a private input to the circuit
and essentially do the same computation
like unrolling inside this record itself
and now we have a public input which is
the blockage so essentially the
commitment from which we unroll it
so the trusted input the public input
can be literally asserted when we do the
on-train verification
and why we unroll it we can accumulate
inside the miracle tree or American
mountain range why American mountain
range is is cool because well let's
imagine that you want to have like seven
gigabytes of data processing one star
like the proving time is going to be
horrible and why would you even like
prove this commitment for like the
entire history like do you really need
that probably not so let's chunk it like
into smaller pieces and Miracle mountain
ranges are pretty cool primitive that
allow to do this to do to do this
to give you like a bit of intuition how
how does it work it's essential think of
it as a tree of trees
um yeah so once we do all this proving
like of chain we simply verify the proof
on chain as you know like refine the
proof is is way cheaper than doing this
directly on the chain
and still we just provide a miracle path
and that's it we essentially have access
to any sort of data we want
let's do a recap again so approach
number one on the accumulation on chain
compression of chain compression three
categories prover overhead gas cost
storage cost
actually gas costs should be
computational cost
okay so prover overhead on-chain
accumulation do we prove anything well
not really so we are happy answering
compression well
we still like need to update the miracle
tree I think actually there is uh there
is an issue here so I'll just skip this
part after in compression you're very
very sad because well we need to prove
actually significant computation so the
proving time is significant okay now in
terms of gas cause the third approach is
horrible because it just costs a lot
because we do the entire computation
engine compression well we're a bit
happy because we just do a bit of
computation but still it's a lot of cool
data a lot of computation but at least
not so much storage storage cost uh oh
sorry gas cost in the second approach
while we just verify approved so it's
cool
um okay storage cost for the first
approach well seven gigabytes of data it
is horrible so we are very set
on chain compression
uh sorry storage cost for launching
compression we just
the root of the miracle tree so we are
happy and in the second case we're even
more happy because we again we just
essentially keep updating a tree and we
don't even need to post a lot post a lot
of cool data because the cool data we
passed is literally just the proof so
we're very very happy but again I don't
want to say that all of the one of these
approaches is the best one because as
you see there are trade-offs
and
yeah so this part is actually pretty
easy so as you know as you may notice
here I was explaining like the second
step when it comes to two linguist
storage proofs and now there is the the
last part which is essentially verifying
the proof itself so approach number one
is verifying the proof directly on the
Chain approach number two let's verify
the proving side the star can then
verify the Stark approach number three
let's verify multiple proofs inside the
snark and then verify the snark we can
aggregate multiple sharks together and
so on but obviously there are some
trade-offs especially when it comes to
proving time
um and yeah so now why the first
approach is feasible on on ZK rollups
for example on structural data is very
cheap and what we want to avoid in this
specific processes called Data so this
approach is for example feasible on
starknet but for example if you want to
verify like a proof on optimism or a
collate is very expensive you want to
reduce it as much as possible so for
that reason you might want to use a
snark and finally if you have like many
slots that you want to prove why can't
you just verify them inside one snark
you're gonna pay improver time but you
just present one proof at the end so
this approach is cheaper is the cheapest
one but only if you have multiple
actions to to take so
there are trade-offs
so let's identify them
categories approver overhead latency
verification cost so verifying the proof
directly prover overhead doesn't exist
latency doesn't exist because we don't
need to prove anything verification
costs well it is significant
because we need to post School data and
we need and we need to do the actual
computation so like going through the
entire path and each step in the path is
one hashing function oh and also
let me get back to the previous slide I
forgot this is very important why
wrapping inside this wrapping inside
this Arc is pretty important if you're
like dealing with a storage layout that
is using a specific hashing function
let's say for example Peterson Peterson
is not available like on on the evm like
you just need to implement it's not the
pre-composed it's gonna be costly but if
you do inside the snork and Peterson is
pretty smart friendly it's not friendly
then well it just verifies in our
control one and you abstract it so it's
going to be way way way cheaper but
again there are trade-offs let me get
back to this so I went for this the
normal competition 3 star Cricket fight
proof through the overhead it exists so
we are not super happy latency you're
also not happy because we actually need
to spend time on improving this this
thing verification costs we are happy
because well we we just verify your
proof so it's fine and it's an artifying
multiple proofs the prover overhead is
still there latency is still there it's
even bigger because it takes a bit
longer in improving time and
verification because we are super happy
because essentially we can mutualize the
cost of verifying multiple proofs
by just verifying one single Stark proof
okay went through quite a lot of things
let's put this all together
so let's imagine we have three chains
and we want to have interoperability
interoperability between them so we have
chain Z chain X and chain y
so it all starts with a message AKA
commitment we send a message in order to
get the commitment so let's say that we
send a message from chain Z to chain X
because on chain X we want to access the
the state of changing so what do we do
once we have the commitment we literally
recreate all the headers
using one of the three approaches
and once we recreate it the header is
still the point for which I want to
prove the storage I just verify a proof
and again for verifying get proof there
are multiple approaches but now let's
say that on chain y I want to access the
state of change Z and there is no direct
communication between chain Y and chain
Z so it must be routed through trainx by
the way I'm
like talking about this in a pretty
abstract Way by Chain X I just mini room
later one
um yeah so from chain X I'm just gonna
send again the commitment about change
the as a message and then simply
recreate all these all these headers as
you may not notice it's pretty redundant
because we perform the same computation
on two different chains and we don't
need to do that especially if you use
like the third approach which is
generating the proof on chain but now
there is another problem how do you
actually know what you should do like
you need to be somehow aware of what is
happening and for that reason we
introduce an API we don't expect like
developers to deal with all that
complexities choosing the right approach
for the direct thing essentially right
now our apis optimizes cost wise soon
we'll be able to optimize latency wise
um and yeah and essentially
that's it
um just about our API I highly highly
encourage you to check this out
um and yeah like a few final words about
the API it acts as a coordinator it
optimize the costs it optimizes the cost
because we can batch multiple things and
once the job is done we get a
notification like via webhook VIA an
event like whatever you want so
essentially you're not you don't need to
be like a infrastructure maintainer and
you can just focus on essentially
building on top of this primitive
and I think that's it
um questions
so the API essentially is a rest API for
now we also have a Json interface we
have option function entry points so we
can request the data like by making
enough jingle like calling a rest API or
like calling a Json or PC method or if
you're a smart contracts like wants to
access this data then you just submit an
event we're gonna catch the event and
later on like after a bit of time fit
this uh the specific data inside the
smart contract so we have like a bunch
of interfaces and by the way speaking of
like the off-train entry points once the
entire leg work is done on our site you
can get a notification it can be like a
web hook we can like send you a bit of
information like using a websocket uh it
can be essentially whatever whatever you
want
foreign
oh yeah so uh that's actually a great
question so different chains use a
different like storage uh I would say
architecture they might commit to
America Patricia 3 Miracle 3 uh maybe
even vertical tree and obviously like I
said having a generalized verifier it's
like pretty it's not a clean approach so
we essentially abstract it but by using
a snark and inside the snark itself we
just do the proper work like
you know you go for the for the tree
like for the for the um through the
elements of the proof and then we can
like use a specific hashing function so
for example now Poseidon is Poseidon is
uh is is pretty popular
um I think that scroll uses Poseidon and
also SDK sync uses Poseidon on the avian
like performing Poseidon will be pretty
expensive so for that reason you cannot
verify the proof directly but what you
can do you can do the entire
verification inside the snark and then
on the one you don't really care about
the Strunk is like doing you just just
verify it so that's how we actually did
it deal with it if we need to have it
abstracted we have it abstracted if we
don't then we just don't
foreign
oh yeah
oh yeah that's uh that's actually a good
question because I think I went super
technical uh so actually what we do at
Herodotus every two weeks we have some
internal hackathons and right before the
merge uh we built a proof of concept
that we called merge Swap and
essentially we allowed anyone to dump
their proof of work if on proof of stake
and the way how it works would you
literally build the bridge on top of
this technology and the bridge Works in
a way that you can lock your if proof of
work inside a smart contract on if proof
of under if proof of work chain you can
prove that you've done it on ethereum
proof of stake you can once you the
proof is verified you can meet the erc20
token and you can do whatever you want
with this token and then if you want to
withdraw back to if you're in proof of
work you just burn it you prove the fact
that you burned on the other side and
and yeah that's it also in terms of
other use cases I think that
cross-chain collateralization is pretty
cool because this is the place where you
want to avoid latency as much as
possible and you want to be asynchronous
as much as possible and essentially
that's that's what we do here because
our latency comes only from from the
proving time but again using some
optimistic approaches and so on there a
lot of things we can do
cure I hope it answers the question
okay I think that's it I have like three
minutes so I guess we can wrap it up and
yeah thanks