Lita│Pushing the Performance and Usability of Zero Knowledge Proofs│ETHDam 2024

[Music] awesome thank you for being here and now we have Daniel hi everyone um I'll be filling in for vental today I think she was on the program um I'm here with the Lita foundation and uh we'll be talking about valid our zero knowledge virtual machine and how we're using it to push the performance and usability of zero knowledge proofs uh is this the how do I click uh oh um is this the clicker am I am I doing something wrong should it's not pluged in oh yes of course it's a spin manifold keyboard set up there we go great um so yeah um here's here's an outline we'll be talking about virtual machines in general uh some of the different types some of the limitations with um some the other virtual machines on the market today as well as what we've done at valida to create the fastest VM out there and a little bit about the future um so the motivating question is how do I prove succinctly and in zero knowledge that a given program was executed and that the um gave the correct result so importantly this is supposed to be a universal thing right um a zero knowledge virtual machine will be a zero knowledge um a zero knowledge circuit that can prove the execution of arbitrary computer program specified in some given language um the Key Properties we need are succinctness and zero knowledge um succinctness proofs are not too long um can be said differently in the context of a virtual machine that it should be much faster to verify the proof than it is to run the actual computation zero knowledge this is the key property for privacy right um the proof should reveal no information on the internal States of the machine in the course of creating the of running the computation uh so this would include any private input such as secret keys or you know um transaction amounts uh account addresses something like that that you would use inside of the of the machine um these are wonderful pieces of cryptography that are really pushing the space forward however right now Zer knowledge has these two major problems one is that it's it's a technical subject a lot of the tooling um even that's supposed to be developer friendly it still has a pretty steep learning curve as well as the proofs themselves are large and um or sorry they're not large that's the key property the proofs take a lot of time space and energy to create so even though they're really fast to verify the cost is um when making the proof yourself it takes a lot of time to do so right so we hope one day that we could do something like generating these proofs you know totally client side on your phone or something uh but this is a challenging thing to do right now this tooling is is rather slow um so here is a wall of text on uh some of the different high level approaches to creating these virtual machines um so maybe ignoring some of the details on the slides here but the um the big idea here is like what do we mean to specify a computer program right um everything from you know C to Magic the Gathering is tur incomplete so the property of being Universal isn't very specific um and there's there's sort of two ends of the spectrum here one would be to have a domain specific language um a well-known example of a project that does this is Cairo and this can be thought of as um a sequence of macros that lets you create zero knowledge circuits directly uh this is good for sort of fine-tuning of performance but is bad for the difficulty of use um as well as it's a little bit harder to reason about the uh mathematical correctness uh so this is you know a common a common dichotomy in uh programming outside of the Zer knowledge context where low-level languages let you get performance really correct and highle languages let you specify um you know the correctness of execution at um at a level that's easier to reason about and the approach we take with valida is this third one um so here we Define a virtual machine with an instruction set architecture like an actual processor has um ours is extremely simplified so only a very small number of instructions uh and we compile from highle languages to this and then this is what we actually Implement in zero knowledge the you know State transitions memory loading and stuff for the virtual machine itself um and we hope that zkv will be the dominant way in which developers will use zero knowledge um and this will help with increasing productivity as well as avoiding security flaws uh zero knowledge is a complex subject there's a lot of difficult cryptography involved and we don't want everybody who's building a privacy application to have to start from scratch and do this um so with the zkv m you can write your code in a language of your choice compile it run it and prove it in zero knowledge um and so you can get all the benefits both the privacy and the scalability coming from Zer knowledge without needing to do the cryptography yourself um so there's this is a crowded space right now there have been a lot of uh VMS just this year uh however we think that many of them have some some real problems that we're trying to solve um as I mentioned on the previous slide a lot of these use a domain specific language that has a uh steep learning curve for development ERS uh both in terms of the language itself and sometimes things like you have to have um absolute bounds on number of repetitions in a loop memory is uh structured in an unfamiliar way you know so it's not just a superficial difference in the language it's actually a a really unfamiliar programming Paradigm um also several of the other uh virtual machines out there have you claimed to be open source but uh then have closed Source component for example proof aggregation or generating the constraints for the virtual machine itself um and another thing that uh is really important is to have builtins um you can think of like the ethereum pre-c compiles but in the ZK setting uh for cryptography operations like signatures or hashes as well as blockchain operations like evm transactions um then finally the sort of most important thing that we're trying to solve is that many of the virtual machines that exist today are still not nearly performant enough to be able to be used at a large scale um and some of the reasons for this are the design of the machine itself is not tuned for um Optimum performance in zero knowledge circuits but rather for you know familiarity or you using a um instruction set that exists in ordinary electronic computers um finally we want to make sure everything is very extensible so that you know there's been a new crypto paper on this subject like every two weeks um that changes everything so we want to be able to keep Pace with these advances so extensible performant and developer friendly um here's a kind of schematic of how we went about this so we start with the cryptography um choosing a proving system that has the optimum uh set of trade-offs uh so there's generally a trade-off between proof systems that have really small proofs and proof systems that have really fast provs uh and there are some tricks for combining those then uh the virtual machine itself is uh we call it ZK friendly instruction set architecture so uh we take a really small really simplified model of a computer processor and we compile everything to that um so an important part of this process is step three to create good compiling tools that let you take a program written in a high level language like rust high level in this context um and have something that can be proved in our system uh so this kind of lets us lets us have our cake and need it to with the uh choice on one of the previous slides that we we use a um instruction set that's tailored for zero knowledge to give us really good performance but then we also create the necessary tools so that developers don't need to use anything unfamiliar to work with it um finally these last two steps are a little bit more forward-looking but we want to have um use Hardware acceleration ranging from gpus to maybe fpgas or as6 one day to um really boost the performance as much as possible and then finally we want to use formal verification for all the key steps in the process um you know the idea is that uh this zero knowledge virtual machine might one day be the main engine that powers some large scale zero knowledge uh rollup or blockchain that could potentially have you know a whole lot of money on it so we want to make sure that every key cryptographic piece of it is not just audited but formally verified in the sense of uh formal theorum like lean um okay I'll say a little bit about the the the design some of the choices we made to get the performance that we have um so we can think of this virtual machine as sitting in between a prover and a compiler um so the compiler takes highle language spits out something that our virtual machine understands and then the virtual machine creates um a set of constraints uh you know some mathematical model of computation that's far away from how you normally think about it and this is what's actually proved cryptographically uh so a key part here is to make sure that we use the most efficient instructions possible uh for example we have special instructions to do finite field arithmetic in our instruction set and we um remove most of the registers to simplify the the CPU itself uh and then on the compiler side we have to replace calls to instructions that we don't have with sequences of equivalent ones that we do um so at a high level we divide our system up into into a set of chips uh so we have the main processor one for memory one for um binary arithmetic as well as uh a couple more specialized ones here uh and then the the cryptography underlying it is Starks and specifically Starks over a small 31-bit field um this is a schematic of of what I just said so we right here is what we're proving we separate uh readon memory for the program it's a Harvard architecture um you can't edit your own code a big RAM and um input output and these these communicate through a series of buses with this set of chips Each of which is a separate um zero knowledge circuit um so we do not have any general registers the only registers we have hold the program counter and the frame pointer so these tell us where the instruction that we're about to execute is as well as where the uh local variables are stored we can address Ram both uh in relative and absolute modes can't address ROM at all uh so this is you know a very different construction than you usually have with an electronic computer and that's because there's no notion of fast versus slow memory and zero knowledge right and in an actual physical circuit then you want to avoid uh addressing main memory as much as possible use caches use registers because their orders of magnitude faster and that concept just doesn't translate here so the uh Notions of processor that work in the general electronic model are not the right ones to use for zero knowledge um yes a little more about this we don't have a stock pointer we so our stack frames are constant size and anything that doesn't fit in that just go onto the Heap which again is really no more expensive to use than anywhere else um so when using the VM you'll first run it through the execution engine so this is the actual virtualization you take your your software you run it and you record an execution Trace so all the intermediate values used to um generate the ultimate value of the computation and then you prove that you have this execution trace this is the cryptographic part and then this proof uh can is succinct and can be verified cheaply uh later on by by anyone for example onchain um one key thing that makes our system fast is that we use this baby bear field it's a 31-bit field and because it's very close to a power of two the arithmetic in this field can be done really quickly in actual physical Hardware you know you um you need to constantly be reducing mod P and doing that is easy because p is very close to a power of two um however this field is too small for cryptographic security so the actual cryptographic challenges come from an extension field um and then the the system that we use to commit to polinomial the core cryptographic primitive is fry uh this is what's used in all Stark systems and is really um by far the fastest polinomial commitment scheme out there today uh so when all execution Trace is uh separated into one for each chip each of these is a separate zero knowledge circuit and then we later uh prove the correct execution for each chip and then later on WE prove that the chips have compatible views with one another uh so that the for example the processor chip and the memory chip have the same view of all of the uh loads in stores um we okay then to actually do this cryptographically we represent these vectors as polinomial using interpolation commit to these polinomial um and again with this we we do what's called a permutation argument for this compatibility check so given all these single variable pols uh one representing each sort of column each variable uh over time we uh combine them in in a constraint equation to get a single polinomial and then we show that it vanishes on the correct domain uh so this is this is the setup that is used sort of throughout the zero knowledge literature uh so maybe let me not say a whole more about that um one key fact is that we uh require constraints to have degree at most three because constraint degree is a large driver of cost um again we're using this baby bear field uh we might one day uh be able to use the maren Prime field using some uh recent advances in the Stark literature this field has even faster arithmetic because it's literally just one off from a power of two um a main part of our project is the compiler as well uh so we we can compile from llvm to our specialized instruction set uh here's a schematic on what that compiler pipeline might look like uh but again right we use ordinary programming languages ordinary compilers to generate the llvm intermediate representation you know this is something you can do with with the compiler that's already on your machine for your language of choice and then we have um a series of further optimizations before we get the thing that we actually prove um so here's our GitHub you can download it now you can um write your own uh chips and have them generated at compile time to get a machine that has you know the exact operations that you want optimized and everything is fully open um we welcome outside contributions uh we have an aache MIT license and uh I think I won't have time for for this demo here's a little mockup of what um the developer interface might look like so something like GitHub Pro but in zero knowledge uh we have an early Access program so if you'd like to build with valida right now all of our code is on GitHub and um we would absolutely love to talk to you to support uh integration we're hiring uh across you know as every one is uh cryptography compiler Engineers as well as product people and um not necessarily employee open source uh cont contributors uh here's our contacts I'm tessera um our founder is Vali we'd all be uh really happy to hear from you awesome thank you so much um and well we yeah we can leave this one up um and if we can have the lights up and do we have any questions we're good all right well thank you again Dan we really really appreciated it thank you and so that is the end of the programming at this stage you can still head downstairs for the conversation about regulation Innovation and then after that there will be a debate about uh scaling so [Music]