Panel Smart Contract Security in Ethereum

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