so so the panel is about smart contract
security and one thing that's been
talked about a lot recently is formal
verification so if we start off with
that do you think that formal
verification is going to be a new tool
in the like developer tool chain that's
going to be commonly used when
developing smart contracts what's your
take all right so I worked in formal
verification for almost four years
before I joined IC 3 at Cornell and I
think formal verification is really in
the broader community finally getting to
that point where it's reaching
acceptance and the tools are reaching
the level of maturity that makes them
actually practical so yeah I think
formal verification is really going to
be one critical piece of the overall
security picture yeah like I said in my
talk yesterday it's really not a silver
bullet but I'm really looking forward to
using etherium and the smart contract
space to set the standard for how formal
verification should be done in the
broader software development industry
and even in the safety-critical domain
so I think we have a big opportunity
here to show people how it's done really
so and you think that so it's not only
going to be for the specialized
contracts but more for in general people
are going to do formal verification is
that going to be the developers moving
over into the form of verification
domain or are we going to have tools
which make it's more easy to formal
verify your your contracts I think we're
gonna have a little bit of both and I
think it's up to the users of these
contracts to really demand the standard
and the level of rigor that's
appropriate for the amount of money
that's going into them I think having
low effort automated tools is really a
great goal and is something that I would
personally even like to contribute to in
this space and I think that will be
great for many many contracts but when
you have really really high value
contracts I think we will need to have
some sort of specialized approach where
we bring in experts and we asked quite
about what is this contract actually
doing and how can we make sure it's
doing what we think it's doing so yeah I
think to answer the question it'll be a
combination of both general automatic
and specialized approaches and it really
depends on how much money your contract
is handling and what the attack surface
is and other factors like that and I
would add to that that the tooling is
going to be a critical component because
a lot of the developers that are coming
in and developing contracts are coming
from the app development space so if
you're building web apps or mobile apps
you're not used to these kinds of
requirements and truly smart contract
development is much more similar to
writing software to put a shuttle into
space or writing software for safety
medical devices you're writing software
that handles millions of dollars
potentially so the kinds of security
requirements are closer to those
applications and a lot of the DAP
developers are not coming from that
space so a combination of tooling that
automates a lot of the formal
verification and then also education
just as a process to bring developers up
to speed with here's the domain we're in
and here's really what the requirements
are to produce production apps
yeah and I think a lot of that is gonna
come from the user side as well we
really need to educate users and make
them demand the appropriate level of
rigor for the software that they're
using I know people are putting lots of
money in contracts right now that don't
even have tests and that's like really
the bare minimum in terms of software
engineering so until we educate people
to sort of what's possible and what the
tools exists to do I don't think we'll
see much improvement so there definitely
needs to be a push on both the developer
and the user side in terms of these
tools not just a matter of educating
users I think the other thing that we
can and should be targeting is like one
one two three four can reform only the
RF I use microphones next time at six
seven eight nine
what I was saying is that I think it's
not just the users that we should be
targeting here I think it's also user
facing intermediaries so like one good
thing from that standpoint that has
already happened is just the fact that
quality Explorer is like either and have
code verification and now check if you
would see a contract saying might be
disagreeing interacting with it actually
codes it's you can check this source may
verify the source actually matches the
byte code you could see something like
that potentially being expanded quite a
bit you know including you know check
marks for like what kinds of form of
your vacation guarantee is this it's
passed are there any tests that it's
faster we tested it failed and so forth
so I know grain you've been developing
some tooling for solidity and so when
we're talking about tools
what kind of more tools are needed in
this space well there's a huge range and
I think it's useful to have both the
tools that are offering rigorous methods
of completeness and the academic work
and the research is really essential to
that but you can get a lot of value out
of heuristics as well and you know
things that are rather obvious now like
the reentry attack on the Dow maybe the
particulars of it weren't obvious the
spot but the particular attack of having
a recursive call from an external call
is quite easy to spot and so it doesn't
take a very heavy-duty approach to be
able to detect those things so the
tooling can range from the more rigorous
to just some simple sorts of analyses
static analysis is a great tool to be
able to just detect things that are
potential areas of risk so I think that
can go a long way towards providing
people more visibility into contracts
and if you know that you're looking for
risks then we can devise tools that
highlight that and expose where the
potential areas are and that can be a
low that can be low investment you know
you don't have to do a full security
audit
first as a first step you'll want to do
it later but as a first step if you can
run some tools that provide some
indications of where to look for
security vulnerabilities that offers a
lot of value for low-cost and and I
think that stuff should be in the
compiler like in most high-level
languages you have that kind of basic
static analysis already built into the
compiler and there's no reason we
shouldn't be doing the same here the
only caution that I would have is being
careful not to just run sort of all the
low effort tools and then call it a
solve problem and put a bunch of money
in the contract because that's something
that happens inside of the corporate
space and even in high assurance
software all the time where people will
run a few tools and then assume that
they have assurance that really isn't
there so so when we talk about smart
contract security often you talk about
only from the developer perspective but
and is easy to forget that there's also
a user perspective so what what how can
we make it more secure for end-users to
interact with contracts which may or may
not be hostile or backdoored or flawed I
think like there's always going to be
like a little puzzle so like earlier on
I mean I mentioned black explorers one
other possibility is that figure out
some kind of what kind of walls or what
kind of things should be integrated into
something like a mist um then of course
there's a question of exactly what kinds
of things do you get integrated so but
if it's formal verification checkers
then like one question is what exactly
if you are flying because it's easy to
write a contracts where what if you're a
malicious developer or you write the
contracts and you also just like write a
bunch of weird why three statements and
it looks impressive and looks secure but
in reality the why three statements are
like missing something that's actually a
backdoor
so there's but that's part of it but the
the other part is even just things like
security auditing and even saying you
know I mean this particular contract has
been audited by like these particular
people this particular contract matches
some particular time
yeah I think this is this is
fundamentally a UX problem and we should
take inspiration from the work that's
been done in browsers there's been a lot
of work about how to securely browse
websites and there are a lot of
parallels between that indie apps well I
think are the security model that we
have here that we're trying to achieve
is definitely a bit stricter as we're
saying that it's the job of mystic even
to protect the user from number one bad
contracts number two bad interfaces to
good contracts we don't even trust the
source or the JavaScript this is Sarah
Lee and and then you know if you have
good contracts and you know you have
good JavaScript on top of that there's
also built-in user access control which
is you know something that we can have a
catalan all by itself so if you make the
comparison to to for example the web and
just browse the internet with with
google chrome you have their blacklist
approach where they tried to access
something which is known bad and they
alert you so do you see that as a
possible way forward or more reputation
about reputation systems for known good
contracts financial services you know as
far as reputation systems go reputation
systems go like the two are sort of flow
into each other like a blacklist as a
reputation system with a default this
euro and can go negative and the other
one is where the default is euro one can
go positive and I think both approaches
have their merits so for example I think
there are there are some kinds of white
whitelisted that do you make sense so
for example if you are accessing some
particular application and then the
application all of a sudden decides
stoical force your accounts to call to
do a call to some people you look
unknown address with a large amount of
gas and a large amount of data you might
want to make sure that be concerned that
maybe that call is like actually
stealing all of your maker coins or
something similar and so I an approach
that explicitly asks for your permission
if it's outside of some way whitelist
might be a good way of mitigating that
me and well if there is some like a
known black quest then that's something
I am you could provide like you've even
stronger warnings about so it's
it depends on what it is that you're
blocking and it also depends on sort of
what the consequences are of you know
something being outside of the whitelist
or inside the blacklist and I do think
that the web access control on the web
is a good good comparison from a UI
perspective and the industry's had to
deal with how do you communicate to
users that this is a risk but a
particular type of risk so the same way
that you would download an app and they
would ask permission to use a camera you
know if you flood the user with too many
of those warnings you just entrain them
to click ok and but if you don't provide
the correct access control for the for
the correct types of operations then
then the security is worse so I think we
do at least from a UI perspective we
have a kind of comparison and like how
do you create something for the user
that is both simple and provides those
the the robust robust security measures
against things like sending lots of
ether or whatever there's also an
opportunity for some of the existing
early adapt development companies in the
space to set a standard so what one
thing that we don't want for example is
a situation where it's just like an
accepted defaults to like ask for every
single permission Under the Sun is what
to do that then you just work with the
value of this is the place but if on the
other hand you know a lot of
applications are designed in such a way
that they use flow nicely with the act
with the security and access control
that exists then something that doesn't
sort of fit those patterns would be
would actually get looked at much more
suspicious to me which is what we will
I'm gonna ask a direct question so in
the as of today with the languages we
have if you want to ride secure
contracts is it possible to develop a
secure contract without knowing pretty
much in depth how the VM works
underneath the language level the quirks
nothing of any complexity I'd say I mean
if you have something very simple that's
following an established pattern sure
but if you're going into some new space
then yeah you should understand how the
internals affect your contract or have
someone look at it because you know
ideally I think we'd wants to reach them
reach the stage where like the language
is intuitive and like the limitations in
the VM layer don't really yeah look it
cause any quirks that are sort of
unexpected that don't appear at this at
the solidity level itself but at the
same time we're not quite there yet so
look we have thing you know we have
things to worry about like gasps we have
caustic limits that we have we have
stack limits so there are a couple of
ways of attacking the problem so one of
them is modifying the protocol to try
and reduce the number of those limits so
like I have an EIP out there that
basically gets rid of the call stack
limited basically replaces it was like a
gas based limitation scheme another
thing is to basically just like to put
more checks into the development
environment so if for example you have
code where you can't like let's say
formally verified that they consume is
like less than I've seen a safe amount
of gas and that's something that should
be more closely and look those are
things where we can't have a tool where
we can't have supposed to highlight so
I'm gonna draw on an analogy to safety
critical systems here where if you
really want to build something that's
going in a spacecraft or something like
that you still have to consider the
hardware and you still have to consider
the assembly representation and you
really have to consider at least the
whole stack so I don't think you'll I
think maybe eventually once we really
develop these tools you'll be able to
have some sort of ignorance and
abstraction of those lower levels but I
think it's gonna be years personally do
you think that the development of new
domain-specific languages for certain
types of
or contracts in general would aid do you
think that's coming that we're having
more languages because earlier we had
there was development both in solidity
and serpent and for that part LLL now it
seems that solidity is the leading the
race and is almost the canonical
contract development language will there
be more well I can speak from my
perspective that I I hope there will be
more because the language a language
like solidity that's fairly high-level
is our main abstraction layer over the
EVM so as developers we spend more time
writing smart contracts in that that
abstraction layer and so to the extent
that the abstraction later layer
supports good security practices that's
going to help the whole community right
more secure contracts and right now I
think that the the convergence on
solidity is helpful to create stability
in the community but we really do need
other languages and other abstraction
layers not to necessarily find the
ultimate one but too similar to the to
the web community to have more
experimentation and have the ecosystem
naturally evolved these different
abstraction layers so yeah I personally
I would love to see other languages and
you know the EVM C and JIT work that we
heard about yesterday is really exciting
in order to open up that the the
platform so I'm gonna play a little bit
of devil's advocate on this I don't
think good languages can solve bad
programmers and I think that as long as
you're having a turing-complete language
that has expressiveness you're gonna run
into problems of some sort with the
language and I do think that having a
small number of diverse languages is
better than having a very large number
of languages because then you have more
people in the community who can
understand the language really well and
sort of audit your code so for the web
it's a great example you mostly see
JavaScript really in practice for
client-side computation and even though
it's not the greatest language people do
understand it and they sort of
understand the common anti patterns and
that helps them write secure code in
many cases to use your own example
however the transpilers
that have taken off in the last five to
ten years in the JavaScript community
have allowed the community to test es6
es seven features before they're part of
the core so that's like this bottom up
contribution to the language and
evolution so it's not just the tc39
committee that is bringing the language
changes from the top down
they're certainly helping to add them to
the language but there's this bottom-up
effort from community members and
transpilers and so it just helps inform
it from both sides so I would agree with
you that I'm having the kind of core
language offerings and having people
develop expertise in that language is is
the primary concern but then if you take
a step back and look at the ecosystem as
a whole and the evolution of the
patterns and abstractions and languages
they're available having multiple
sources of experimentation and evolution
I think really helps totally agree all
right the topic one last question do you
think there are any particular features
of the EVM or new uploads or changes to
the EVM which could be made which could
improve the security in contracts one
thing that I really don't like about the
EVM is the lack of distinction between
calling a function sending money and
sending a message I think there should
be some ways to access more restrictive
subsets of this functionality where
maybe you only want to send money and
allow other contracts that you're
sending money to to perform only limited
operations otherwise fail so I think
maybe that that architectural concern
could use some work but in general I I
don't think so I think there's a lot
more work to be done at the higher
levels than at the EVM right now I have
a few specific proposals or like one of
them is look as as I mentioned replacing
the cost the cost at replacing the cost
element was with gas one of them is the
call static proposal where he can make a
call so that which can record as much as
it needs to Anam
any state changes and a few others and
you know I think we can meet good
building blocks Ike and there are
different creative ways of high-level
languages vary but in general like the
impression I've gotten is that it's much
more about these sort of incremental
additions than redesigns all right I
think we're running out of time is that
right thing yeah so thank you guys thank
you