Medjai: Verifying ZK Smart Contracts

Transcript

[Music] hello hello okay hey everyone um all right let's get started so I'm Jacob I'm a researcher at veridice and today I'll be telling you about Magi one of our formal methods tools we've developed for zero knowledge programs first off let me concretize what I mean when I say formal methods because this term refers to a wide variety of different techniques we consider formal methods to describe any technique for automating reasoning about the correctness of programs

along the Spectrum from left to right these automated tools can provide stronger guarantees at the cost of more human effort and to be clear when I talk about formal methods in this context I'm not just referring to a single technique or tool on this slide instead I'm referring to a class of techniques including systematic testing stack analysis and formal verification for our specific domain in this talk which is zero knowledge smart contracts we use formal methods for the purpose of both finding bugs and constructing proofs about the correctness of programs indicating a lack of bugs for example automated testing has proven able to uncover bugs that handwritten

tests are not likely to find while formal verification can prove guarantees about code correctness today I'll tell you about Magi which sits in the formal verification bucket at verdice in general though we also make other tools for both static analysis and automated testing over a variety of domains let me give you a bit more detail about Magi specifically Magi formally verifies Cairo smart contracts by using a formal methods technique called symbolic execution given a Cairo program and a high level specification written in a language called V ijay either reports that a program fully satisfies the specification or reports

that the program failed to verify with an explanation of that failure this explanation comes in the form of a concrete input that causes a bug the main downside to using Magi here is in the complexity since Magi must reason about all possible program executions it's possible for Magi to encounter pathological cases for which generating a proof is very challenging uh time permitting though later on in the talk I'll uh show you a small optimization that mejac performs in order to actually scale to these pathological cases in practice now to understand how Magi is useful practically let's take a look at the

transfer function you see here written in the Cairo language at a high level we want this transfer function to increase the destination balance and decrease the source balance by a specific amount and abstracting even further we want the balance of destination to increase in the balance of source to decrease it makes sense for a transfer function so um to use Magi we can write a specification that says exactly what I just said in English and pass it into Magi along with this program we'll run it and for this case menji actually finds that that the specification does not hold when it does so it will give an example

indicating how the bug can be triggered understanding this bug requires a bit of understanding about how Cairo specifically represents uint256 values since Cairo is a language for zero knowledge smart contracts it uses a field element data type as a primitive called a felt here field element data types are integers in a field whose Prime is about 2 to the 252. so you'll notice that it's not quite big enough to hold the unit 256. instead Cairo represents unit 256 with two Felts one for the low bits and one for the High bits and here you might see where the problem starts to arise they're actually U int 256 values that

are invalid specifically when either the low or high bits is greater than 2 to the 128. however the subtraction and addition functions you see here actually assume that the amount is well formed thus media can find a counter example by creating an ill-formed un-256 and in this example this is not something that the developer realized initially however using this counter example Magi or sorry using this counter example the developer can actually adjust their code and fix the bug then in order to determine that their fix was actually correct they can take that same specification they had before and re-run Magi

in this case the bug is actually fixed so Magi reports that the program is verified and in this case the guarantees here are a bit stronger than the guarantees you would get by running a fuzzer and not finding any bugs it here Magi is saying that for this specification there are actually no inputs um that invalidate the specification okay so that's it for the overview but in the rest of this talk I'm going to highlight three key components of Magi first we're going to talk about how to actually specify correctness in the v language second we're going to talk about how symbolic execution works at the core of Magi

and lastly if we have a little bit of time I will briefly discuss an optimization that Magi uses all right first off let's talk about how Magi uses how mengi users can actually specify correctness users specify correctness in a language called V which is a declarative high level language designed to Paradise for expressing program correctness across a wide variety of applications uh because of these goals V is both blockchain and language agnostic meaning that these specifications can apply to this wide variety of applications perhaps even more importantly these features mean that our tools

um can take uh specifications in v and um sorry this means that our users can write specifications in v and apply them across our various tools for example if you write a specification in V to use with Magi you'll be able to immediately reuse that same spec to run our Cairo fuzzing tester so how do we actually write uh specifications in v well specifications in V are written using in the form of statements statements are composed of three parts an action a Target and a property actions specify uh what program behaviors should be considered in the specification

for example the action called finished specifies that only transactions that complete successfully should be considered second targets tell the tool which transaction to execute in our previous example this would be the transfer function finally the property itself specifies the condition we want to check or the desired state of the blockchain after the transaction slightly more complex properties can be described as pre and post-conditioned pairs these two conditions are properties that should hold before and after the transaction respectively more specifically the specification here asks the following question assuming the precondition holds before

the transaction does the Post condition hold after the transaction executes according to the action now let's take a look at how we can use V to write our specification from the previous example for the Post condition here you can see that we basically copy and paste what we had before very straightforward um and very similar the action we want to consider here is going to be finished because we want to consider successful transactions and probably obvious to most of you the target is going to be transfer because we want to consider the transfer function but we can actually add a bit more detail by using that pre and post condition condition structure I showed before

specifically we can consider an arbitrary address called other and say that this other address should be distinct from both the source and destination in this case the transfer function shouldn't affect the balance of other at all as we specified here and that's it for writing V specifications so now I'll move on to how some block execution works so for understanding symbolic execution I'm again going to use that same example from before and we're going to start with just how a concrete execution looks so I'll try to go pretty quickly because I'm sure a lot of you understand how concrete program execution works specifically we're going to start with a starting state that I should just show a

snapshot of here and we're going to go step by step through the program so first we'll check for the validity of the amount sure enough this amount is valid so we're going to step to the next state once we reach the block that subtracts amount from The Source we're going to perform that by updating the state here you can see that the balance for Source has been updated and then lastly the block that adds adds amount to the destination balance is going to perform very similarly we're going to take that state that we got before and update it and now that we're at the end of the program what we get is an ending State pretty straightforward so symbolic execution is going to work

in much the same way except instead of concrete numbers you saw there as part of the state we're going to use symbolic values these symbolic values represent multiple concrete values that could be in the state at runtime and importantly though these values are symbolic the actual types of the state variables still maintains uh still stays the same so what do we do now with this symbolic State starting execution well when we perform this check for validity if the amount is not valid we stop execution so when we update our state we include now this precondition that

says the amount should be valid and why do we do this well it's because if the amount was not valid we would not continue along this branch of execution in general this path condition or pre here I call it a precondition I'll call it a path condition from now on it describes the properties that much must hold to reach this part of the program with this state we can continue in a similar way to concrete execution here but we perform these operations over the symbolic values of the state here we perform the subtraction on the source balance using our symbolic amount

similarly we're going to take the result of that subtraction which is our intermediate State here and plug it into the next block the addition which gives us uh this final State here with both the balance and with a balance for source and destination updated based on the amount after we do this and get our final state we can check the post condition of our specification with an existing satisfiability solver specifically we'll ask this solver if any instantiation of these symbolic values can possibly invalidate our

property if not then we know that there are no bugs with regard to the specification okay in the last minute or two uh I'll briefly go over uh an optimization that Magi uses to scale and practice in the previous example you might have noticed that the program we were looking at was fairly straight line code however let's consider how symbolic execution handles the branching program to the left we'll first consider the case that takes a branch and update the state like so then separately we have to consider the else Branch so the state's not updated following from here we need to handle the second if for each of these cases

which means we Branch based on the first state and We additionally Branch based on the second state as we continue you can see how the number of possible States we must consider grows exponentially for this reason Magi takes advantage of an optimization called State merging specifically after a branch Magi merges the two resulting States into one symbolic execution can then continue from this point and you'll notice that the state here actually gets a little bit more complex so the solving time may increase a bit but it's worth the trade-off to avoid this exponential blow up in state exploration

and that's it for Magi and how Magi scales to real world programs so please let me know if you have any questions all right one two hi nice talk uh what's status of Magi development because in the last 10 months we you don't have any activity on GitHub and uh your examples are about Cairo zero what about Chiron yeah that's a good question so uh we have a both public and private version of Magi right now so figuring out how to schedule updates for that

um is uh definitely a point of interest and yeah you are great to notice that the examples I gave are Cairo zero um that made it a little bit easier to show the examples but Magi actually works at the um bytecode level and this stays the same through Cairo 1.0 Cairo 2.0 so Magi still works for those uh new versions um it is true that the new versions of Cairo some bugs might not be as likely for developers to write because I mean it's just a little bit easier to program but fundamentally the same properties uh that I describe still hold thanks for the question any other question yep thank you for the talk is your Technique

sound for programs with loops yeah that's another good question so for programs with loops uh symbolic execution is gonna differ basically you can't use symbolic execution if your Loop is unbounded right for example if I take in an input and I want that input to be symbolic and I also Loop based on that input you're not going to be able to uh complete symbolic execution right um however if you have loops that you can provide a concrete Bound for then this technique will be able to scale and will

be sound thanks for the question somebody else yep we'll have to help me out thank you hey thanks for the talk um can you comment on the expressiveness of your language and uh how much did you manage to have developers writing specs um specifically the so just to repeat the question uh how expressive is the the specification language uh and the answer is uh We've designed the specification language to be uh as expressive as possible um the goal here is that programmers

should be able to express um any type of functional correctness additionally what I didn't describe here is that V also allows for temporal logic to be expressed the reason I didn't mention it is because this is not something that Magi supports but it is something that other tools that verdice is making does support so yeah to answer your question developers are able to write V I think in a in my opinion in a pretty straightforward manner but obviously I'm a little bit biased and we've designed it to be as expressive as possible yep all right

can you express interactions between multiple transactions so can you somehow change the transactions and have a state followed in between them yeah that's a really great question and um I that's not something I elaborate on the talk just for Simplicity but you saw how you can have a single V statement with the action the single transaction and the specification um or sorry the condition right if you want to express what you're talking about um multiple transactions in sequence all you do is use multiple V statements in sequence any further questions oh

all right thank you then yeah thank you [Applause] [Music] foreign [Music]