so hi everyone my name is Rita twinkler
I'm the chairman and co-founder together
with Mona Lisa of Mellon port and Marcin
advisor to the web 3 Foundation so great
so let's starts with formal education so
formal verification is the act of
proving or disproving an algorithm with
respect to an Intendant underlying
algorithm so this algorithm is specified
in a in a formal specification so I'd
like to ask all of you what makes a good
specification what makes a good
specification that's a good question so
I think theoretically the the answer is
that the specification accurately
captures the intent of the developer who
wrote it making sure that's the case is
obviously very difficult so I think a
lot of that depends on sort of your
tooling and the feedback that it
provides when you're writing the
specification but in general I'd say a
good specification accurately reflects
the intent of the developer and also
encodes sort of all of the assumptions
that the smart contract makes very
explicitly and very clearly so that if
someone were to update the smart
contract later or something they would
all be very nicely in the same place is
going to add a little bit more I think a
good specifications to be easy to
understand and to be easily to for other
to you know read and you know built ask
a little and it's clearly you know it
follows some standard as well I think in
general any specification is better than
what most people do which is no
specification so that's probably a good
place to start ideally you'd you know
write a specification and then argue
over that for a few days at least and
then you know write your tests and then
the encoding but a lot of people kind of
do it maybe in the reverse order or
something like that
maybe they never even read a
specification so please answer captures
it but maybe a good specification should
put contract in bigger picture what kind
of game people can play on it what would
be the well-paced
strategy for rational players and so
yeah if a specification fits into this
script economic mechanic game a
theoretic reasoning that something nice
but the yeah this depends on the
application Thanks
so so what is your take on a
specification kind of you know specified
kind of abstractly
with formal methods of mathematics Bosch
versus specification implemented for
example in Haskell so I mean one is kind
of like a reference implementation in
Haskell and the other is just kind of
abstract like purely theoretical well I
think that a reference implementation in
Haskell is a perfectly fine
specification honestly I think a lot of
people when they think of a
specification think of kind of just an
English language document or something
like that but at least in our group we
focus a lot on executable specifications
so I think you know a Haskell
implementation you know that's a whole
lot hell of a lot better than no
specification once again and at least
you can test it right you can you can
run tests against your specification
even before you go to implementing the
final thing so that's that's already a
huge huge advantage over an English
language specification for example but
certainly English language
specifications are easier to write so
maybe you start with that and then do
the Haskell or something like that yeah
I totally agree with everything that was
just said and I sort of want to add that
you can have good or bad specifications
in any format so absolutely while it's
nice to have a specification be testable
and clear and readable you can have
really really good at Haskell language
specifications or you can have pretty
bad Haskell specifications and I've even
seen English language specifications
that are not entirely
so sort of goes more to the expertise of
whoever's implementing it I think great
[Music]
so like could you maybe share a bit
about what is like new and unique about
formally verifying smart contracts
blockchains
kind of compared to you know safety
critical hardware verification and what
are the corresponding opportunities of
it you know what is new and unique about
formally verifying smart contracts or
blockchains compared to like for example
verifying hardware and what are the
opportunities of it I guess smart
contracts has a new sort of play
semantics right so we have a concept and
action at the conservative gas and solid
token heater which you know doesn't
exist in in you know existing system
like you know critical hardware or
software system so when you really
formally verified I think you you need
literally find new property that you
want to verify that only exists in you
know smart contract and also it Orion
there's definitely some really nice
things about smart contracts they are
bounded in terms of their execution time
there are generally very small simple
programs at least compared to something
you'd see in a safety critical system a
car or an airplane or something like
that and they directly handle large
quantities of money so actually I'm
really excited I think that I said this
last year and I still strongly believe
it that as a space we have an
opportunity to set standards for how
software is developed even beyond block
chains and smart contracts because I
think the users of smart contracts and
block chains have a much stronger
understanding and demand for this kind
of technology than the users of a car or
something like that so it's room torture
machine has no non determined behaviors
no not defined behaviors because that
means consensus folks so
so this possibility of different clients
following different folks is a huge
problem but it's really bracing for us
on top of the virtual machine because
that means the specification is really
always deterministic that's a huge
improvement over proving anything over
intelligible so our cheapest Thanks
pretty much agree with what people said
the non determinism makes it easy to
bound it gas makes it kind of nice
although sometimes it's hard to reason
about exactly how much gas the contract
will use and basically you know what's
making the most driving force behind
this is the amount of money being at
stake essentially as opposed to just
normal programs in other settings let me
move over because a course really equals
to make it really hard hard for me to
understand the question yeah it's it's
kind of interesting how people care a
little bit more about money than their
lives right you have someone lose their
fifty thousand endow tokens and they're
clamoring for formal verification but
then Toyota has an issue in their ECU's
that kills 20 people and Toyota
customers could not care less about the
software in their car so I just think
that's kind of an interesting
observation on humanity it is kind of
interesting yeah right so could you
maybe talk a bit about the limitations
and challenging challenges so for
modification and maybe also like
introduced the project that you're
involved with and how your project kind
of tries to make things easier or better
so my background the interactive theorem
proving is not user friendly so take
class of computer science students of
thirty people maybe a couple of them
willing to use interactive theorem
provers maybe only one of them can
finish verifying a program of like 2030
times
in the month also so it's kind of
challenging actually verifying software
using these interactive theorem provers
is so challenging that I don't see much
I don't see many successful applications
so but for the reasons described before
I believe in a theorem it might still
make sense I guess you know it's really
hardly to formally prove you know
existing smart contract especially the
complicated one because you know first
of all you need like to represent them
in some mathematical model that you can
easily prove some property later on but
you know it's really hardly to you know
you know convert or transfer or you know
interpret the program into the new
language or the new model because of the
you know compare compatibility issues
right and also sometimes you cannot even
explore all the possible
you know outcomes or in properties of
the program and you know most of the
formal verification true requires you
know a strong background and and you
know human involved right and most of
the project and companies do not have
these you know people so so you know
we're really like we we need like some
sort of like you user-friendly developer
tool so that you know you can just like
run the tool with some existing smart
contract and it will produce other or
the headphone output for the developers
Thanks yeah so I work on sort of a
number of projects in the correctness
space one of them is I'm advising this
sort of heavier weight formal
verification project called KVM I'll let
Everett describe that since he's
actually the lead but to speak to the
broader point I think there's like a
very wide range of correctness
techniques that we have here both formal
informal and semi formal and another one
of the projects I'm on Hydra is sort of
a lighter-weight approach to this where
you abandon full formal guarantees for
sort of low cost and easy startup which
i think is a very valuable thing to a
lot of companies who aren't going to be
able to as Lowe said hire the right
people or have the right expertise at
the end of the day formal verification
is still super expensive it's still hard
to do and it still doesn't give you
perfect guarantees so it's
understandable why for a lot of people
especially now that the tools are not
totally mature the business case sort of
isn't there so I think we need to
develop a range of techniques and ask
ourselves what are really our high
assurance contracts here to use our full
fledge techniques and how can we get the
other ones to a better level of security
with like the lower hanging fruit
techniques you know I think I agree
pretty much with what Phil's saying here
and actually it makes me really happy
that I see so many people just
emphasizing the importance of testing
and of writing specifications because
just those two steps alone forced you to
you know first clarify in your head what
is it I'm trying to do which so many
people don't even do they just sit down
and start kind of clunking away at code
and then second to kind of conker ties
that by writing some tests and then say
like is what I did actually you know
implementing these these tests so the
test kind of serve as a semi
specification if you will or
concretization of the specification
regarding the KVM project that Phil
mentioned you know I think it helps with
the entire you know there's the entire
range of verification that you can go
through right you can start at testing
and you can move up to some sort of
runtime verification or runtime model
checking up to model checking which is
where you explore the whole state space
of a program and then up to theorem
proving where you use more advanced
techniques to prove that a program is
behaving correctly and K gives you tools
for all of those things actually so I
think you know KTM can be a useful tool
in that space it doesn't have quite a
nice user interface unfortunately so it
suffers from that but I think it can
help a lot in in all those areas Thanks
so it seems like a common theme seems to
be it's like too complicated so so how
can we make tools and/or how can we
develop approaches or more accessible to
the end-user I think in the end it's not
reasonable to expect the end users or
users to read logical formulas or maybe
K configurations are more accessible but
it's hard so at the end what we want is
sure that can synthesize an advisory
based on the unproven goals this
scenario can happen and it can play it
may be not an animation but like it
should look like somebody attacking you
your contract that would make the
problem much more easier to understand
so I guess if stability is always a hard
problem right and that's also like one
of the motivation that why we build
buoyant e the smart contract analyzer
based on symbolic execution so the idea
here is that you know user they do not
need to understand like how authentic
works
they're only need like to paste the
smart contract into Oyen T or into the
you know web browser and they click
analyze and we can just like show all
the possible vulnerabilities that
orientation can figure out yeah I
personally think demand sort of breeds
progress in this direction and we're
sitting in a room of some extremely
smart and talented people and we've seen
some projects that really push the
envelope in a number of spaces and while
the tools are hard to use and there
certainly could be improvements made
there nothing here is sort of magic or
anything like that so I think
sufficiently motivated developers who
are incentivized by the market to
develop these tools is really what we
need to push the the envelope here
another thing that I think is really
helpful and I'd like to especially
congratulate melon port for taking this
approach is to take these things out of
academia and into industry and use them
on real contracts with real developers
who are working on the ground in
solidity I think just that step could do
a lot for usability
and academics are not really the the
greatest at writing super useable
systems sometimes so more more broad
participation would definitely help yeah
if they're 13 that in just 30 seconds it
but yeah definitely the the approach
that that mellon port is taking seems to
be the correct one just make the tools
usable and make them have check for some
some specific properties automatically
certainly all the verification tools can
be instantiated to do those sorts of
things but you know it takes effort and
takes developer time it takes people who
know the tools to do that instantiation
and that's not going to happen overnight
so you know these lighter-weight methods
like fills hydro stuff that's really
gonna be the stopgap until we can have
better tooling for all these you know
high assurance tools so the last
question from from me and then opening
it up to the audience is essentially a
shout out from you guys so but what
would you like to see come from
different ecosystem players so from from
the users developers investors the
project leads and researchers to make
formal verification mainstream in the
current ecosystem I think it's to the
users responsibility to make sure that
they understand the contract they are
interacting with some people people are
like proposing markets for audits and so
on but it is not working yet so actually
I have to repeat Martin I mean it's fair
to say this but you have to be it a byte
called
learn the VM in order to make sure that
you are interacting with busines brew
thing it's sort of Sadie's but it's
something like that currently and then
yes something like audit market with
reputation system
something like that very gradually
improve the situation but yeah now due
diligence is required for all parties I
believe so I see there as sort of being
two pushes that need to happen one of
them is bottom up the users need to
really start demanding that if there are
techniques available to ensure the
correctness of that kind of their
contracts they're either used or a good
justification is provided for why
they're not used We certainly have a few
tools right now we've seen presentations
today about quite a few of them so so
users really need to start being more
selective about where they put their
money and well sure it's tempting to
sort of buy into every single ICO and
flip it for 2x or whatever that's not
the kind of space that sort of
incentivizes and fosters rigorous proper
software development and so I think
users and investors need to become more
selective and and developers need to
sort of enable them to do that by really
going through the processes in a way
that's serious and in a way that they
put in a concerted effort to get the
maximum assurance out of their contracts
Thanks
yeah kind of echoing what you said a
little bit you know no amount of money
as a substitute for just understanding
right so at some point you just have to
read and understand the bytecode and
understand how EVM works and understand
hustle it D compiles to EVM or whatever
tool it is whatever high level
programming language you're using how it
compiles DBM and what the implications
for security are in that setting and you
know the people doing security audits
they understand this really well and
they like they were saying earlier you
know they just read the code and read it
again and read it again and read it
again you know there's no substitute for
just putting time and effort into you
know high assurance software well I
guess you know in order to make formal
verification popular I think we need to
adopt this first right so I mean I hope
that we can have some sort of like ERC
that you know that allows you know
people to put you know maybe orientate
half Hydra attack or you know KETV on
tap into every single smart contractor
has
Ben you know deploy in the Italian
blockchain Thanks so anyone from the
audience would like to ask some
questions yes maybe it's better if
people with questions should come to the
front that's probably a good idea for
the next person so from an artist
standpoint how would you like to see
people who provide smart contract audits
either contributing to your projects or
using your projects I assume it's sort
of maybe one or the other but maybe
there's both for us right now does that
make sense yeah I do do some smart
contract audits and I would say ideally
the role of these kinds of tools in the
long run would be to sort of put most of
that business right now out of business
to an extent like at least that's my
personal go with it in all my audits I
always make recommendations to the team
about which tools are state-of-the-art
and what they should be running on their
contracts certainly auditors can run
these tools on the contracts as well but
at the end of the day my personal
opinion is that it's the responsibility
of the team and the team to sort of seek
help when they're not able to do
something like this especially because
you know most teams are would not be
willing to sort of pay the hourly for an
auditor to run security on their code or
whatever when they could do the same
thing themselves so I think the role of
auditors to answer your question is to
sort of inform the team about what's
available and what they think could be
useful for the contract and then it's
absolutely the team's responsibility to
follow up on that and put the time in
often I think the hardest part is just
the spin up time right so you you have
some new tool that you're trying to
bring into your tool chain and then you
know it maybe takes a week or something
to get it fully integrated and get it to
be seamless but once you have that spin
up time taken care of then you can kind
of begin to make incremental progress so
what I would like to see is people
taking the case semantics and making
extensions of it so we have already
several extensions one is a small gas
analysis tool that's not very feature
full or very complete or sound it just
kind of gives a rough estimate
but it'd be nice to kind of tighten the
screws on that and then there's another
tool called EVM prime which is just a
small extension of the EVM semantics to
a higher-level language and if people
wanted to hack on that that would be
really cool I'm answering specifically
for KTM because that's you know the
project I'm working on but there's all
sorts of other analysis tools you can
write directly in K itself as an
extension language and the hard part is
the spin up time on K of course but you
know there's no there's no avoiding now
with a project like that so yeah just to
butt in just for one second it would be
really nice also if these auditors and
these teams sort of complained a lot
more about the tools yeah so so far most
of the research focused around either
talk or Krauser which are relatively
smaller size and they off also it's
quite similar but as more more companies
start delivering the product which they
promised today based on the funding the
sides gonna be a lot bigger and the
product will be quite diverse what would
be the challenge when it comes to
verifying these actual product rather
than I talk in the crowd sales this
quick answer because we need to sorry
the question was what are the challenges
for these teams that are using these
tools mostly it's better without the mic
actually I think
yeah yeah so so yeah that's a great
question so the question was about like
most of the verification right now is
tokens or crowd sales because that's
sort of what everyone is doing and it's
all the same but what about when we get
more complicated contracts I personally
think people are always going to sort of
push the envelope and do things that are
more complicated than we actually can
verify and I think that's really cool to
sort of feedback in but the more
complicated the more experimental your
contract is the more time you're going
to have to take and the more you're
gonna have to consult experts who really
know how to write like new
specifications and not just reuse those
same old building blocks in the old ones
I I think auditing make finding bugs in
the contract is a bad game to play
because you have to beat the best
articles in the world so going forward
if you try more complicated stuff you
will need much stronger usable -
otherwise um so I mean the game is not
fair you have to find the old holes and
a very good attacker should find only
one go one poor critical vulnerability
so it's very skew it's a very very
skewed game so maybe a good tooling or
maybe a good game like Hydra is
necessary but I think we are kind of
ready to that take the challenge rights
and thanks very much that concludes the
panel like to thank all the panelists
like it's a huge honor to share the
stage with some of the best researchers
in the field thanks very much
[Applause]
you