zkSummit - Lightning Talk: Martin Lundfall (Maker/Dapphub)

Transcript

thank you very much [Applause] let me just unlock my computer and we got some slides and I wanna get to the little demo I'm gonna be doing at the end of this talk so I won't take a ton of time to explain the context of what I'm doing I'll just tell you that we're doing form of a formal verification of smart contracts so using the semantics of the EVM that was written by the people at runtime verification and the University of Illinois in urbana-champaign which is a complete

semantics of the EVM it passes all of the VM and general state tests and it has symbolic execution and so it's really nice to do reachability proofs which is what we need to do when we do formal verification but in order to do formal verification we need to actually verify something so we need to have some sort of notion of what it is what properties we're interested in in verifying when it comes to smart contracts and for that we have developed the tool we add a pub called Caleb which does primarily two things it allows you to specify in a neat format what you

actually intend your contracts to do and then it calls the kay framework prove err to verify that this behavior actually is implemented in your contract and then Caleb allows you to step through these proofs which are basically execution traces with symbolic inputs and see how things are going and if they went wrong what happened it also does gas analysing for pretty much all of your contract behavior so it will keep things abstract as much as possible and generate a bunch of specs that you can analyze the gas behavior for your various functions of so here's

the specification format the recall act so we see a simple token contract and like 15 lines here and we're interested in verifying the transfer function which just a you know I think you know what that transfer function does so here is the behavior implemented or expressed I should say in the Act language and the interesting part here happens in the storage location where we refer to this tok this storage entry which is the balances mapping and we refer to the

particular entry from the caller ID and we give it some abstract value that it begins with and then say that this value is going to be reduced by minus value and all of the variables that we see here are real integers so in order for this to be true we need to make sure that they actually don't overflow or underflow which is what we say in this if and only if condition so from this we generate a couple of specs we take the if and only if block and we generates to split two specs where we assume the conditions to be true and one worthy we assume that B to be false and then if

there's an if block present we assume them in both of these cases and in the end we get three specs that are relevant to the execution here we do a gas analysis of the first time around here we have like a rough estimate of how the function is going to behave but we don't refer to the gas in a specific format so let me show you what this looks like if we have a proof like this so I pre run the execution so let's begin by debugging the the passing functionality so it it shows that this execution took three thousand steps

these are not 3,000 EBM steps they're actually slightly smaller and I'm gonna tell you why in just a second but here you would have an interface that is familiar to you if you've used any debugger where you can step through you can have the source map to see what's really going on and the thing that distinguishes this from any other debugger is that now you have these symbolic values on the stack and they're going to be constrained in some manner you can look at what the constraints are and see that they lie within the range of an you int 256 and you can step through to the end of the execution and

you can do a bunch of stuff so that's kind of cool but let's look at the fail case so as I said we have another spec that takes care of what happens here and this one is slightly more interesting because it has branching mean we can press B to look at the behavior and now since this is a fail spec it's gonna end in a bunch of reverts at a bunch of places so if we go to the case here this is when the from Bal is smaller than a bi value which in this case we should of course revert because we don't have sufficient funds to do this transaction

we see that if we step through here we actually end in their virtual opcode which is what we asked for in the fail specs so that's kind of nice let me show you something else what we also have if we forget about the behavior for one second is that what we're actually doing here is that we're not only stepping through EVM steps but we can actually look at all of the things that is being handled internally when we try to execute an opcode we want to make sure that the stack doesn't overflow that it doesn't violate whether we're doing a static execution or not and they're reloading some necessary data and then

we're actually calculating gas of the arc code and we're checking whether memory is incremented that we need to check what particular flavor of the VM we're running and we do all of these things so in the end you know it takes maybe seven steps to go through a single opcode and this is really useful especially if you have some malformed code or something and you actually run into some some stack overflow or some more internal errors of the VM now this rarely happens with well compiled code but if your compiler is broken for example this can happen so I think that's all I'm gonna display in

the demo we're working on a bunch of CI right now so that we can automatically take whenever we've updated the the bytecode we can run it against our specs make sure that we didn't violate any of the behavior that we have specified and really doing most of the work right now to make sure that our specs are really exhaustive and cover the complete behavior of our smart contracts and make sure that everything that can happen is actually specified in our contract there's a couple of fun things that you can do once you have this you can you can sort of forget about the implementation and say that the specification is actually what defines your your decentralized application and you can start to optimize for gasps you

can rewrite your entire contract and huff for whatever you want to do you can have also like a bug bounty on the specs so you can say like these specs actually define the behavior of my decentralized application and if you manage to write an implementation that satisfies the spec but is faulty and some you know magical sense then you know we've screwed up in writing these specifications and you should get some credit for that so that was all of the slides that I had so do I have some time for questions nice

questions you said that the specification could be your application but can you sit the size solidity from the specification or do you have to keep maintaining the solidity as you change it so in in the general case like you can specify things that you can't reasonably implements since what you're really doing is like the specification is a little bit like a theorem and the implementation is like a proof for molera fication is a little bit like jeopardy like somebody gives you a question and somebody gives you an answer you need to ask the question of

it so like of course there are things that you can write in the specification that are going to be really hard to find an implementation of but with most reasonable applications you would be able to generate an implementation from it presumably and this is something that we have thought a lot about doing and it would be really nice to get a get out a VM bytecode from the specification language thank you any other questions hi this might come across this might be a really silly question but so from the sounds if you have a formal needs like if you have a specification for your smart contracts

that passes tests then just that kind of the the problem move from how do I put this there's no way of liked and systematically evaluating the control flow of your program to determine if the specification is complete is that because I'm guessing that's impossible well it depends on the particular contract that you're evaluating like if it's a complete orbit rarey piece of code then then of course is gonna be impossible to evaluate but in the most reasonable cases we have some fairly finite state machine that we're interested in describing and then we can actually reach exhaustive Ness thanks

all right let's bring up our next speaker and thank Marty here [Applause]