►
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/bad-proofs-in-formal-verification/
Formal verification can be a huge boon to smart contract security as it checks all possible execution paths. Unfortunately, even verified code can be faulty if the formal specification contains mistakes. "Bad" proofs can lead to false confidence in the code and premature deployment. This talk will discuss different types of "bad" proofs and how to avoid them.
Speaker(s): Uri Kirstein
Skill level: Intermediate
Track: Security
Keywords: Formal,Verification,Bugs
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
A
A
Let's
go
formal
verification
is
the
process
where
we
take
a
piece
of
software
and
try
to
see
if
it
behaves
According
to
some
pre-fined
set
of
of
rules.
We
call
those
security,
Properties
or
rules.
We
call
them
specifications
and
they're
one
of
the
two
inputs,
along
with
the
code
that
we
want
to
check
that
we
need
to
feed
into
the
the
software
that
that
executes
the
formal
verification
in
this
case,
for
example
the
circular
approver
and
then
after
the
prover,
gets
those
two
inputs.
A
Let's
show
that,
with
a
simple
example
of
a
facility
pseudocode,
this
is
a
transfer
function,
we're
driving
we're
transferring
some
amount
of
tokens
from
one
address
to
the
other
and
an
example
of
a
specification
that
we
can
give
to
to
the
software.
That
does
the
formal
verification
is
this
invariant
that
says
that
the
total
supply
of
the
token
is
equal
to
the
sum
of
the
balances
of
all
addresses
that
hold
a
token,
which
makes
sense
if
we
feed
those
two
inputs
to
the
prover,
we
will
get
a
bug.
A
We
get
a
counter
example
A
specific
scenario
where
that
invariant
doesn't
hold
anymore.
Here
we
can
see
that
when
we
pass
an
amount
of
18
from
the
address
of
Alice
to
the
address
of
Alice,
we
get
a
violation.
We
see
that
Alice's
Alice's
balance
grew
by
18
tokens,
which
it
shouldn't
have
now
the
invariant
is
broken,
and
that's
why
it's
a
bug,
however,
if
we
try
and
fix
that
solidity
code,
let's
say
to
this:
implementation,
which
doesn't
contain
bug
will
actually
get
a
proof,
and
what
does
that
proof
mean?
A
It
means
that
the
sum
of
the
balances
of
the
token
for
all
addresses
before
and
after
the
transfer
is
equal,
and
then
we
can
be
sure
that
it's
true,
no
matter
which
addresses
we
chose
and
which
amount
we
have
chosen
and
that's
one
of
the
key
advantages
of
formal
verification.
It
is
exhaustiveness
we're
not
checking
for
a
specific
set
of
inputs,
but
instead
we're
covering
the
entire
input
space
that
way
we're
able
to
find
bugs
that
are
often
or
sometimes
missed
by
humans.
A
Another
big
Advantage
is
that
whenever
we
get
a
violation,
it's
very
easy
to
verify
it.
We
get
specific
numbers
specific
addresses
and
we
can
see
and
run
it
ourselves
and
see
if
we
get
a
violation
or
not
and
try
to
track
and
see
exactly
where
the
problem
lies
and
also
we
can
get
a
proof
of
correctness,
which
is
something
great
that
we
can't
really
get
through
many
other
security
methods
for
smart
contracts.
A
However,
those
proofs
are
very
hard
to
verify.
Obviously,
we
cannot
go
ourselves
through
all
the
different
inputs
and
see
that
it's
true
or
not
else
would
have
done
that,
instead
of
trying
to
prove
it
right
and
actually
sometimes
our
proofs
don't
actually
mean
what
we
think
they
do.
Sometimes
we're
proving
something
completely
different
from
what
we've
intended
and
those
proofs
are
bad
because
they
can
give
us
a
false
sense
of
security.
A
A
Let's
look
deeper
into
those
specifications.
I've
been
telling
you
about
this
code
that
you
see
on
the
screen
behind
me
is
written
in
a
specific
language
called
the
circular
verification
language
used
for
writing
specifications,
but
the
same
principles
hold
no
matter
how
you
represent
your
property,
the
general
Anatomy
is
dividing
into
three
different
parts.
The
first
is
the
precondition.
A
Then
we
have
an
operation
and
then
we
have
a
post
condition
and
if
we
look
at
this
specific
example
here
we
check
that
the
transfer
function
behaves
as
intended.
The
way
that
we
do
that
is
that
at
first
our
precondition,
we
check
the
balance
of
Bob.
For
a
specific
token,
that's
our
precondition
and
we
keep
that
number.
A
Then
we
do
the
operation
in
this
case.
It's
the
transfer
function
and
after
the
operation
we
check
the
post
condition.
We
check
the
balance
of
the
tokens
of
Bob
after
the
transfer
and
see
if
it
is
indeed
equal
to
the
balance
Bob
had
before
the
transfer
plus
the
amount
of
tokens
we
have
transferred
to
Bob.
A
Let's
look
at
it
more
visually
and
when
we
Define
a
property,
we
Define
a
starting
state
by
the
different
constraints
that
we
give
and
that's
the
circle.
The
arrow
represents
the
operation,
and
then
we
want
to
land
within
one
of
the
desired
States.
One
of
the
states
that
satisfy
or
in
which
the
assert
expression
that
we
had
holds.
Okay,
so
the
desired
behavior
is
that
every
state
that
is
within
the
starting
States.
A
A
That's
a
counter
example,
that's
a
violation,
that's
what
might
be
a
bug,
and
the
interesting
thing
to
note
is
that
if
the
tool
cannot
find
a
counter
example
for
the
specification
or
the
property
that
we
provided
it,
then
it
will
output
us
approve,
and
that
is
because
in
in
logic,
we
Define
a
false
statement.
As
a
statement
to
which
we
can
give
a
counter
example,.
A
A
The
first
step
is
what
we
call
a
vacuous
rule
or
vacuous
proof.
Vacuous
is
something
empty
or
mini
glass
or
insignificant,
and
this
is
better
shown
by
a
real
life
example:
I
am
29
years
old
and
I.
Don't
have
any
children
yet
and
I'm
claiming
the
following
statement:
if
I
let
my
children
drink,
Colombian
coffee,
they
will
sleep
better
at
night.
A
Is
that
statement
true
or
false?
So
if
we
want
to
say
that
the
statement
is
false,
we
need
to
provide
a
counter
example.
So
we
need
to
start
from
one
of
the
starting
States,
meaning
you
need
to
choose
one
of
my
children.
Then
you
need
to
do
the
operation,
meaning
let
them
drink,
Colombian,
coffee,
hopefully
not
too
hot,
not
to
injure
them,
and
then
you
want
to
see
that
they
actually
do
not
fall
asleep
at
night.
A
A
A
However
I
can
also
say
something
that
apparently
seems
completely
contradictory.
I
can
say
that
if
I,
let
my
children
drink,
Colombian
coffee,
they
will
not
sleep
at
night,
sounds
completely
the
opposite.
Yet
the
same
principles
still
hold.
You
still
cannot
provide
a
counter
example
here:
I
still
don't
have
a
child,
and
therefore
that
statement
is
also
true.
A
A
A
One
of
Sir
torah's
employees
was
working
on
open,
Zeppelin
contracts
as
well
as
writing
a
rule
of
property
that
he
thought
should
hold
on
the
tokens
of
open
Zeppelin.
However,
that
rule
that
specification
contained
an
error.
You
see
in
the
middle
of
the
rule.
We
have
this
requirement
that
the
balance
of
the
adverse
zero
for
a
given
token
must
be
zero.
A
That
can
never
happen,
because
every
call
to
the
function,
balance
off
for
the
address
0
will
revert
and
if
it
reverts
in
particular,
it
never
returns
back
the
value
zero.
Therefore,
nothing
can
satisfy
this
requirement.
If
nothing
can
satisfy
this
requirement,
we
don't
have
any
starting
States.
This
is
a
vacuous
rule
and
therefore
it
doesn't
actually
matter
what
appears
later
in
the
rule.
After
that
requirement,
it
will
be
true,
no
matter
what
we
do
and
in
fact
I
could
try
and
insert
something
completely
ridiculous.
A
A
Unfortunately,
vacuous
rules
are
not
just
an
academic
concern,
for
modification
has
been
used.
A
lot
on
Hardware
along
the
years
and
Studies
have
found
that
about
20
percent
of
specifications
written
on
Hardware
on
the
first
time
are
actually
vacuous
and
whenever
they
are
vacuous,
they
hint
at
a
real
problem,
either
at
the
code
you're
trying
to
verify
or
your
specification.
A
What
we
do
is
that
we
take
the
same
specification
as
before,
exactly
as
it
is
and
add
something
at
the
end,
we
add
an
assertion
of
false.
Obviously,
assertion
of
false
is
always
false,
so
we
want
so.
We
expect
the
rule
to
fail.
We
expect
to
get
a
counter
example
right,
because,
because
nothing
can
can
satisfy
false.
A
However,
if
we
do
not
get
a
counter
example,
if
the
rule
is
proven
that
that
means,
we
didn't
actually
reach
that
last
line
of
the
specification,
we
didn't
reach
that
last
line
of
the
specification,
because
that
requirement
erased
out
all
the
possible
starting
States.
It
doesn't
matter.
We
never
reach
that
last
line
and
that's
how
we
check
that
we,
we
say
something
absurd
at
the
end
and
we
see
if
we
fail
or
not.
If
we
don't
fail,
that's
the
problem.
That's
when
we
know
that
a
rule
is
vacuous.
A
For
completeness,
I
will
say
that,
usually,
when
we
have
vacuous
rules,
it's
not
due
to
one
One
precondition
One
requirement.
That
is
never
satisfiable.
It's
usually
due
to
a
combination
that
their
intersection
is
actually
empty
and
not
satisfiable,
but
each
part
by
its
own
makes
sense.
For
example,
here
if
you
require
that
X
is
smaller
than
y,
maybe
we
can.
We
can
prove
the
property.
Let's
say
we
add
another
requirement
y
smaller
than
Z.
Now
we
limit
the
starting
state
only
to
be
the
intersection.
A
And
if
we
add
this
third
requirement
that
Z
is
smaller
than
x,
then
we
have
no
intersection
anymore
here
by
transitivity
we
say
that
X
is
smaller
than
itself
and
that's
never
true
for
any
number.
Therefore,
we
don't
have
any
starting
States,
and
this
rule
is
vacuous
but
note
that
some
combination
of
those
requirements
could
make
for
a
sensible
rule.
A
For
example,
let's
look
at
this
Rule
and
this
rule
tries
to
check
again
the
Integrity
of
the
transfer
function.
We
check
that
the
balance
of
a
recipient
is
zero.
Then
we
transfer
some
positive
amounts
of
tokens
to
that
recipient.
Then
we
assert
that
the
bounce
of
tokens
for
that
recipient
actually
grew.
A
However,
this
rule
on
the
screen
is
wrong
because
we
didn't
check
the
balance
of
the
user.
Before
and
after
the
transfer,
we
checked
that
the
balance
of
the
of
the
user
after
the
transfer
is
not
smaller
than
itself,
and
this
is
something
that's
always
true
for
any
number
and
that's
a
problem,
because
in
this
case
we
didn't
actually
check
what
the
transfer
function
is
doing.
We're
checking
something
that
is
always
true.
A
The
transfer
function
could
burn
all
the
tokens
could
send
all
the
tokens
to
me,
or
you
can
do
something
entirely
different
and
not
move
any
tokens
around.
We
don't
know.
We
didn't
actually
check
that
if
we
look
at
it
visually
at
autology,
something
is
always
true,
so
it
encompasses
the
entire
space
of
possibilities.
So
here
the
arrow
representing
the
operation
lands
somewhere
within
the
space
of
possibilities
and
therefore
is
true.
A
A
A
A
The
way
with
the
reproving
variance
is
by
induction,
and
you
might
be
familiar
with
it
from
school,
it's
similar
to
proving,
by
induction
things
about
natural
numbers.
We
have
the
base
of
the
induction,
we're
trying
to
see
if
the
condition
is
true
right
after
calling
the
Constructor
and
then
we're
doing
the
step
of
the
induction.
That
is,
we
assume
that
the
invariant
holds.
We
operate
some
function
of
the
contract,
that
must
be
public
or
external,
and
then
we
check
that
that
it's
still
true
after
the
same
condition
is
true.
A
A
A
What
they
tried
to
to
prove
here
is
that
an
asset
in
their
system
and
their
system
allows
lending
and
borrowing
at
fixed
rates.
By
the
way,
an
asset
cannot
be
counted
both
as
a
bitmap
asset
and
as
an
active
asset,
and
here
we
see
that
they
try
to
reach
that
conclusion.
At
the
end,
the
highlighted
line
at
the
end
says
that
the
same
currency
can't
be
both
active
and
bitmap.
A
A
So
if
you
look
just
at
that
part
of
the
or
statement
we
see
that
the
Vietnam
currency
is
not
zero
and
the
active
currency
is
zero,
so
zero
and
non-zero
are
always
different.
So
the
conclusion
is
true:
trivially,
true
what
happens
if
you
look
at
the
other
part
of
the
or
statement
here
we
require
that
the
active
Mass
currency
is
zero
emotional
system
assets
are
represented
using
14
bits,
plus
two
more
bits
for
a
mask,
so
the
masking
passes
all
16
bits
and
the
unmasked
encompasses
the
lower
14..
A
Therefore
it
follows
that
it
is
zero
itself
and
we
have
actually
reached
the
same
statement
as
we've
reached
before
meaning.
If
the
bitmap
currency
is
not
zero
and
the
active
currency
is
zero,
then
they
must
be
different
and
that's
always
true,
because
zero
is
always
different
than
non-zero
and
in
total
we
get
that
this
entire
statement,
although
complex,
is
their
statutology
hard
to
see,
and
you
can
understand
why
the
person
that
wrote
it
could
make
that
mistake.
A
It's
not
apparent,
but
this
is
indeed
a
tautology
and
unfortunately
the
code
was
deployed
thinking
that
it
cannot
contain
that
bug
and
unfortunately
it
did
the
bug
light
in
this
specific
function
enable
bitmap
currency,
and
it's
a
bit
hard
to
see
the
bug
itself.
So
I'm
just
going
to
show
you
the
exploit
scenario.
A
A
A
A
The
interesting
thing
is
that
these
invariant
I
have
shown
before
is
pretty
close
to
the
correct
one.
The
correct
one,
the
fixed
invariant,
will
look.
Something
like
this
actually
looks
simpler
in
this
case,
and
the
interesting
thing
to
see
is
that
if
we
run
this
invariant
on
the
buggy
version
of
the
code,
we
get
the
exact
same
counter.
Example,
where
you
set
one
token
as
a
bit
of
currency
deposit.
Another
token
then
move
the
Bitcoin
currency
to
be
the
other
active
currency.
A
A
To
sum
it
up,
specifications
are
written
by
humans
just
like
who
it
is,
and
they're
equally
or
even
harder
to
write.
This
is
something
you
have
to
keep
in
mind.
You
shouldn't
expect
your
specifications
to
be
perfect.
Like
you,
don't
expect
your
code
to
be
perfect,
therefore,
you
should
always
check
your
spec.
It's
good,
if
other
another
person
reviews
it.
If
an
expert
reviews
it
and
also
even
better,
to
use
some
automatic
checks
like
we
insert
or
provide
you,
you
should
always
suspect
what
the
tool
gives
you
like.
A
You
would
any
other
security
tool
when
you
get
a
bug,
it's
always
a
good
result,
because
you
can
always
check
it
and
see
if
it's
good
or
not.
However,
when
you
get
a
proof,
you
don't
have
a
good
way
to
verify
it,
and
the
best
course
of
action
is
to
be
suspicious
of
it.
Don't
take
it
blindly
and
just
upload
your
code
and
obviously
we
could
have
seen
that
writing
the
correct
specifications
you
can
still
find
bugs
that
are
worth
millions
or
billions
of
dollars.
B
Thank
you
so
great
presentation,
so
it
seems
from
from
what
you
explained
that
when
you
have
a
bad
proof
that
is
vacuous,
you
can
just
detect
it
just
with
a
coverage
report.
Let's
say
in
which
part
of
your
of
your
specification
was
never
reached.
So
it's
it's!
It's
like
immediate,
but
when
you
have
a
tautology,
it's
more
difficult
because
you
will
need
to
remove,
let's
say
preconditions
and
removing
precondition.
You
can
have
like
10
preconditions.
You
don't
know
which
one
perhaps
a
combination
of
this.
B
A
Okay,
so
one
thing
I
want
to
emphasize
the
checks
that
I
have
shown:
you
don't
catch
all
types
of
acuities
and
not
all
types
of
tautologies
just
catches,
only
the
simplest
types
and
I've
chosen
to
present
them
to
you,
because
they're
the
easiest
to
explain
in
a
20
minute
slot
they're,
actually
more
involved
checks
that
try
to
to
to
cover
more
and
more
cases.
We
don't
cover
all
of
them.
Currently
it's
an
ongoing
effort
in
sartora
or
in
full
verification
at
Large.
A
Maybe
it
was
not
clear
so
I'm,
just
gonna
say
something
simple:
the
removal
of
all
the
preconditioning
operations
is
done
automatically
by
Satora.
It's
an
automatic
check.
So
in
that
sense
it's
not
harder.
So
if
I
understand
the
question
correctly,
you
say
how
can
I
fix
it,
which
part
of
this
statement
causes
it
to
be
a
tautology
and
that
it
indeed
sometimes
more
difficult.
But
it's
something
that
you
can
do
systematically
say.
A
Your
expression
is
an
or
expression
you
can
check
each
part
of
the
or
independently
and
see
which
branch
of
the
or
is
something
that
is
always
correct.
If
something
is
always
correct,
it
means
the
entire
statement
is
always
correct.
Therefore,
this
thing
causes
ubiquity,
and
this
is
actually
a
feature-
that's
very
close
to
production
in
sartora,
maybe
I'm
wrong.
It's
already
in
production,
maybe
I'm,
not
so
so
keen
on
the
details,
but
it's
really
close
to
production.
A
If
you
have
an
implication
same
thing,
you
can
see
that
maybe
the
premise-
that's
the
part
before
the
arrow
that
comes
before
the
conclusion.
If
it's
something
that's
always
false,
you
will
have
a
rule,
that's
vacuous.
So,
depending
on
the
structure
of
your
conditions,
you
can
learn
more
intelligent
things
about
them
that
can
guide
you.
It's
still
not
perfect,
but
this
is
something
that
we're
actively
working
on.