►
From YouTube: Tackling Rounding Errors with Precision Analysis by Raoul Schaffranek | Devcon Bogotá
Description
Visit the https://archive.devcon.org/ to gain access to the entire library of Devcon talks with the ease of filtering, playlists, personalized suggestions, decentralized access on Swarm, IPFS and more.
https://archive.devcon.org/archive/watch/6/tackling-rounding-errors-with-precision-analysis/
Rounding errors in smart contracts can lead to severe security vulnerabilities. In this talk, we'll motivate the importance of rigorous numerical analysis through real-world exploits, and review existing precision analysis techniques. We'll then argue for the development of automated error propagation analysis tools to overcome the tediousness of manual efforts.
Speaker(s): Raoul Schaffranek
Skill level: Intermediate
Track: Security
Keywords: Security techniques,code quality,rounding errors
Follow us: https://twitter.com/efdevcon, https://twitter.com/ethereum
Learn more about devcon: https://www.devcon.org/
Learn more about ethereum: https://ethereum.org/
Devcon is the Ethereum conference for developers, researchers, thinkers, and makers.
Devcon 6 was held in Bogotá, Colombia on Oct 11 - 14, 2022.
Devcon is organized and presented by the Ethereum Foundation, with the support of our sponsors. To find out more, please visit https://ethereum.foundation/
A
A
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.
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.
A
A
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
and
make
sure
to
understand
like
the
two-way
trading
problem,
because
otherwise
you
won't
be
able
to
follow
my
talk.
A
Everything
like
get
to
this
point
stay
with
me
until
this
point,
and
then
you
can
make
sense
of
this
talk
so
grounding
errors.
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
before
uni
swap
V1
was
deployed,
but
I
leave
it
to
your
imagination
how
the
blockchain
landscape
would
have
looked
liked.
A
So
luckily
again
these
were
not
exploited
by
the,
but
they
were
found
by
white
hackers
before
any
serious
damage.
Could
it
could
be
done
so
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
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.
A
So
I
want
to
show
you
the
two-way
trading
problem
and
I
promise
you.
This
is
like
the
most
mathematical
slide
on
my
on
my
entire
talk,
which
is
strange
well
because
I'm
talking
about
running
errors
right,
okay,
but
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.
A
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
and
we
have
exchange
rate.
Currently
that
says,
I
can
get
like
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?
A
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.
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.
A
Can
I
get
my
Gill
back
and
I
offer
Alice
the
half
the
dollar
and
she
does
the
computation
and
now
this
time
she
needs
to
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
there's
there's
no
decimal,
no
digit
after
the
decimal
point.
That's
just
for
Simplicity!
A
So
now,
Alice
I'm
Raul
I
have
one
Guild
to
offer
how
many
dollars
do
I
get
for
that?
Let's
do
the
computation,
and
but
she
does
a
rounding
error.
Do
I
have
a
laser
pointer
here?
No
I
don't
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
rounding
to
the
nearest
neighbor
here.
So
that
means
we
are
rounding
up.
A
A
Do
the
calculation
this
time
she's
not
even
doing
a
rounding
error,
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.
A
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.
A
A
So
this
is
what
a
typical
the
typical
implementation
of
a
deposit
and
a
redeem
function.
Look
like
looks
like,
and
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.
A
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
like.
A
Let's
walk
over
the
deposit
functions
so
instead
of
like
just
multiplying
I,
just
know
now:
I
use
now
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.
A
A
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,
but
but
like
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
actually
detect
counter
examples
and
achieve
a
higher
level
of
confidence.
A
So
we
are
now
looking
at
the
at
a
property
test,
so
that
is
basically
just
like
a
unit
test,
but
it
has
parameters
parameters
to
it.
So
it
has
two
parameters:
shares
per
asset,
which
should
just
it's
just
the
current
exchange
rate
and
it
has
another
very
in
another
parameter
assets
and
when
this
test
is
run
Foundry
by
the
way,
that's
a
Foundry
test.
A
I,
don't
know
if
I
have
said
that
so
and
when
Foundry
wants
this
test,
it
will
like
insert
call
this
test
with
a
bunch
of
random
inputs
like
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.
A
A
So
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
the
sad
message
here
like
the
third
example
from
the
from
the
first
slide
that
I
showed
you
this
example.
It
was
the
Stables
stable,
swap
contract
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.
A
That
explains
this
vinyl
ability,
and
just
let
it
read
me,
let
it
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.
A
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
that
that
fuzzing
has
and
on
the
right
hand,
side
on
the
white
column.
A
If
you
combine
both
of
these
efforts-
and
we
recently
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
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
over
the
parameters
and
that
has
like
different
trade-offs.
A
So
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,
so
that's
that's
like
easier
than
than
having
to
to
to
write
your
tests
in
JavaScript
or
typescript
developers
like
Foundry,
especially
because
of
this
property.
A
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
safety
properties
that
you
simply
cannot
express
in
solidity,
and
that's
like
one
advantage
of
this
symbolic
execution
approach
like
that.
You
can
actually,
you
can
escape
from
from
the.
A
From
the
specification
format-
and
you
can
actually
use
the
the
K
language
to
specify
to
gain
additional
expressiveness
and
express
more
properties,
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
so
and
compared
to
that
symbolic
execution
is
slow,
so
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.
A
It's
computationally
much
more
expensive
than
fuzzing,
so
it's
slow,
but
it's
not
too
slow
like
it
works.
For
example,
you
could
simply
integrate
it
into
your
CI
Pipeline
and
let
the
let
the
prover
run
like
on
your
nightly
builds
for
example
and
like
this
shows,
like
the
benefit
of
like
composing.
Both
strategies
like
fuzzing
with
Foundry
and
then
symbolic
execution
with
with
KVM.
A
So
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.
A
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
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
so
there
are
no
false
negatives.
When
you
use
when
you
use
kevm,
then
there's
a
diff
there's
another
trade-off,
and
that
is
Foundry
is
extremely
easy
to
use.
A
If
you
have
it
installed
on
your
machine
and
you
have
Foundry
tests
specified,
you
can
just
try
running
the
KVM
on
that
and
maybe
you're
lucky,
and
maybe
the
KVM
will
tell
you
right
your
test
pass
or
your
your
your
yeah.
Your
test
was
proven
or
it
was
like,
or
we
found
a
counter
example,
but
in
some
cases
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.
A
A
One
final
example
of
running
running
Foundry
and
running
the
KVM
symbolic
execution
engine
on
the
same
test,
Suite
so
on
the
on
the
top
image.
I
just
called
Forge
test
and
I
can
see
the
output
like
that
tells
me.
Okay,
I
was
running
one
test
and
it
passed.
I
tried
256
samples
on
that
tested
that
it
means
Foundry
won.
This
test
was
256
different
inputs
and
then
I
can
use
like
after
I've
won
the
founder
test.
A
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
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.
A
So
that's
basically
it
with
my
talk,
I've,
just
one
more,
a
couple
of
more
notes,
so
I
work
at
one
time,
verification
and
we
have
a
research
department
and
we
just
recently
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.
A
If
everything,
if
anything
interests
you
all
right
and
then,
like
one
other
announcement,
a
colleague
of
mine,
Richardson,
audience
somewhere
I
see
them
he's
giving
a
workshop
on
formal
methods
for
the
working
D5
Dev
tomorrow
at
at
11AM
in
Workshop
room
number
three.
So
if
you
like,
this
talk,
go
ahead
and
visit
Richard's
talk,
it's
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.
C
C
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.
This
code
was
fast,
but
perhaps
they
are
not
using
the
correct
properties.
So
what
is
what
is
your
take
on
this
yeah.
A
Yeah,
that's
true,
so
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.
C
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.