[Music]
all right hope everyone's doing good
today we're going to talk about writing
secure
writing
secure and correct smart contracts so in
particular I'm going to talk about some
directions and some problems we've been
thinking about in academia and I'll also
try to tie it into an industry
perspective for those of you who are
smart contract practitioners alright so
let's start out with who is IC 3 IC 3 is
sort of a research hub centered around
the universities you see they're mostly
Cornell University also UI UC Berkeley
Cornell Tech and the Technion we've got
12 faculty at the last count and we're
adding more all the time in the last
month we've added at least two or three
faculty and we've got many many students
at all levels of education
so before I start I'd like to give a
special thanks to the etherium
foundation for inviting us here and
putting in all the work to bring us
together and also to our industry
partners at chain digital asset and IBM
thank you guys very much for your
continued support of smart contract
research will also be announcing more
partners in the coming weeks and we'd
love to have you guys as a partner I
know there are a lot of companies here
who are interested in the correctness
and performance of crypto currencies
blog chains and smart contracts so if
that's you please feel free to check out
our website at an its e3 organ contact
us alright so here is the work that IC 3
is doing as far as we see it there are
five Grand Challenges in smart contract
performance
sorry smart contracts and crypto
currencies one of them is scaling in
performance the second one is
correctness third one is confidentiality
the fourth one is authenticated data so
getting data sources into these systems
and the last one is safety and
compliance which you've heard a little
bit about today so this talk I'm gonna
be focusing on correctness and its
relationship to security and how we
write your secure and correct smart
contracts so this is intended to be a
high level overview we're not trying to
be comprehensive here there's a lot of
work we're not gonna mention we're also
going to provide some suggestions for
practitioners since there are many of
you guys in the room writing smart
contracts and I'm gonna draw frequent
parallels to safety critical software
whether they be in planes cars
power grids or other infrastructure
systems and software like that all right
so we all know this problem pretty well
by now as a community the problem is you
have this software bug it leads to money
being lost or stolen and then people who
write and participate in the smart
contracts cry
so there are some things about this
challenge that are definitely unique to
the cryptocurrency and smart contract
ecosystem one of those is that security
is more closely tied to code correctness
than anywhere else so you have this sort
of problem that any issue in correctness
which leads to a fault or software bug
may be directly monetizable by an
attacker and these attackers can also
anonymously monetize these exploits
untraceable we've also got a unique
adversarial environment here so
everything that runs on these systems
from the miners to the node network to
the actors that participate in the
contracts could potentially be
adversarial and if it's not bad enough
already we're looking at public code so
in your car or in an airplane you don't
have access to the code that's running
to try to test it for exploits but on
smart contracts all code is public on
the blockchain all right so how do we
start tackling this pretty difficult
problem as far as we see it there are
three prongs here that will help us sort
of stick a fork in this problem with
smart contract correctness and security
the first one is formal verification and
specification the second one is escape
hatches or otherwise known as kill
switches and the last one is bug
bounties
so getting right into it we're going to
talk about formal verification here so
formal verification is probably the
hottest topic of these three in the
community right now there are several
talks going on about it at this event
and it's a really exciting space to be
in so what do we like about formal
verification well first of all I think
specification is a great virtue so by
rigorously and mathematically specifying
what you're building it helps you
understand the systems that you're
making on a deeper level also specifying
the lower levels this rigorously things
like the EVM and the languages that
we're using helps authors of higher
level systems know exactly what
guarantees they can expect from these
systems so specifications are great and
the more rigorous these specifications
are the better we can start to stat
start to tackle the problem of writing
correct contracts English specifications
are pretty common in the field these are
definitely not enough they admit
ambiguity you want an example of this
check out the ISO c11 standard which has
a whole committee whose job it is to
argue about whether certain programs do
or do not conform to the standard formal
specifications can also go further in
serving as criterias for Forks so the
question of when to fork these systems
could be answered by when the
implementation of the system differs
from its specification in which case you
have a very clear bug
obviously specifications also give you
these other side benefits they can help
us find bugs and they can help us
generate tools that we use to analyze
our contracts all right so let's talk a
little bit about the work that's being
done here both of these slides are gonna
have later talks on them so I'll be
brief one of them is this tool called
Oriente out of the university of
singapore i believe and what they did is
they took the semantics of the EVM that
was very nicely laid out in the etherium
yellow paper which i think is an
excellent document and a great way to
sort of set the standard for the rigor
that we expect from these systems and
they built some tools on top of it to
analyze the block chain to try to
discover bugs in smart contracts running
in the wild so I highly suggest you read
the paper I love the work that this team
did I think it's not perfect I do think
that there are many false positives that
sort of come with their approach that we
can further refine and get rid of as
these tools evolve so if you want to
talk more about this work you can ask
questions at the presentation that's
coming up later in the event or you can
find me afterwards all right here is
another great example dr. christian
right weasoner I hope I pronounced that
right with a y3 sort of back-end for
formal verification in solidity so here
you can see a very simple funds contract
and a specification over this contract
that was presented at the ic3 etherion
boot camp earlier and this contract
allows you to withdraw a certain amount
of shares and comes with the
specification that the number of shares
preserves the balance of the contract
so that was the wrong direction
so here's another contract that
satisfies this specification and this
sort of helps us illustrate that writing
complete specifications is pretty
difficult so if you're a trained
developer you're sitting here looking at
a set of specifications just like
writing buggy code there could be
something that you miss now this is not
intended to say that that this work was
intended to catch these sort of cases
this is obviously a trivial example but
the general point is anywhere you look
in the formal verification space writing
these specifications is extremely
difficult
so the gaps in this work specification
is hard some properties can't be
specified at all I'm thinking
specifically about properties of
incentives game theoretical properties
and higher-level properties of smart
contracts that are pretty much
impossible to specify often when you
have a proof of these kinds of things
you are trusting the tools that
outputted the proof which is not an
ideal situation because these tools are
very hard to audit and they require
significant expertise we don't even
really know how to audit them in general
a key takeaway I'd like you to get from
this is that any good tool must use some
sort of semantics that is a definition
of of the lower levels of the language
and the infrastructure on which they
operate so when you're trying to
evaluate one of these tools ask yourself
what semantics are they using how is it
audited and what guarantees do we have
that that system will actually conform
to those semantics right now to really
formally verify complex systems we need
experts we need multiple PhDs it's not
an easy problem and there are also some
famous incompleteness & undecidability
results that may suggest that gaps in
these logics could require more work to
achieve a robust system all right so
escape hatches
this comes out of the need of not always
being able to verify our contracts so
what we need here is something they
figured out very early on in safety
critical systems which is we need to put
a human in the loop at some point
it's true that the promise of these
systems involves in many cases taking
the humans out of the loop and I think
in many cases that can be achieved but
we shouldn't necessarily take that as an
absolute if verification or bounties or
the other two prongs of the approaches
fail it's important to have some sort of
failsafe or backup mechanism there are a
lot of parallels to legacy contract law
here so there are a lot of lessons to be
learned from how people have done this
previously in contracts and also
parallels to safety critical systems so
I'll pose the question to the audience
would you write a nuclear power plant
software that has no kill switch in it
probably not and I wouldn't want a multi
hundred million dollar contract not to
have one either so we've been doing some
work on this and I see three by Bill
merino here I highly suggest you read
the paper for more information since I
don't have much time to discuss it
and what we did here bill was a lawyer
by trade and got a master's in computer
science and he looked at parallels
between smart contracts and legacy
contract laws so he looked at all of
these concepts of termination rescission
and modification that are codified in
the law that have been designed to solve
problems that have come up in historical
precedents and he wrote little etherium
libraries sort of mirroring these
concepts in traditional contract law so
if you're writing a high-volume smart
contract I highly suggest you take a
look so this is again not problem-free
we've got a bunch of gaps in this
approach how do we verify that the
escape hatch code is correct what layer
do we put the escape hatches in do we
want escape hatches in the EVM which
would inherently be sort of less general
since you'd have a specific set of
hatches or do we want to put them in the
compiler which lets us save some
generality by deferring the problem to
the language or do we want to just say
contracts use well audited libraries of
escape hatches that you can modify as
you see fit giving us that full
generality so it's an open question
there's also a lot of potential for
abuse and escape hatches so
a bad actor could perhaps trigger an
escape hatch in a case where it's
profitable for them even if it doesn't
follow the intent of the escape hatch
that's something we always sort of need
to keep in mind okay so can you think of
a badly made escape hatch there is there
have definitely been contracts before
that have intended to provide a
mechanism for users to remove funds that
have then been abused to drain all of
the funds out of the system I won't
mention specifics but it's on line six
six six of the contract that I'm talking
about it's also worth noting that that
Forks of the system in general can be
viewed as an escape hatch whenever there
is a catastrophic failure involving
multiple aspects of the system you sort
of get the social consensus based escape
hatch that comes with the back end
architecture of these systems
all right the last prong of our three
three-pronged fork bug bounties so we
believe bug bounties are very important
because the incentivization structure of
developing exploits is pretty broken
without bounties so what do we mean by
this insecurity traditionally we say
it's never impossible to exploit a
system it can only be expensive and when
you have a cost of exploiting a system
that's actually much lower than the
amount that's to be gained from
exploiting it an exploit and an attack
will pretty much inevitably surface so
in order to fix these sort of issues the
general security community has
recognized the value of providing
bounties to incentivize people to defend
the system financially rather than only
financially incentivizing attackers
without them defenders are really only
motivated by ego or maybe goodwill which
as we've seen in the past are not really
powerful motivators to do the type of
work that's required for a full security
audit
so the good about bug bounties we have
the poor man's formal verification or as
we like to call it decentralized
censorship resistant anti fragile
incentive compatible crowd-sourced
verification you can tell that one to
your managers and I'm sure they'll be
glad to fund your escape hatch
development
all right so we got some cool work going
on in this space some of my favorite
work is the idea of using these
prediction markets that we're developing
as sort of Canaries for one an exploit
is about to happen because attackers
will naturally be incentivized to to
reveal this by taking a position on the
prediction markets in that direction so
that's sort of the more fringe work
that's going on we also have work that
directly addresses these issues in a
more traditional way so there's a blog
post by Simone de la riviere again I
hope I'm pronouncing that right on
medium called asset cards which I highly
suggest you take a look at that details
one potential approach for escape
hatches there's also escape hatches
mentioned in the etherium best practices
for smart contracts documentation and
there's a user called doubt challenge on
medium who's posted a series of really
small contracts that contain common
patterns and ask the community to try to
break these contracts in order to reveal
underlying language flaws or issues in
our coding practices that we haven't
really yet thought of
there's a lot more work going on in this
space if you google escape sorry bug
bounties if you're my bounty smart
contracts you'll come up with a ton of
stuff so there's a common problem in in
academia and in general that you have
all of these great solutions to the
escape hatch problem and all these great
proposals and you consider the problem
solved and I would urge you guys to
avoid that line of thinking because
there are still gaps in this in this bug
bounty approach so with prediction
markets there's always the question of
how to avoid bad incentives and how to
prevent incentivizing attackers and bad
actors from actually deploying their
attacks on the main end and profiting
there's also the hard problem of how to
create trustless bounties with trustless
payout we don't want to leak these
exploits to the test net because once
you leak the exploit to the test net
you've removed the incentive for
defenders and attackers can take that
exploit and deploy it on the main net we
also don't want to trust contract
authors to pay out because that
significantly harms the attackers
incentive to report the the bug if they
think it's a really profitable bug and
the contract authors may just invoke a
kill switch or fix it before they have
the chance to get paid there's also the
very very hard problem of how do we
define conditions for bug bounties how
do we know when an exploit is a valid
claim of a bounty we have a bunch of
academic solutions here sealed glass
proofs we have a paper about that on our
website that basically involves using
trusted hardware to deliver a proof of
an exploit without revealing the exploit
itself
SGX also leverages trusted hardware
maybe zero knowledge proof could be
useful here etc bug bounties are also
hard to do for subtle issues things that
I talked about before gain theoretical
issues or fundamental flaws in the
architecture of your contracts so like
our other two prongs they're not a
silver bullet
also I urge you not to forget
traditional software engineering test
fuzzing static dynamic analysis phase
deployment upgrades smaller test
contracts these are all very valuable
things I don't think I need to talk
about them pretty obvious how to use
them and I highly suggest you cover all
of these bases if you're writing a high
value contract alright so takeaways
we've got lots of work still to do here
the ecosystem definitely will develop
good formal tools we have a number of
talks on this think about humans in the
loops when you're writing your smart
contracts and use bug bounties as a
stopgap for verification and incentive
fixes
thank you guys for listening and if you
want to interact with us further please
check out our website at India c3 org
check out our publications and we are
always looking for industry
collaborations and partners we'd love to
work with you to solve the open research
problems in the space so definitely
contact us or find me somewhere if you
have questions about anything I've said
here all right thank you very much
[Applause]
[Music]