foreign
[Music]
and I work as a former very very formal
verification engineer for one-time
verification and today I want to talk to
you about rounding errors and what we
can do about them
so very roughly speaking and I'm really
oversimplifying uh there are two things
that can go wrong when we do approximate
arithmetic in contrast to exact
arithmetic the first one is our the
rounding error that we do is just
too big too far away from the exact
result and that is a problem in itself
but that is not the topic of today so I
want to talk about uh the second thing
that can go wrong and that is
um what can happen is that you want to
approximate a value From Below or you
want to come from above but you do it in
the wrong direction like
uh in other words you want to round down
but you round it up instead and that can
lead to severe security vulnerabilities
I will show you some examples that you
will recognize maybe and then but I'm
not going to work on these real world
examples I'm working on a like
simplified example
um and make sure to understand like the
two-way trading problem
um
because otherwise you won't be able to
follow my talk everything like get to
this point stay with me until this point
and then you can make sense of this talk
um so
uh grounding errors
um they are well we need to accept them
we cannot do exact arithmetic on the
blockchain it's not feasible so and we
found
rounding errors in uni Swap
and luckily this running error was fixed
um before uni swap V1 was deployed but I
leave it to your imagination
how the blockchain landscape would have
looked liked
um if this bug was not caught during an
audit and then we had like two more
examples Solana token Landing contract
and Solana token stable swap
um
and there so the um these bugs were
actually caught doing like why these
contracts haven't deployed and at the
peak time there were like three billion
assets at risk
um
so luckily again uh
these were not exploited by the but they
were found by white hackers uh before
any serious damage could it could be
done
um so
uh I cannot get into detail into any of
those but like I promise you if you
follow my talk then you will be able to
visit the links that I put on the slide
um and you will be able to make sense of
these exploits and and like how or these
vulnerabilities and how they could have
been exploited if they haven't been
fixed
so
um I want to show you the two-way
trading problem and I promise you this
is like the most mathematical slide on
my uh on my entire talk which is strange
well because I'm talking about running
errors right okay but
um I want to introduce to you to my
image now with friend Alice she's right
here hi Alice and I will demonstrate to
you the two-way rounding problem as the
two-way trading problem so first I'm
going to offer Alice a trade and we do
it with exact arithmetic and then we're
doing we are going to replay the wall
the role play and then we are doing it
with rounding so hi Alice also basic
scenarios we have two currencies we have
dollar and Gill Gill is just a fantasy
currency
um and we have exchange rate currently
uh that says I can get like
um two Gill for one dollar so exchange
rate is two so I'm Raul I have one girl
in my pocket and this is Alice and hey
Alice do you want to trade with me I can
offer you one gear how many dollars do I
get for that and let us do the
calculation
he gives me one dollar he gives me one
kill so I need to divide by the exchange
rate uh so you get one you get half a
dollar back from me so now I have half a
dollar so I get back to Alice and say
hey Alice I don't want my half dollar
anymore
um can I get my Gill back and I offer
Alice the uh half the dollar and she
does the computation and now this time
she needs to
um to to multiply by the exchange rate
and so she ends up with one girl
everything went fine I started with one
Gill and I ended up with one kill right
so now let's do the same thing with
rounding so and for Simplicity I'm just
rounding to like uh there's there's no
decimal no digit after the decimal point
that's just for Simplicity
um so now Alice I'm Raul I have one uh
Guild to offer how many dollars do I get
for that let's do the computation and
but she does a rounding error
um
do I have a laser pointer here no I
don't
um so she does a rounding aware in this
computation so
we divide two by one this gives us two
and then we want divide one by two which
gives us 0.5 and we are using uh
rounding to the nearest neighbor here so
that means we are rounding up
um so that means I get one dollar back
from Alice so now I have one dollar
uh I go back to our list and say hey
Alice I don't want my dollar anymore can
I get my Gill back and again Alice do
the calculation this time she's not even
doing a rounding error
um but she ends up giving me two kill
and that is the basic problem right I
started with one girl I did two trades
with Alice and I ended up with two
guilds in my pocket so in other words I
just like created money out of thin air
so let's bring this example into the
blockchain context
um so the important thing here in this
example was that I needed two trades and
like in in many smart contracts you will
see
a pair of trading functions like a
deposit and a redu-im function or
deposit and withdraw stake and unstake
function and so on
and so what what happened here what went
wrong like you know have a look at the
red line so I deposited one Guild to
Alice and then I immediately redeemed it
like in the same transaction and I was
able to make two kill out of that so I
created money out of thin air so
um
now okay so we we don't want that right
we need to fix that so we need to like
make a sanity check that we don't get
like more money out than we put in
um and this is the second line here this
is my sanity assumption that when I put
one Guild into the contract or
um I should be able to get at most one
kill out if I immediately redeem
um and of course this concept can be
generalized it shouldn't only hold for
one gear but it should essentially hold
for for
um arbitrary amounts that I'm putting
into the contract
um so this is what a typical the typical
implementation of
um a deposit and a redeem function look
like looks like and
um what you can see here is like let's
walk over the deposit function real
quick so the deposit function accepts an
asset amount and then it converts this
asset amount into shares just by
multiplying the amount of assets with a
current exchange rate
then we are transferring the asset we
are pulling in we are pulling the Assets
in from the
um from the user uh then we are minting
some shares and finally we return the
shares that we have minted and the
redeem function is similar and with what
I just told you you can see or maybe you
cannot see it because well I didn't use
the uh you cannot see the implementation
of the multiplication function
um but like this contract is suffering
uh from the exact vulnerability that
that I showed you before
um and that was present in a like more
complicated uh a more complex setting in
this uh in this unit swap contract that
I talked about earlier
um so this multiplication function and
this division function is is implemented
as like rounding to the nearest neighbor
and that is the mistake that we did here
but like how do we actually know in
which direction we should round and
um there's like a very simple uh
a very simple rule of some rule of thumb
that I can give you and that is I call
it keep the change that means whenever
we whenever we are rounding up uh oh
sorry whenever we have incoming assets
like accept assets from the user then we
are going to round up and whenever like
we are sending assets out to the user we
are rounding down and if we follow this
this rule that means you will
approximate your values from the right
direction and users won't be able to
create money out of thin air and doing
your contracts that is the simple rule
so that means like let's revisit the
example from before so
um like let's walk over the deposit
functions so instead of like just
multiplying I just know now I use now
um a variation of the multiplication
function that always rounds down and it
runs down because I'm sending the assets
out to the user
and for the redeem function here in this
example it's it's the same
um so now
how can we actually be sure that our
implementation is correct I mean this
example was really simple and you were
maybe able to follow it like on the spot
um but but like uh
um when you're working when you're a
developer and working on a like real
world contract your logic will be more
complex so you want to have tests that
ensure that you can
um actually
um detect counter examples and achieve a
higher level of confidence so we are now
looking at the
um at a property test so
um that is basically just like a unit
test
um but it has parameters parameters to
it so it has two parameters shares per
asset which should just uh it's just the
current exchange rate and it has another
very in another parameter assets and
when this test is run
um uh Foundry by the way that's a
Foundry test I don't know if I have said
that
um
so and when Foundry wants this test it
will like insert call this test with a
bunch of random inputs
um like uh and that's the benefit of a
unit test when you have a unit test and
you want to detect such routing error
you basically need to be lucky and like
put the right numbers into the unit test
and guess the counter example like with
this Foundry test Foundry does a
guessing for you and can it do much
quicker than you ever could like it can
one like 1000 samples or two thousand
two thousand samples in a couple of
milliseconds
um so and I want now to have you a look
at line 14 and 15 and see that it
resembles the property that we specified
above so I hope that you can see in line
14 that we are like executing a deposit
function and in the same transaction we
are executing the redeem function and
like that is exactly what the property
is above uh what the property above says
so and then then there's some
boilerplate code to to that test as well
uh that's like it's not like mandatory
to understand but like if you look at
lines two to line sevens uh to line
seven these are just some assumptions
that I make over the inputs and I put
these assumptions there just to avoid
arithmetic overflow and arithmetic
underflow because if I went into such a
situation my test would simply revert
and I I only want to execute like uh the
happy path with this test
um and then like line eight to line 12
is just a basic test setup so that I
that my contract is in the state that it
can actually fulfill the transfer
functions that I'm calling in line 14.
so
um
fuzzing is good and you should actually
you should do it when you test for
rounding errors but like fuzzing is not
enough that's the uh the sad message
here like the third example from the um
from the first slide that I showed you
um
this example it was
um the uh Stables stable swap contract
um
uh suffered from this rounding Direction
vinyl ability although it was heavily
fast and like this excerpt that you see
here is like from the blog post uh that
explains this vinyl ability and just let
it read me let it uh let me read it out
to you so another interesting takeaway
is that fuzzing can give you a false
sense of security prior to our report
saber had already deployed comprehensive
fuzzles for their state for their swept
implementation a researcher looking at
the code coverage alone might come to
the incorrect conclusion that such
extensively fast code couldn't possibly
have a vulnerability
all right so what else can we do to
increase our confidence in in our
implementation and like one possible
solution is that we could use like that
we could use symbolic execution on top
of fuzzing so if you see that table on
the left hand side there are some like
some properties uh uh that that fuzzing
has and on the right hand side on the
white column you see some properties of
symbolic execution but I don't want to
want you to think about like this slide
as fuzzing versus symbolic execution
it's like you can get the best of both
worlds if you combine both of these
efforts and we recently
um so we at one time verification we
have a symbolic execution engine that's
called KVM that's it's a symbolic
execution engine tailored to the um to
to the ethereum virtual machine and we
recently added a feature to that that
allows you to put Foundry tests into it
and instead of fuzzing over the
parameters so instead of choosing random
input variables for the parameters and
we do symbolic execution over the uh
over the parameters and that has like
different trade-offs so
um the nice thing is that well for
Foundry and for symbolic execution with
the evm you get to specify your tests
and your specifications in Foundry
itself in solidity itself sorry
uh so that's that's like easier than um
than having to uh to to write your tests
in JavaScript or typescript developers
like Foundry especially because of this
property
um
so but that also means
like when it comes to Foundry that you
are somewhat limited to the
expressiveness of solidity and there are
a bunch of like
um safety properties that you simply
cannot express in solidity and that's
like one advantage of this symbolic
execution
um approach like that you can actually
you can escape from from the uh from the
specification format and you can
actually use uh the the K language to
specify uh to gain additional
expressiveness and express more
properties
um
so Foundry fuzzing is extremely fast
it's like you can run 1 000 samples and
a couple of milliseconds and that is
like really important for for developers
who want to get instant feedback
um
so and compared to that symbolic
execution is slow so
um
um and there's a reason for that so
symbolic execution can can give you much
more safety guarantees than than fuzzing
can but that also means like it's
it's um
computationally much more expensive than
fuzzing
um so it's slow but it's not too slow
like uh it works for example you could
simply integrate it into your CI
Pipeline and let the um let the prover
run like on your nightly builds for
example and like this shows like the
benefit of like composing both
um strategies like fuzzing with Foundry
and then symbolic execution with um with
KVM
um
so
uh
I don't want to go over every line in
this table and but I want to talk about
the false positives and the false
negatives
so
Foundry doesn't have false positives and
what I mean by that is when Foundry
comes up with a counter example that
means that counterexample really works
it breaks your code so it doesn't come
up with a with a counter example that
does not work your code so there's no
false positive
but Foundry has false negatives and that
is simply if Foundry is not able to
choose the right input variables
um that means it fails to guess the
right counter example and at the end
founder will tell you that test that
that test actually passed and that is
like the false sense of security that
you get from
um using Foundry alone so if we use
symbolic executions like we cover 100 of
the input domain and we will find that
counter example there's no matter what
um so there are no false negatives when
you use uh when you use kevm
um
then there's a diff there's another
trade-off and that is Foundry is
extremely easy to use I I'd argue it's
even easier to use than than hardhead or
or truffle uh for testing because well
the developers the smart contract
developers are already familiar with um
with solidity like the language that
they use to write their contracts and
um so that makes foundu very easy to use
uh symbolic execution with KVM is is a
little bit different like it's very easy
to try out it's it's like if you have it
installed on your machine and you have
Foundry tests specified you can just try
running
um the KVM on that and maybe you're
lucky and maybe uh the KVM will tell you
right your test pass or your your your
um yeah your test was proven or it was
like or we found a counter example but
in some cases
um you will get like a third state that
is you didn't pass you didn't fail but
we are not sure like we don't know and
if you end up in this we don't know
State
um that is when a human
needs to drive the proof forward and
that is actually something uh that needs
some practice I think I don't think it's
impossible to learn uh I learned it so
I'm sure you guys can
um but it's it's harder than just uh
just calling um a Foundry test so
uh
one final example of running running
Foundry and running the KVM symbolic
execution engine on the same test Suite
so on the uh on the top image I just
called Forge test
um and I can see the output like
um that tells me okay uh I was running
one test
um and it passed I tried
256 uh samples on that tested that it
means Foundry
um uh won this test was 256 different
inputs
um
and then I can use like after I've won
the founder test I can run KVM Foundry
compile and give it a Foundry out
directory as a parameter and what this
comment will do is it will turn The
Foundry test Suite into a proof
obligation for the symbolic execution
engine like it's a compile step and then
um
when I've done that I can actually try
to discharge this proof obligation by
one in KVM Foundry proof
um and the output that you see here is
the lucky case that our like symbolic
execution was actually able to discharge
the proof obligation and that's why it
says top top at the bottom
um
so
but well when this when a test doesn't
pass you will get a counter example that
is not as easy like to link back to the
original code of the test than the
um then The Foundry country example or
even worse it will give you this unknown
State and like making sense of this
unknown State really requires some
practice you you need to to learn to
read these configurations to need to eat
these stuck States
um so that's basically it with my talk
um I've just
um one more a couple of more notes so I
work at one time verification and we
have a research department and we just
recently
um posted some open research challenges
on our website research dot runtime
verification.com and if you are a
researcher go to that website see if
something interests you and we have like
multiple ways to collaborate with you
like if everything if anything interests
you
all right and then like one other
announcement
um
a colleague of mine Richardson audience
somewhere I see them uh he's giving a
workshop on formal methods for the
working D5 Dev tomorrow at uh at 11AM in
Workshop room number three so uh if you
like this talk uh go ahead and visit
Richard's talk it's uh I highly
recommend it right and that's it I think
we have some time for questions do we
we have
do we have a microphone for questions
hello uh great great presentation uh I
have a couple of questions can you go
back to the table that you show both uh
like fasting and symbolic execution
I have it on the screen but I don't have
it on the projector
um
[Music]
there it is okay great so you you put
like in the fasting column that it
requires no inter in human intervention
but you need someone to write the
properties it's the same for the
symbolic execution right so if you have
good properties you will catch good bags
if you don't have good properties you
will have catch no bugs right and this
is the same with the examples that you
show like see fasting is not enough uh
this code was fast but perhaps they are
not using the correct uh properties so
what is what is your take on this yeah
yeah that's true so uh this is not like
fully automatic like for example when
you run a static analysis tool on your
code base then you essentially have to
do nothing you can just like hit a
button and one Slither on your code base
so for fuzzing you need to write down
the tests and like like getting the
tests getting the white tests is is a
challenge on its own it's not like it
doesn't come easy it has to be practiced
um and the same is even more to when you
do symbolic execution
um because where symbolic execution can
also can also be a foot gun if you don't
know how to use it appropriately all
right yeah yeah definitely and the other
thing very quickly you put like false
negatives like on fun on fasting which
is which I agree and you put no false
negative on symbolic execution or
whatever you said that you could have at
third state in which you don't know if
it's true or is false
that sounds like a false negative to me
like you you don't know the answer the
tool doesn't know the answer so it is it
is like yeah but it doesn't say I
discharged this proof application and
everything is right it says you I'm
stuck and that is um you should
interpret this as
um I need to put more effort in the
proof or in the code to get it to like a
final state that says true or false yeah
but it's the same for for fasting when
you when you say like a past like a
tested pass it's simply because you
didn't you didn't put enough enough time
right to to run it so it's it's a matter
of interpretation and it's a little
misleading you could try like passing
over
um like the entire input space and then
you will also have like no false uh no
false negatives you could try that but
like you will never terminate like uh
but but that would work yeah come to my
talk tomorrow because we'll be be going
over how to write properties that's
basically the next talk
[Music]