Specifying & verifying Solidity contracts by Martin Lundfall

um so uh me and lee are going to be talking about formal verification of solidity contracts and a little bit smart contracts in general um some of the ways in which the language and the compiler can assist in doing this process and uh also talking about act which is a um language for specifying the behavior of smart contracts and i'll try to keep this relatively uh brief leaving a lot of room for discussion about what can be done to improve the workflow as it is right now so um to begin i'll just uh position this this question of how to specify the behaviors related functions in context um sort of opening up for the discussion one way in which you can do this is to use asserts directly in the function source and if you are not using annotations but rather referring to the variables directly in the solution code this is how that can look like for a transfer function you would be asserting that the relevant variables are changing expressed in pre and post conditions and it can look something like this but if you don't want to do it directly in the function source an alternative would be to have like a wrapper function and this relates again to the discussion we just had on conventions for testing frameworks um because this looks very similar to how you would write a test if you are writing your tests in solidity at least um and yeah i think it's sort of straightforward what's going on here you you do some caching of variables before you execute a certain function and then you compare those values according to some condition against the state that you get after executing that function and then there is the alternative of specifying the behavior in a language in a different language altogether and so here this language is act which i'll be going a little deeper in during the next couple of minutes so i think this is a good example to just get a flavor of what the syntax can look like if you want to really highlight everything that's going on inside a transfer function so it should be noted that this function makes a little more of a precise claim on the previous two uh in the previous two really only talking about the updates that happened to the balance of mapping whereas here we're also saying under which precise conditions these updates are happening we're saying that call value should be zero since this is a non-payable function and we're doing the um we're doing the check that is is done implicitly here by the safe map and we're also immediately forced to consider the edge case of what happens when you're actually transferring to yourself so in aspects you are forced to split up um every claim that refers to mappings depending on whether you have a collision in those mappings or not so i'll get more into that in the next slide i think but let's just talk a little bit about the different approaches and and sort of the the pros and cons for them so for the first two obviously a big uh advantage is that it's integrated and the developer doesn't need to learn an additional language however obscure you may find it but it can just work directly in solidity and if you're writing your properties of the function directly in a source things are also pretty transparent or auditable by people reading the implementation because they'll see your claims about what the behavior is supposed to be and they can either test it for themselves with their own frameworks or they can just sort of get a better understanding maybe of what this function is supposed to do if they prefer um reading this this functional description uh over the uh sort of implementation that is given um an advantage of of the the latter twos of having this wrapper spec for the specification in a language completely outside of solidity is that it's more agnostic to the particular implementation if you were to change how the nature of transfer were implemented you could probably still reuse the same testing function and even this spec but if you want to change how the implementation does what it's doing according to the spec then you'll be forced to rearrange your spec too probably or you'll be forced to rearrange the cranes that you're making inside the implementation uh and you can get that sort of pair because now you're editing both um what the contract is actually doing and the description of what it should do uh insane in the same development process um and so another advantage of using a different language that is designed to design for the purpose of specifying smart contracts is that you have these you can make decisions that are more aligned with how functions are described independent of how they are implemented you don't really need to care much about uh what is the most gas efficient way to do something but you just want to describe the result of whatever implementation you might have um and also as i mentioned there are certain features of the act language that are designed to lean the developer into making sure that they really think about all of the edge cases that may exist in the implementation um and are forced to think about them explicitly um also when when one has an outside language that sort of exists beyond the scope of the evm one can talk about all of the variables involved as true integers and not just evm words that wrap around to the 256 as we can see here on the last line of the infinitely if block we're able to express that the addition of value to balances of two should not overflow and we can express that by explicitly giving the bound of 2 to the 256 even though that is essentially unexpressable at least in this form if we are only allowed to use bitwise edition uh yeah some additional points there that i think are obvious one big approach that i didn't mention here is of course if you do a sort of sulci verify um approach where we use annotations instead of using the source code directly uh so to summarize the the um the essence of act um it is designed to be a human readable function a human readable specification language in which you can express function descriptions and contract invariants get to that later which from which you can generate proof obligations to multiple backends so there's a large number of um formal verification tools that are emerging well there has been for a while but they're getting uh very good right now and it's really curious to try these different tools up because they have certain strengths and weaknesses and are also operating in slightly different domains and so act can be used to try these test tools against each other and compare the results but also utilize the different tools that are targeting different domains so when you're working with these source level specifications or development tools you're always at risk of the compiler doing something that you're unaware of or behaving unexpectedly and this is sort of a blind spot for the formal verification process but then on the other hand if you're doing byte code verification it takes a very long time and can be difficult to do stuff like contract environments so act as an attempt of modularizing the process of doing formal verification for smart contracts and being interoperable with these different backends so our first couple of plants for different backends we'll be targeting um is a caulk back end for claims that are difficult to prove using smt solvers and really require manual groups um smt queries for doing contract invariants and certain checks that are easier to do in the snt setting and for bytecode verification um you already have a prototype of exporting proofs to kvm and there's also an hdm backend and it works which will be faster in in many cases but slightly less general and so to go a little deeper into this point about the modularity of of proving tools and verification setups uh here is a more in-depth uh example where we are expressing a invariance in the constructor of the token so this also touches on a point that i'll get to a little later where here we have this sum construct which is which is not native to to solidity or even something that could generate any reasonable byte code but it's very useful for formulating properties about what we expect our contracts to do so yeah here's here's more of an example and i guess one point that i'm trying to make here is that i think this language is pretty similar to how you may express the nature of what you want a token to do in a setting like you're writing an erc when i recently was writing an efc for permit i wrote the description and the specification of how this new function and token extension is supposed to behave in a language that was very similar to this because i think that it really allows for people to make their own implementations and and have freedom in how they decide to uh optimize their particular behavior while still being completely unambiguous in terms of uh what the function should do so as a result of this it means that if you're writing an erc in this language not only will it be clear for people to read and implement but it can also be something that you can use to test and formally verify that um ercs are actually implemented in the correct way um yeah so here's a little bit more about how it actually works is there a question or just a sign i'll keep going then um so i'm not going to go into too much detail here i'm just going to say what i said before that that the the design decisions of act are made in such a way that you should be able to um really think about all of the education there was actually a question mark there was a question should i go to the gator chat or like someone raise their hand here who was it just it was me um so what about the limitation of the language can i for example describe my property over a set of function like something should old after calling f1 and f2 or something like that yes so we are so actually the the syntax that you saw here uh of invariant is a um special case of a numerator that holds over all functions but there's also a syntax where you can do invariant of and then functions so yeah it's a good point um right so so here is i guess um a more concrete um way of expressing what i mean by doing this modular approach to verification if we take a an example smart contract this one this is going to be a contract that i now only express in terms of ax syntax but you can probably imagine the selected implementation should be fairly straightforward to see so we have some sort of we have three variables that it's dealing with x y z um and an invariant that we expect to hold from them if we have two functions which simply updates two of our variables in both by multiplying it with a scalar either multiplying x and z using a function f or updating y and z using the function g then this generates a cog theory which is beyond the scope and sort of agnostic about the blockchain setting that this smart contract is operating it and so it has sort of the essence of this contract and it allows you to [Music] get all of the relevant definitions over which you can do the proof of safety that that you've expressed in the um in the act syntax so all of the boilerplate that comes with generating the definition and the theorems here of the smart contract involved would be generated automatically and you simply insert the proof i skipped ahead a little bit let's see if there was something we missed yeah so i guess i showed it now by example rather than explaining the details of uh of what i meant to say i'm essentially saying that usually when you're doing a formal verification this sort of end-to-end formal verification process where you have some smart contract business logic sometimes people refer to or high level specification which you expect certain properties to follow you can make proofs on a high level which aren't referring to any byte bytecode specific or blockchain specific parts and then you can also perform the bytecode level proofs with the same specification if you're using act so this refinement that the higher level properties that you're proving also hold of the lower level bytecode that you get from the compiler is more of a property that either holds or doesn't help the fact well hopefully it holds if we do everything right but it's not something that you need to do for each project right so here's just a little list of some motivating properties or motivating examples for why you may sometimes require something more complex than just smt solvers for proving correctness of your smart contracts simply because there are certain properties of smart contracts that that express the correctness of them that are too difficult for smt solvers to do and this is a good example which you can actually prove using smt theories um depending on which strategy you take to doing it but i think uh doing something more complex would be out of scope for this um okay so in conclusion leaving more time for questions than and discussion rather than just presentation um in doing acts and in writing specifications of smart contracts using act you get this language improver agnosticism so you can compare different provers but you can also compare different implementations of the same logic or different languages uh writing the same smart contract so we can compare the bytecode generated by force by per se versus the bytecode generated by civility against each other um actually just just as a note on that this was the subject of a presentation that i did at last.com where we had um similar to the previous slide a a specification for uh in year c20 and then the the talk was more of a hackathon where people were competing to make the most gas efficient erc20 and this is sort of a safe way to do these gas golf competitions because now you know that not only can you have these crazy optimized versions that are supposed to do something and you sort of have some tests we get to check it again but you can actually do formal verification against the bytecode that is generated in the app so it's a very um very good measure to have if you're really keen on making crazy optimizations um yes so this is act please come to the gitter channel to discuss it if you're interested and just to to keep this sort of focused on on solidity here are just some uh pointers that um uh well an ask really um to uh to sulci and the developers of maybe something that was discussed already uh during the debug session i'm not sure it was enabled to not send that unfortunately um but the ask is essentially this and it's related to bytecode verification basically this situation is that um when you're doing byte code level proofs often you have a pretty performance heavy duty because you're symbolically executing abn code and there's a lot of things that can happen and in order to scale this process what one wants to do is to reuse proofs about subsets of bytecode as lemmas and other groups so if you already know that a particular internal function can be summarized to do this then you can reuse it whenever you get to that part of the bytecode but this is sort of tricky to do using solidity right now because it requires a lot of manual labor to extract the relevance relevant pieces of byte code the ast really helps and the source map really helps but what would help even more is to have pc values directly from specifically internal functions and modifiers so this is my password i have a method of extracting it now which involves you know combining the ast and the source map but it's very unreliable and i think direct support for this would be beneficial for other tools as well um yeah are there any other things i want to say not really anything more than what i said here oh well maybe one thing um variable location um at function heads and and loops uh it could also be valuable can you be a bit more specific on that so what also on the pc values what exactly do you mean so uh essentially what i've been doing before is when doing a proof about an internal function is that you go to the pc value that represent the jump test where this function begins and usually if it is a stack based function you have the arguments organized in stack in reverse order to how they appear in the function declaration and then you can do your proof like that it becomes more complicated if you have a function which involves memory and and also if the function comes from a different contract that has been imported somehow uh or inherited from then uh getting the the the location of how these functions relate to the bytecode um is kind of tricky is that clear chris or can i clarify something is that so stupid why is there even a hang up button to finish up on that so um you would like a mapping from probably ast id of all functions to the entry point as a bytecode offset um yeah okay cool thanks francie can you direct or sort of say who yes uh jocelyn is uh yeah nice talk so could you describe uh act start and stop typically like is it um a dsl with a json output or does it do like more stuff like checking if it's a variable like if the x variable are the same as the contract variable and stuff like that um so it is right now a generating from from the specification language json output which or sort of intermediate um representation which can be used for um to plug into different packets um and also we'll be supporting some back ends internally without throwing this this ast but there's also the option of um so to answer your question i think it's about whether the source code needs to be available uh for these proofs to go through or not or at least that seems to be part of the question and the answer is for some back-ends it will be necessary um or for some back-ends you will be required to do additional work if the source code is not present so a newly introduced feature or you're new but a feature now of the solution compiler is that you can extract the location of storage variables and then it's very very nice to write specifications like this where you want to do by verification proofs because you can simply refer to them by the name and if you have the source code you know what those uh storage locations are gonna map over to in terms of evm locations um so if you don't have the byte code or if you don't have the source code of a contract when you still want to make this bike a local proof you would need to be more explicit about where these different locations go and if i have the source code the json output is going to have directly the storage location uh yes there is