Using Solidity's SMTChecker by Leonardo Alt (Devcon4)

yeah he's heading Leo work with on foundation aetherium foundation on the solidity team doing language design work and compiler work and also doing formal verification which is what this talk is about I'm going to talk about so ladies SMT checker which is a formal verification component that gives compile time results about safety safety checks so have two questions so how many people here are a solidity developers okay cool and how do you feel about audience participation okay cool you asked how so request the answer is you're gonna help me solve this so I want to first introduce what is SMT what's why SMT checker so the SMT comes from satisfiability modular theories and Assam to solver is a tool that will take a formula like this a first-order logic formula and try to answer this questions can we find integer values for a b c such that this formula when we substitute the values for these variables evaluates to true so just two I can go together over the formula just to give a little bit of context to whoever is not familiar with electrical activity this kind of things okay so it's a boolean formula right it's a conjunction of constraints so this formula kind of returns true or false right a boolean value this constraints are satisfiable together or not so first we have this part of the formula which basically says it's kind of like a function definition right so there's a lot of same sex abuse here but we're gonna ignore that for now so this says that for whatever acts f of X equals x times 42 okay the next we have two constraints over the input variables we chose so we're saying that a has to be greater or equal B and B has to be greater or equal C and then last we applied function f we defined before over a and C saying FFA has a be greater or equal F of C so now the question again can we find integer values that evaluate the formula to two true yes okay can you give me values for ABC yeah so now you told me that it's possible right it's possible to give values for a B C such that the formulas true 0 0 0 does that work it works right zero greater equals 0 true same thing for BC f of a 0 F F is f of C 0 it's true right but unfortunately that's not the one that I had here so anyway so this one works right also this one works and this one works how many do you think how many solutions how many different sets of values for ABC do you think we can get for this formula infinite right now a slightly different question what happens if we change this we could change the comparison of FA and F of C to this and repeat the question is there a set of values for ABC that make the formula true so there's a consensus saying no and that's correct and when that's the case we say that the formula is unsatisfiable because there is no set of values that satisfy the formula so in the previous case were satisfiable now we have unsatisfiable and why did I choose this formula could have chosen many other formulas so the reason is we can read this formula in many ways right it can be just a logical formula but this formula happens to we can't we can also read this formula as this part here highlighted right now being a property we want to prove to function right application of the function that part being local constraints say on input variables and here basically a function definition so this is basically how we just prove correctness of this smart contract here we have a function definition which would be encoded in the SMT language as the first term of the conjunction here we have two local constraints right that evaluate that or encoder Tory as those those circumstance and here we have the application of the function but you will probably notice notice right now that in the code I have assert F FA greater or equal F of C because it's a property I want to prove right and here in the logical formula that we give to the SMT solver it's actually last then so it's the opposite operation right the reason why we actually ask for the opposite is if this is unsatisfiable if we try to prove the negation of the property and the solver says is unsatisfiable this means that there's no behavior there's no values for local rivals with that encoding that actually break the assertion right so in this case the solver will tell me it's unsatisfiable which means that certian is safe again because there's no way you can go through the program and break the assertion so for all cases you can ever come up with the assertion is true but let's change a little bit so is that assertion true is that assert correct for every input it's not right so for our query to the SMT solver we negate the property right so I want to find values I want the SMT solver to give me values for my variables that actually break the certian so one FFA to be different from F of C and in this case the solver will tell me it's satisfiable and here are some values and this is exactly the output that solidity compiler will give you at compile time when it's Y when you run exactly that code so here we see that compilers say assertion violation happens here for its assertion for a1 b1 c1 c0 sorry so the SMT checker as a summary after Jack symbolizes saw it's a SMT based so we use SMT solvers so it's an SMT based it smart contract form of verification framework it's built in a compiler which is for us one of the one of the big advantages compared to other ways to formally verify your code the way it works the way the approach our approach is that we encode program logic from solidity into SMT statements and use SMT solver to run those queries that I just mentioned and we use those to check for assertion failures overflow underflow trivial conditions and reachable code and all of that happens automatically when you run the compiler one characteristic of this approach which is close to from the fortification community called bounded model checking is that this approach is sound but not complete and what that means is if it's sound which this approach is whenever it says the assertion is safe it is actually safe but whenever it says the assertion is not safe here's a counter example it might be that might be not true so you might have to verify it and see that this this might have been caused by an abstraction of some unsupported features or functions which is the case for our approach but then being sound but not complete also gives advantage that it's pretty fast and light compared to other approaches and it gives useful counter examples because it's applied directly on solidity code instead of EVM bytecode which then you would have to map back to solidity program variables which doesn't necessarily work so here's some other frameworks that have been already in indigo system for for some time in EVM formal semantics I'd have Isabel and KVM which are or KVM specially is pretty established as a really good framework for fortification of smart contracts it's more expressive but it also means that it it's harder and takes longer to give you proof so these two approaches have pros and cons caleb is a really nice debugger for a cape for K proofs wit and they will have a workshop tomorrow so make sure to check that out for a vm byte code verification there are tools like int me through in mayan which do symbolic execution on the byte code and try to find bugs basically and there were other projects that were translating solidity to language that were whatever verifiable like y3f star and zoos that with LLVM if I'm not mistake so how do you use it you just need one line of code right now it's an experimental feature it's a very experimental feature right now so if you use it you will find internal compile errors they will find and supported features and all kind of things but we are working on it to make it of course much more usable and hopefully non-experimental one day but then the next question is how do I actually use it so if they just insert this line of code there then sure it's gonna enable the run of destiny checker but what is it what is actually doing so you need to write formal specifications right so whenever you prove your program safe you only prove it with respect to specification at the regional proving anything so you need to specify what properties you're actually proving in solidity or with the SMT checker you don't need anything extra you use the normal require and asserts from the language itself so requires and asserts in a compiler or translated into runtime checks right when it's compiled to bytecode but here in the SMT checker we use them as as the formal specification so ease requires as assumptions and asserts as verification targets so whatever conditions you write in a require the SMT checker has been assume it's true and whatever you write has had an assert it's going to try to prove okay so how to use a require actually so there's a lot of debate for quite a while already on requires and asserts and when to use each or what it what which one means so I just copied it I'm gonna read it from solute docks the require function should be used to ensure valid conditions on inputs and contracts a tribals or to validate return values from calls to external contracts so here in this example we have a contract that has stayed forever a a bunch of functions G and H which suppose like that we don't know right now what they do and we have this function f that takes an integer X so here we're using requires requires two filter values for a and ax right so we want for some reason a to be 0 and ax would be less than 100 then we sum both we put it in a and then after that we we know that al as then and 100 is true right because of the requires before so if you want to prove that the last statement should actually have been a require sorry in a certain order require because it requires just going to assume it and with this with the assert we're actually using passed knowledge to prove a new property about your code in the end of the function so what about asserts the third function should only be used to test for internal errors and to check invariants a properly functioning code should never reach a fail in a search statement and this is really important if this happens there's a bug in our contract which you should fix same example now just using asserts everywhere can we assert a equals zero over there very likely not right of course it depends on what what G and H are doing but if we don't really know what it's doing we cannot say assert a equals a because they can be whatever right and especially for ax here if you say assert ax less than 100 it's a public function so anyone can call this function with x equals to a hundred and your assertions already wrong right so this is really important to notice like you should only assert things that you're really are true at that moment for every single execution path that rich is that point and here the assertion is correctly placed at the end because the new property are proven yeah yeah this moment yeah so for example we have I'm gonna talk about this later but if you call an external function for example which don't have control over or they know the code then when a function comes back we have to reset all knowledge about state variables right because you might have this contractor called might have called your contract back which changed a so you can't really keep the knowledge about it but yeah but modular verification one of the research goals that we have is to actually infer properties from different functions and see what state invariants we can come up with automatically this is not done yet but it's under to do list what about false positives so I mentioned earlier that the approach is sound so if it's a safe it's safe but it gives count it gives false positives which is basically false counter examples so your assertion might be correct and safe by the tool says it's not safe why does that happen it happens because we have to abstract the encoding sometimes so for example for complex types and functions say like cryptographic Elections we it's not our approach not expressive enough to actually implement it so we have to use symbolic variables on on the application of the function and that's as far as it gets so we don't really know what the actual value of the function call is going to be so in these abstractions might lead to false positives also if you call external function if you do if you yeah I call external functions we might have you we do clear the knowledge after the call after a function call so it might not have been the case that the that state variable a got rewritten but you never know so to be safe again we have to clear the knowledge also the contract state invariants you as the developer of the contract might know that certain properties are valid throughout your contract but the SMT checker is not yet smart enough to deduce those properties automatically so and one point that I wanted to mention in this talk is you can actually help the SMT checker you can help the tool to actually find it proofs and it's a very simple way to do it you can flood your code with requires so every assumption even very simple things that you know are true at that point even if it's if even if it might sound redundant to you it might help the solver because the more constrained to give the last false positives the tool is gonna it's gonna issue so I'm gonna run a couple examples right now think of how like eight minutes can everyone read not in general but screen what I did push yeah and it sorry this one like okay so this is like a very tiny token and not very interesting so we have a map in with balance constructor initializes the balance of the message center with a bunch of tokens and accounts can transfer tokens which other right so there are few line a few extra lines in this piece of code right compared to normal token implementations so first of all this is a normal one right we required that the message sender actually has the amount in their balance but here I'm actually storing the old values for the balances for the person sending the transaction and the person receiving and yeah the person received the account receiving the amount here the balances are updated right and here we have an assertion that says that the sum of the balances before the transaction before the operations have to be equal the sum of the balances after the operation oh sorry yeah this should be the right assertion but I want it to break so okay so here the tool tell the compiler tells us the assertion is broken and gives a bunch of values for for our variables right so but there's something weird right so it's saying that it gave zero to both two and message sender which commonly people prevent right so we can just add that here I want message sender to be oh this is actually gonna work so I'm just gonna say they have to be different it's fine if there is zero so okay now it changed right so two and two one before was zero mass percentage to zero but that's fine because they're different and the assertion is actually saying that the balance before was greater than the balance right now which means that some tokens vanished right so the assertion is basically saying every time there's a transfer tokens vanish which hopefully is wrong and the tool set is wrong can say balance from plus balance to is actually the same as balance of serum plus balance of one which are the accounts so if we actually fix the assertion there you go if there's no if it doesn't complain it means it's safe I'm gonna move on to it's likely a better example with a bunch of false positives oh not this this okay so here we have yeah this contract see this there's external contract this matter for now oh sorry about that it's not the one I want to show this one so we have just like kind of an account but some it stores the some the balance of like it's its own balance and here it counts how many transactions how many times the fall back function was called increasing the value increasing the balance of this account so here we have the fall back function that says that the value sent to be greater than zero and this is just to give a constraint for an avoider if cause later requiring that this account cannot have more than 1 million the balance cannot be greater than 1 million so here we just increase the sum and increase account right and here we have a function called average that computes the average the average value that was sent per transaction all right so here I put is required because if if there was no transaction doesn't make sense compute the average but here we have an ax so here we compute the average and we assert that the average has to be greater than zero right because if you did have a transaction because of this line we cannot compute we cannot we don't count zeros in a transaction so the assertion is true agreed okay so it's telling us that the assertion is actually not true and give some value so it says that if count is one and sum is zero then the average is zero which is correct right but then the question is can this ever happen can count can it have ever happened that count is 1 and sum is zero why exactly so message Valley is an integer right with this require is a message value is actually at least one here and count only increases by one so this property here is true right it's an invariant it's true like at any point of the contract right but it's hard for the SMT checker to figure that out on its own and that's what I meant with you as a developer of the contract know this kind of thing then you can help you can help destiny checker by adding those invariants whenever you have these harder checks let's see okay now it's fine so I have one last example which was the one that actually closed here yeah it's the same it's the same contract just with the extension that we have this exterior contract and we call some function f next we know contract and what what happens here is that when we call the external function the knowledge gets basically erased and you would need to add new constraints after the after the after the function call you maybe even need to repeat unconstrained sue in order to help us over to actually prove it and not get false positives and one last thing that I wanted to say is future plans that we have for for the tool yeah we have more examples and I'd be glad to talk about the tool more offline if you guys want I want to talk about it as future plans we have what I mentioned which is this sort of function modular verification part which is kind of involved with the state invariant automatic deduction which is a very hard thing to do but we want to try it anyway and also one other thing we want introduced rudder soon is actually the ability to let that developers give this variance so something like you could write something like declare your invariants and this would be one of them and with this invariant is invariant would be applied as a require in the beginning of every function and asserted in the end of every function in Diani we could even use that to get inductive proofs and yeah just get give more power mm jacquard and actually get harder properties proven anyway even though they're pretty hard so yeah open for questions not sure how much time there's left yeah no time left so we can discuss offline time is gone thank you