Bad Proofs in Formal Verification by Uri Kirstein | Devcon Bogotá

foreign [Music] and today we're going to talk about bad proofs in formal verification many times people think of formal verification as the Holy Grail or highest insurance against bugs and yet sometimes we still see that even projects that have been formally verified still contain bugs for example this is a high profile case where uh we in sartora have formally verified a specific thing about one of our customers and it still contained a bug in deployment in this lecture we're going to see how that is possible how it happens and how can we prevent that in general the lecture is going to be divided into a few different parts at first we'll say what is formal verification what are the proof that you get out of it and what does it mean for a proof to be bad then we will showcase two different types of bad proofs and we'll also show you how you can sometimes tell if a proof is bad or not and at the end we'll show you a real life example the same example I've shown you on the previous slide we'll delve into it deeply and understand it let's go formal verification is the process where we take a piece of software and try to see if it behaves According to some pre-fined set of of rules we call those um security Properties or rules we call them specifications and they're one of the two inputs along with the code that we want to check that we need to feed into the the software that that executes the formal verification in this case for example the circular approver and then after the prover gets those two inputs it can give us one out of three possible outcomes one a proof that means that in all different cases ways behaviors or States the program behaves as intended another is that it doesn't always behave as intended and then we get what we call a counter example which is um often showing us something that is hard to find and very often a bug in our program an unintended Behavior and also the tool can time out and then in that case we don't know if the software is behaving well or not let's show that with a simple example of a facility pseudocode this is a transfer function we're driving we're transferring some amount of tokens from one address to the other and an example of a specification that we can give to to the software that does the formal verification is this invariant that says that the total supply of the token is equal to the sum of the balances of all addresses that hold a token which makes sense if we feed those two inputs to the prover we will get a bug we get a counter example A specific scenario where that invariant doesn't hold anymore here we can see that when we pass an amount of 18 from the address of Alice to the address of Alice we get a violation we see that Alice's Alice's balance grew by 18 tokens which it shouldn't have now the invariant is broken and that's why it's a bug however if we try and fix that solidity code let's say to this implementation which doesn't contain bug will actually get a proof and what does that proof mean it means that the sum of the balances of the token for all addresses before and after the transfer is equal and then we can be sure that it's true no matter which addresses we chose and which amount we have chosen and that's one of the key advantages of formal verification it is exhaustiveness we're not checking for a specific set of inputs but instead we're covering the entire input space that way we're able to find bugs that are often or sometimes missed by humans another big Advantage is that whenever we get a violation it's very easy to verify it we get specific numbers specific addresses and we can see and run it ourselves and see if we get a violation or not and try to track and see exactly where the problem lies and also we can get a proof of correctness which is something great that we can't really get through many other security methods for smart contracts however those proofs are very hard to verify obviously we cannot go ourselves through all the different inputs and see that it's true or not else would have done that instead of trying to prove it right and actually sometimes our proofs don't actually mean what we think they do sometimes we're proving something completely different from what we've intended and those proofs are bad because they can give us a false sense of security and if we have a false sense of security we might upload code prematurely that might contain bugs let's look deeper into those specifications I've been telling you about this code that you see on the screen behind me is written in a specific language called the circular verification language used for writing specifications but um the same principles hold no matter how you represent your property the general Anatomy is dividing into three different parts the first is the precondition then we have an operation and then we have a post condition and if we look at this specific example here we check that the transfer function behaves as intended the way that we do that is that at first our precondition we check the balance of Bob for a specific token that's our precondition and we keep that number then we do the operation in this case it's the transfer function and after the operation we check the post condition we check the balance of the tokens of Bob after the transfer and see if it is indeed equal to the balance Bob had before the transfer plus the amount of tokens we have transferred to Bob let's look at it more visually and when we Define a property we Define a starting state by the different constraints that we give and that's the circle the arrow represents the operation and then we want to land within one of the desired States one of the states that satisfy or in which the assert expression that we had holds okay so the desired behavior is that every state that is within the starting States if we do the operation if we draw the arrow we end up within the green circle and all of them live within the space of possibilities when we get a violation we get into a counter example that means that we started from one of the starting States we did an operation we have an arrow but that Arrow doesn't land within the desired States that's a counter example that's a violation that's what might be a bug and the interesting thing to note is that if the tool cannot find a counter example for the specification or the property that we provided it then it will output us approve and that is because in in logic we Define a false statement as a statement to which we can give a counter example that part covered on the first section of this lecture what are the proofs and what is formal verification and now we look at two different types of bad proofs the first step is what we call a vacuous rule or vacuous proof vacuous is something empty or mini glass or insignificant and this is better shown by a real life example I am 29 years old and I don't have any children yet and I'm claiming the following statement if I let my children drink Colombian coffee they will sleep better at night is that statement true or false so if we want to say that the statement is false we need to provide a counter example so we need to start from one of the starting States meaning you need to choose one of my children then you need to do the operation meaning let them drink Colombian coffee hopefully not too hot not to injure them and then you want to see that they actually do not fall asleep at night can you do that you cannot do that since I don't have any children and therefore there is no counter example to that claim if we don't have a counter example to a claim the claim is true here it's true vacuously we don't have a starting state so it's true however I can also say something that apparently seems completely contradictory I can say that if I let my children drink Colombian coffee they will not sleep at night sounds completely the opposite yet the same principles still hold you still cannot provide a counter example here I still don't have a child and therefore that statement is also true if you look at it visually we just don't have any starting States and we don't have any arrows and therefore we cannot have a counter example let's look at a code example this balance of function belongs to a token of open Zeppelin and the interesting part about it is that we require that the address that we check the balance of cannot be addressed zero one of Sir torah's employees was working on open Zeppelin contracts as well as writing a rule of property that he thought should hold on the tokens of open Zeppelin however that rule that specification contained an error you see in the middle of the rule we have this requirement that the balance of the adverse zero for a given token must be zero that can never happen because every call to the function balance off for the address 0 will revert and if it reverts in particular it never returns back the value zero therefore nothing can satisfy this requirement if nothing can satisfy this requirement we don't have any starting States this is a vacuous rule and therefore it doesn't actually matter what appears later in the rule after that requirement it will be true no matter what we do and in fact I could try and insert something completely ridiculous I can assert that 0 is greater than one and that would still be true because you cannot still give me any counter examples and when a rule is vacuous we can prove anything we want unfortunately vacuous rules are not just an academic concern for modification has been used a lot on Hardware along the years and Studies have found that about 20 percent of specifications written on Hardware on the first time are actually vacuous and whenever they are vacuous they hint at a real problem either at the code you're trying to verify or your specification so this is a pressing problem but fortunately we have some ways to try and catch them and one of the ways that we use insertora is is doing what we call a reachability check what we do is that we take the same specification as before exactly as it is and add something at the end we add an assertion of false obviously assertion of false is always false so we want so we expect the rule to fail we expect to get a counter example right because because nothing can can satisfy false however if we do not get a counter example if the rule is proven that that means we didn't actually reach that last line of the specification we didn't reach that last line of the specification because that requirement um erased out all the possible starting States it doesn't matter we never reach that last line and that's how we check that we we say something absurd at the end and we see if we fail or not if we don't fail that's the problem that's when we know that a rule is vacuous for completeness I will say that usually when we have vacuous rules it's not due to one um One precondition One requirement that is never satisfiable it's usually due to a combination that um their uh intersection is actually empty and not satisfiable but each part by its own makes sense for example here if you require that X is smaller than y maybe we can we can prove the property let's say we add another requirement y smaller than Z now we limit the starting state only to be the intersection and if we add this third requirement that Z is smaller than x then we have no intersection anymore here by transitivity we say that X is smaller than itself and that's never true for any number therefore we don't have any starting States and this rule is vacuous but note that some combination of those requirements could make for a sensible rule moving on to the next type of bad proofs we're going to talk about tautologies a tautology is something that is always true um and therefore is actually not telling us anything useful about the code that we're trying to to prove things on for example let's look at uh this Rule and this rule tries to check again um the Integrity of the transfer function we check that the balance of a recipient is zero then we transfer some positive amounts of tokens to that recipient then we assert that the bounce of tokens for that recipient actually grew however this rule on the screen is wrong because we didn't check the balance of the user before and after the transfer we checked that the balance of the of the user after the transfer is not smaller than itself and this is something that's always true for any number and that's a problem because in this case we didn't actually check what the transfer function is doing we're checking something that is always true the transfer function could burn all the tokens could send all the tokens to me or you can do something entirely different and not move any tokens around we don't know we didn't actually check that if we look at it visually at autology something is always true so it encompasses the entire space of possibilities so here the arrow representing the operation lands somewhere within the space of possibilities and therefore is true the problem is that we could have drawn any Arrow we could have done any operation and it would still be true so we didn't check anything specifically about our code at all the way one of the ways that we find dotology in the insertora is that we will remove all the preconditions and all the operations just live the record the assertion at the end and see if it still passes or not if it passes it means that it it does not depend on the requirements and the operation it's something that is just always true and therefore it's a tautology so here in this example we just remove all the lines but the last two and in this case this rule would pass it would always be true and that hints that it's a tautology and now it's time to delve into the real life example I've shown you briefly at the beginning of the lecture before that I need to introduce you some new notion a notion of an invariant an invariant is something that is always true in particular it's something that is kept after doing some operations in our case is it's calling functions of a smart contract the way with the reproving variance is by induction and you might be familiar with it from school it's similar to proving by induction things about natural numbers we have the base of the induction we're trying to see if the condition is true right after calling the Constructor and then we're doing the step of the induction that is we assume that the invariant holds we operate some function of the contract that must be public or external and then we check that uh that it's still true after the same condition is true after if we do that we get that the invariant is true the same when the induction proved that things are true the interesting thing here is that we check for every possible function of the contract and this example belongs to notional which is one of the tourist customers and they were using our tool and writing a specification and we'll go over it it's a more complex example because it's a real life example what they tried to to prove here is that an asset in their system and their system allows lending and borrowing at fixed rates by the way an asset cannot be counted both as a bitmap asset and as an active asset and here we see that they try to reach that conclusion at the end the highlighted line at the end says that the same currency can't be both active and bitmap the first line here is just a natural requirement on the index of the asset and is not very interesting and the rest is where it starts to get a bit more complicated here we see we have one statement that says that the Vietnam currency cannot be zero and that will always have to be true then we have another statement that has an or sign and if we look at the first part of it we see that we require that the active on mass currency is equal to zero so if you look just at that part of the or statement we see that the Vietnam currency is not zero and the active currency is zero so zero and non-zero are always different so the conclusion is true trivially true what happens if you look at the other part of the or statement here we require that the active Mass currency is zero emotional system assets are represented using 14 bits plus two more bits for a mask so the masking passes all 16 bits and the unmasked encompasses the lower 14. but if the mass currency is all zeros means that the and mass currency must also all be zeros therefore it follows that it is zero itself and we have actually reached the same statement as we've reached before meaning if the bitmap currency is not zero and the active currency is zero then they must be different and that's always true because zero is always different than non-zero and in total we get that this entire statement although complex is their statutology hard to see and you can understand why uh the person that wrote it could make that mistake it's not apparent but this is indeed a tautology and unfortunately the code was deployed uh thinking that it cannot contain that bug and unfortunately it did the bug light in this specific function enable bitmap currency and it's a bit hard to see the bug itself so I'm just going to show you the exploit scenario the exploit scenarios goes like this we enable the bitum currency for an account let's say if we deposit a second currency for that account uh let's say die and then we try to enable die now as the bitmap currency due to the bug now dye will be counted both as an active asset and as a bitmap asset that means it will be counted twice it means that the user collateral will be larger than it really is and therefore we could borrow more money than we should and therefore we can drain funds from the system fortunately this bug was found by a white hat so no real damage was done um notional had to pay the maximal uh Bounty amount of 1 million USD but no real damage was done the interesting thing is that these invariant I have shown before is pretty close to the correct one the correct one the fixed invariant will look something like this actually looks simpler in this case and the interesting thing to see is that if we run this invariant on the buggy version of the code we get the exact same counter example where you set one token as a bit of currency deposit another token then move the Bitcoin currency to be the other active currency we get this exact counter example notional use some of the top Auditors in the field and formal vacation and missed it however it's interesting to see that if they use funnel verification correctly they could have caught this critical bug so not only can we catch the bug with the fixed rule version we can also verify the fix right because um the specification doesn't change when the code changes so we can run it again and more importantly this incident was a catalyst for Satora to invest in ways to catch bad proofs and ensure quality of specifications automatically and today you could have caught that um the buggy invariant was a tautology using the method that I've shown you before meaning that we just take it and require the we require this condition without having the precondition without having any operation we would have seen that this would hold because it's a dotology and therefore this mistake would not be possible with our tool today and we're still working on more ways to ensuring qualities of good specification and catching more possible bugs and and bad types of proofs to sum it up specifications are written by humans just like who it is and they're equally or even harder to write this is something you have to keep in mind you shouldn't expect your specifications to be perfect like you don't expect your code to be perfect therefore you should always check your spec it's good if other another person reviews it if an expert reviews it and also even better to use some automatic checks like we insert or provide you you should always suspect what the tool gives you like you would any other security tool when you get a bug it's always a good result because you can always check it and see if it's good or not however when you get a proof you don't have a good way to verify it and the best course of action is to be suspicious of it don't take it blindly and just upload your code and obviously we could have seen that writing the correct specifications you can still find bugs that are worth millions or billions of dollars thank you [Applause] I would like to take some questions thank you so great presentation um so it seems from from what you explained that um when you have a bad proof uh that is uh vacuous you can just detect it just with a coverage report let's say in which part of your of your specification was never reached so it's it's it's like immediate but when you have a tautology it's more difficult because you will need to remove let's say preconditions and removing precondition you can have like 10 preconditions you don't know which one perhaps a combination of this uh so what is what is your view on this is is it is it correct that it's easier to detect vacuums than tautologies okay so one thing I want to emphasize um the checks that I have shown you don't catch all types of acuities and not all types of tautologies just catches only the simplest types and I've chosen to present them to you because they're the easiest to explain in a 20 minute slot they're actually more involved checks that try to to to cover more and more cases we don't cover all of them currently it's an ongoing effort in sartora or in full verification at Large maybe it was not clear so I'm just gonna say something simple the removal of all the preconditioning operations is done automatically by Satora it's an automatic check so in that sense it's not harder so if I understand the question correctly you say how can I fix it which part of this statement causes it to be a tautology and that it indeed sometimes more difficult but it's something that you can do systematically say um your expression is an or expression you can check each part of the or independently and see which branch of the or is something that is always correct if something is always correct it means the entire statement is always correct therefore this thing causes ubiquity and this is actually a feature that's very close to production in sartora maybe I'm wrong it's already in production maybe I'm not so so keen on the details but it's really close to production if you have an implication same thing you can see that um maybe um the premise that's the part before the arrow that comes before the conclusion if it's something that's always false you will have a rule that's vacuous so depending on the structure of your conditions you can learn more intelligent things about them that can guide you it's still not perfect but this is something that we're actively working on there is time to another so thank you all