Smart contracts as inductive systems

Transcript

I'm at the etherium foundation of the formal verification team that was recently started in the summer last year and I'm gonna be talking to you about what we're doing and generally the state of formal verification of smart contracts as they are today and I have a couple of different alternatives for the title of this talk where I want to emphasize slightly different things so the first one which also became the canonical title that went into the schedule smart contracts as inductive systems is emphasizing this particular way of thinking of smart contracts which is particularly useful if you want to

reason about invariants of smart contracts that is behaviors of the smart contracts that persist across the entire lifetime of the contract another perhaps even more or equally galaxy brain sounding title has to do with the dual nature of specifications of smart contracts and with this as I will emphasize a couple of different times in this talk I want to speak of specifications as playing two roles as playing the role against which you check your implementation for implementation

correctness but also the fundamental building blocks against which you check for contract invariants or higher level design goals so in that way your specifications live on this middle ground where you can do a modular approach to formal verification up to them or up from them and lastly perhaps the most down-to-earth title is simply an update from the formal verification team emphasizing the aspects of this talk that that are more exploratory and that we haven't really fully figured out the appropriate way of doing everything yet but we

have some progress to share and this is what I'm gonna talk in about today so Oh another thing that I want to mention is that the slides for this talk will contain some links and some references that you may find interesting and since they are hyperlinks it's kind of hard to click them by just looking at this big screen so instead if you go to this URL you will be teleported to this exact presentation and you can click them on your computer or just follow along as you see fit so we begin with the question of what the appropriate way of thinking about smart contracts is and of

course there are many ways in which we can answer this question that may be appropriate for different domains I want to present two candidate views and then my own that that will sort of sandwich in between these two high level versus low level views so if we look at the coinage of the term when Nick Szabo was writing about smart contracts in 1996 he says that a smart contract is a set of promises specified in digital form including protocols within which the parties perform on these promises and I think this definition is nice in some

aspects specifically it emphasizes the protocol of interaction already keeping in mind that there will be different parties perhaps debating or engaging over different things it's quite close to a game theoretic view of a smart contracts and and the different moves in which players can make in that protocol so those are the things that I like another thing that I enjoy about this write-up is that Nick Szabo already mentions some attack vectors of smart contracts whether it be naive and ilysm where you are not really gaining

anything from destroying the smart contract but just wrecking it and rendering it unusable for other people or some form of incentive compatible breaches where you can personally gain from attacking it but if we want to reason about specific smart contracts I mean this is an overly vague definition and it's also somewhat interesting if we go into detail on this on this write-up that Szabo was doing is that stake or what these contracts are about the sort of value inherent to them seem to live beyond the contract he mentions that intermediate intermediaries must be informed about

the state or the past performance of these contracts and so they don't really seem to live inherent to them the way that we think of smart contracts in the theorem ecosystem carrying value in the contract itself so it seems like proof of stake for example would fit in this definition and that's not really an example that I would like to keep in my definition of smart contracts s I'm gonna use them for the context of this talk he also mentions an important precursor of smart contracts being the humble vending machine which I enjoy because vending machines are also used as a canonical

example in many mathematical explorations of let's say linear logic or different kinds of state machines that they're being used to model many different kinds of systems and they're also kind of nice so here's an example of an important precursor of a smart contracts being a vending machine where you can buy wigs for your dogs so on the other end of the spectrum we have a way more precise definition of a smart contract specifically of how we think of them in the etherium ecosystem from the yellow paper not verbatim but implied by everything that is being said there

where a smart contract is simply an address with non-empty evm code and it's nice that it's specific like we can say a lots of things about it we can clearly point out what is the smart content and what is not we know that it can be stateful because we have storage in contracts and and we can say how they update over time through transactions and whatnot but it's a little too specific in the sense that if you have two smart contracts with identical behavior and identical state they would still be different smart contracts just simply by living at different addresses

and so it's a little too granular for the purposes of this talk and it also doesn't really say anything about attack vectors so if you're a firm believer of this definition of a smart contract you may be one of the people who say say for example that the the DAO heart Fork attacker was not an attacker at all it was simply utilizing the protocol as it was specified so somewhere in the middle specifically for the context of reasoning about contracts and their security properties I like to think of smart contracts as stateful systems or

inductive systems meaning more specifically an initial States together with a finite list of stateful functions operating in a context of other state full systems another way of saying this is that there are inductive systems with each external function method an inductive step in this inductive system and I apologize someone confusing if we're using two different definition of functions in on one slide in these two different paragraphs what I want to emphasize is that in the first paragraph where I specify a finite list of stateful functions these functions are mathematical functions and so they have

one output per input and that they are stateful means that in order to specify the output of this function we need to specify the entire state and the entire input variables that are relevant to execution it's essentially to specify these functions we would need to say what the pre stated and what's the post status and however we may reach the post state the the algorithm by which we get there what I call a function method in the second paragraph is not really relevant to the definition of the smart contract yourself

we could have isomorphic smart contracts that are implemented in different ways but they behave similarly as inductive systems I'll go more into detail on that later but first the picture to keep in mind when thinking of a smart contract as an inductive system is something like this this is taken from Leo's presentation on the SMT checker at DEFCON 5 and it sort of already shows you this inductive nature of a smart contract as being first defined by its constructor specifying the initial state and then depending on the methods of the smart contracts or the external

functions available you have these different ways of updating its states but during that update always puts you back to the interface to the initial function selector of your smart contract where every transaction begins every function call to your smart contract will begin in the interface and so you really have this well let me show you this picture you have a tree of that unfolds in front of you with all of the possible states of the smart contract so beginning at the bottom you have your

constructor state and then walking down a particular branch of this tree is a particular version of reality unfolding on the blockchain but if you want to reason about the whole range of behavior or the whole possible states that your contract can be in you really need to consider all possible nodes of this infinitely unfolding tree which always have finite number of branches at eight point it's relevant because this is how we're later gonna be proving things about this tree okay so I'm going to say that in order to define a smart contract

we should we should define the initial state and we should define these stateful function of which it consists and to do that we must declare for each function how they update the state and if they have a return value what that is and so if you have done some some stateful programming in Haskell for example this is very similar to how you would write some muriatic function over the state monad you can also define the design goals of a smart contract and this is often you know where the whole

essence of your contract is being formulated so instead of specifying what it is that your contract is you can say what it should do you can say that there are some fundamental properties that define your smart contracts perhaps that the sum of the balances is equal to the total supply this is very crucial property of any of any toking contract you can say that you know there's some fundamental accounting invariant that should be true of your smart contract and these I will refer to as higher-level properties or design goals of smart contracts and they can also be

verified once we have this definition and finally we have the implementation of a smart contract which is writing an algorithm in solidity or in any other smart contract language even in an EVM bytecode if if you're leaning that way by writing these algorithms that satisfy these specifications and so most of the time we really have to sort of infer the definition from the implementation because most people ask they're writing smart contracts are just providing an implementation but then it becomes very hard to even say what its correctness

criteria is they sort of have to extrapolate some form of some form of implicit correctness criteria that is only in the developers head but if we have these specifications if we have all of the methods of the smart contract specified in terms of pre and post state then we can do a very complete notion of formal verification we can also do it in a very modular approach because we can verify both the implementation and the

design goals the higher level properties by considering how they relate to these specifications so to go into a bit more depth on the first point if we want to verify the implementation so to verify that the code that we are written in solidity or in the EVM matches the specifications that we have defined them our strategy is most of the time going to be symbolic execution or model checking and it can be done either on the source code level so on the solidity or Viper level there's mainly only formal verification tools for solidity right now when it comes to source code or smart contracts you will be needing a formal semantics of the

a language in which you're writing are smart contracts but then essentially what you're doing is demonstrating that the source code that you have written acts according to the specification and so some of the tools that you can use to do this is the built-in SMT checker that is built into the solidity compiler there's another tool called salty verify which is has forked this ability compiler and both of these work fairly well for some subset of things that you want to do but they assume correctness in the compiler because they're just

reasoning on the solidity level and so if you want to go deeper and you actually want to say things about how the bytecode behaves you need to have a formal semantics of the EVM and some tools that can help you do this is KBM or the kay frameworks definition of EVM or mythril material somewhat interestingly doesn't often deal with specifications at all they just sort of try to infer some correctness criteria from a large list of commonly used smart contracts patterns and common pitfalls associated with them and there's a whole

longer list of tools that I don't have time to go over right now but if you're interested in getting a more comprehensive view then we are maintaining a longer list of f:v tools at this repository so for the other type of formal verification when you have these higher-level properties or these design goals that you're interested in in demonstrating that your contract behaves according to your strategy for formally verifying that those actually hold is most of the time going to be induction with some extra steps depending on the precise nature of your

claim and here again we can split the concerns into two different categories where the most straightforward one is when you are correctness criteria is formulated in a contract in variance and this is a predicate over state variables so some formula that may contain some some state variables that remains true for the lifetime of the contract so regardless of which branch we walk down this tree this formula will always hold this can be further split into an inductive and non interactive a variance I don't think but I don't have time to go into those

details today but I'll provide a reference and then if you're interested in learning more about that but just for some examples I feel like there are not that many contracts that have formulated some sort of correctness criteria or design goal in this way so here's a few of the ones that I know for most I would say well-behaved token contracts the sum of all of the balances should equal total supply this is again maybe explicit or sorry implicit from the ERC 20 specification which is not really a specification of anything more than the

ABI but we can sort of infer the intended meaning of what it's supposed to be the other one more esoteric of course comes from the infamously esoteric code base of maker Tao is sometimes referred to as the fundamental equation of dye which if you're unfamiliar with these obscure variable names states that the sum of all of the dye that exists in the system is simply the the sum of the unbagged i plus the back to die so the sin here is the

unbaptized so the system expenses as is minting new tokens for in the savings contract but it also keeps you know legitimately back to die in each CDP and this is always multiplied by some accumulating variable that keeps track of the incoming interest rates on loans the third one here is somewhat simplified correctness criteria for unit swap which defines the product of the two balances of the two contracts involved the two tokens

involved in the unit swap exchange as being a constant factor so if you are asking for a particular amount of one token then the price in the other token that you have to pay can be calculating according to this formula but there are also more sophisticated correctness criteria that don't really fall into this category of variance and you know there's a whole range of further classifications that you can do but for the purpose of this talk I'm only going to call them non invariance but generally these are criteria that are

formulated in terms of maybe off chain data or perhaps past call data that is not stored in the contract itself and here we need to do some more the the quantification involved in order to make these statements require access to variables that are not directly accessible from within the contract so let me just go over an example and I think it might be a little clearer how these can look so we're going to be looking into a little more depth of a recent formula formal verification project that was

finished a couple of weeks ago namely that of the etherium to deposit contract this was a contract written in VIPRE which was formally verified by run time verification which is also closely associated with the team that built the k framework in which the proofs were written and this was a sort of end to end formal verification meaning that they actually verified both the implementation and these higher level design goals and the high level design goal was not could not be formulated as an invariant because it deals with call

data past transactions so I'm not going to go into too much detail on how the deposit contract works but generally the property that you want to prove of it if you want to prove its correctness is that when new deposits are put into the leaves of this Merkel tree that the deposit contract consists of you don't store every leaf of the tree rather you only store the minimal information necessary to recompute the roots since you know that the right-hand part of the Merkel tree will always consist of zero

notes and you're opting updating it incrementally you can recompute the root of the tree by only storing the read notes in the picture okay so the correctness criterion here is to show that this optimized version of the algorithm that doesn't store all of the Leafs on chain yields the same Merkel tree root as the one that does store all of the Leafs on chain and so this was verified by our V and this was done in two steps they first built a high-level model of the system that simplified some of the implementation

details and just try to prove that the optimization employed is faithful to the naive implementation and here they found a missing edge case which was not really that important I mean it's it's mainly of academic concern maybe because it deals with a state that is very unlikely to ever be reached but still interesting that that you can find these things at you that your proofs really won't go through unless you have specified this edge case they also found a couple of different implementation bugs and now this has to do with the VIPRE compile the VIPRE compiler mostly since the

contract was written in VIPRE all of which were addressed in subsequent releases of VIPRE and I won't really go over the liveness subtlety but it's there in the link if anybody is interested but another reason why I'm bringing up this example is not just to talk about how you can do formal verifications but also a little bit of an example of what the state of the art looks like when it comes to specifying the behavior of smart contracts there's quite a high level of detail and is not really that human readable by anybody

who isn't intimately familiar with a Kay framework and so I want to present an alternative to writing specs in this manner while maintaining the same level of formality but first let's talk about what we might want our specs to look like I think that a specification should at least be a human readable functional description with clear intended semantics of the smart contracting question clearness here being you know somewhat vague I admit but for a more precise definition you should say that

maybe two to implementers that don't know anything about each other's implementation should have to functionally equivalence implementations by just reading this specification it should be implementation agnostic I think although it can use some common elements from different languages as long as it doesn't commit too much to one route or the other and when it comes to completeness I think one sort of bar to keep in mind should be that it should be complete enough to cover the whole range of behavior that even if somebody wrote

an implementation that was adversarial in the sense that they tried to cram in some backdoors if you can prove that this implementation satisfies the specification then then there shouldn't be any back to us like that you should have a specification that is complete enough to admit anybody submitting an implementation and this being you know as good as anything so here comes Act which is the smart contract specification language that we're developing and I'll give you a flavor of it in a minute but let's just let me just tell you what it is and what its

goals are it grew out of Caleb which was a tool that we developed to to write K specs in in a slightly more human readable language than the slide I just showed you and it aims to be complete in that it should really admit adversarial implementations you should be able to once you have the specs for something just add some implementation and check it against the spec if it passes and this implementation is correct and this mainly deals with implementation of course so what act also aims to do is to

support different proving backends can either deal with the implementation or these high level invariance or design goals and so the first three targets that approving engines that we're dealing with will be KVM SMT theories and caulk and the sort of refinements that shows that the higher level model is faithful to the low level specification should really come for free in that the dual nature of specification ensures that both the implementation verification and the design goal verification is really

dealing with the same fundamental specification of your small contracts so here's an example here's a not a complete ERC 20 but a minimal token that can at least transfer balances around and some thing that I immediately liked about this specification language is that it's roughly the same length as the implementation a little bit longer but it should be more informative in the sense that it may force you to think about cases that you wouldn't otherwise like the corner case where if you're

sending somebody a a token and this somebody turns out to be yourself well what should really happen when you're writing the algorithm that implements this since you're operating in an imperative environments you are really really performing these actions one after another and so what happens is that you first give some balance away and then you you take that balance and give it to somebody and now since these somebodies are really the same person nothing really happens but if we look at the functional description of what this

method does then we need to specify these these things as different cases because if we are specifying the post date as a function of the input space then it doesn't make sense if we assign two different expression to the same storage variable so every storage update that you specify needs to be relating to different locations I'll go into more detail when it comes to the type of proof the the proofs that can be

exported from this framework in a second but I think that there are benefits outside of formal verification to having specifications like this too and some of those are listed here most interestingly perhaps I think that this can be a clear target I guess which you can test and fuzz smart contracts if you have a clear correctness criterion then you can simply randomize your input and keep checking whether this correctness criterion continues to hold under all possible cases somewhat more speculatively perhaps is dealing with decentralized insurance where you have

some form of arbitrator which will reimburse you if a contract turns out to be broken well now you have a very clear definition of what it means for a contract to be broken because you've formulated its correctness criterion and so then the the reimbursements or the the decision on whether to reimburse or not can be automated so here's another example which I hope is large enough to at least get a picture of what's going on and this example is interesting for a couple of reasons but first let me just give give a taste of the different

things that one would be able to export from a specification like this you'd get the K specs which deal with the implementation correctness and since you have these conditions under which well they're translated to requires in the implementation you have these conditions that must be satisfied in order for the function to execute fully and and performance state updates you're really making two claims you're making a claim that if these conditions are all met then the storage will be updated in this way and if they're not nothing should happen so this turns out to be two claims in in terms of case specifications one fail case where you

assert one of these conditions to be false and one pass case where you assert the condition to be true and that the storage updates should be performed accordingly and here's what the key specs look like the second proving engine being SMT queries now this one is not dealing with a functional sorry not dealing with the implementation correctness but rather with this invariance that we have formulated right here the invariant of this contract is that the relationship between these

three storage variables is that the product of two of them equals the third and so to prove this invariance we can formulate the entire control flow of the contract as being given by two methods F and G and then a couple of rewrite rules or in this case horn clauses that that model the control flow of our contract we're saying that given any pre state we can either end up in a post state which matches what happens when we apply the F function or what happens when we apply the G function and then the claim that

we're trying to prove well here it's a negation of the claim that we're interested in they know that there will never be a state that satisfies the there will never be a state that that violates the invariance if this is the case we have an error so doing a query like this would give you a counter example this is why it's negated and then finally the third back end is something that you would use if you were unable to prove the the invariant with an SMT query since there are some limitations to what you can do there and when you're working with proofs in Cocke you need to

do a lot of manual proving so act would really just give you the definitions over which you need to make some manual proofs so the the final statement here is the proof that the Merrion holds and it's it requires manual intervention here's a little bit of a technical point so I'm just gonna check I'm doing on time not doing that well on time so I guess to summarize what I want to say here well first of all it's all summarized in this one readme markdown file that I wrote and it's exploring

different ways of encoding the control flow of contracts and the types of proving methods that you might employ to prove invariance it well comparing two different encodings and showing that one works and one doesn't in this case okay so let me just talk about some of the difficulties in developing this specification language and then some of the future outlook and then hopefully I'll have some time for questions the most obvious difficulty is dealing with calls to unknown code because this is really

a fundamental source of unspecified behavior in your smart contracts you're saying if you have a method F that does some call in the middle of it you're saying that you can clearly specify with what happens up until this point where you do the the call to some unknown code but then clearly it's unspecified what happens and then you return and you do some things so this is not only hard to formulate in the specification language but it's also hard to reason about what might happen another difficulty that I should mention is dealing with loops because to formulate the the post state

as a function of the priests state when you have some looping recursive behavior can be quite involved and you often need some manual intervention here to reenter Z also complicates this inductive view of smart contracts because you can end up in states that are not isomorphic to your original state and so to imply the inductive arguments it becomes complicated as so finally I'd like to urge everybody who's writing smart contracts to be a little bit more diligent when it comes to writing specifications what I've presented here

is one approach to writing specifications but even just having a natural language so English specification is a lot better than 99% of every project out there and especially if you have some form of correctness criterion for your smart contract then formulating this makes it easier for people to understand what your smart contract is about but also to verify that it actually adheres to this behavior so if you have some smart contract that you would like to experiment with specifying in this language then I'd happily accept any examples and maybe there might even be some formal verification proofs of your

smart contracts if you do this I think I'll end there if you're interested in reading more about these things you're looking at some of the examples that I gave in a bit more detail here first of all the slides and then some relevance repositories thank you very much okay so thank you Martine great presentation about form of Education not great with timing though we can have time for one question one question only if there is so I guess greats great there so thank

you thank you [Applause]