J1 PAIN 03 Jacob Eberhardt a toolbox for zkSNARKs on ethereum

good morning everybody I hope you can understand me well I have a little bit of a cold but I'll do my best for next 20 minutes I hope it works out my name is Jakob Eva Hut I work at the Technical University in Germany as a researcher and I'm here today to talk about Socrates which is a toolbox for CK snarks on experiment it was first introduced at Def Con last year and now we made some progress in development and and we like to update you so some of you may have heard of the projects others probably haven't so my plan is to first give you a quick motivation for why this thing exists then give you an overview of the tooling and what it does then I would like to talk about applications a little bit and in the end talk about our roadmap and what we're looking to do in the future so let's jump right into it here on the left side of the slide you see how transaction processing in blockchain usually works today so you have a transaction you sent that transaction to the network and then every node in the network processes it and that means react securing it to make sure that it's actually a valid transaction so that's what we have now now imagine if we had this on the right side of the of the slide where a transaction is sent to the network but instead of being processed on every single note itself it is delegated to a third node to an outside party and there it is executed the computation is performed and then the result and the proof regarding testing the correctness of the execution is written back to the blockchain and then only that proof is verified on the blockchain so the main part of the execution happens off chain actually okay can we do this and what does it bring to the table let's look at that now so what are the benefits of option processing if we can do it so scalability would be one thing if we can verify a computations unchanged cheaper re-executing then then we can fit more processing in one block essentially on the blockchain so that also means the block complexity limit does not apply in the sense as it applies at the moment there's also confidentiality or privacy as some people call it that means private information can be used without revealing it in that case if we have proofs that do not reveal anything about the data we work on off chain what our approach is to implement this kind of idea there's basically two one is true--but which is more of a computation marketplace and it works based on crypto economics so computations are delegated to an off chain party and executed there and then results are written back to the blockchain but instead of having a proof regarding the correctness of execution what they do is they provide incentives for others to prove that the people who posted the results were wrong and we do it another way here we use ck snarks we could use other mechanisms but at the moment they're not quite efficient enough for use in practice that would be CK starts and bulletproof which do not require trusted setup which is a charming property but they're not as evolved yet so there's still research going on there so we use CK snarks and let me briefly talk about what CK snarks are so that we're all on the same basis so CK star extent stands for sir knowledge 16 non-interactive arguments of knowledge and that's the type of computational proof that is short and non interactive non interactivity here means that I can simply take approve send it to someone who's supposed to verify it you can then do it without any further message exchanges so it's around one round of protocol there's zero knowledge that means they don't expose any information that went into the generation of the proof and another cool property we user is that the verification cost is not dependent of on the complex complexity of the off chain computation so you can have a very very complex object computation and still verified with the constant cost of on chain that also means though that very simple processing steps would cost more to verify on the blockchain with this mechanism than executing them on chain in the first place on that case we don't gain anything it's it's use case dependent what you actually prove from an abstraction standpoint is that you know a satisfying variable assignment for either in arithmetic circuits or rank one constraint system and as you see they look a bit complex and not good to deal with and that's essentially where Socrates comes in to provide a better abstraction to specify computations that can then be off chain and integrate them so how does the CK snark process work briefly on the left side we have a circuit or Anquan constraint system that encodes the computation in that case we have an example where we multiply by number two numbers and say it equals the third number very simple first we need to do a set up and that's the pain point which is not solved yet but there's ways to deal with it so we do a trusted set up once we have to trust the participant who does it or move to multi-party computation protocol if we do not want to trust a single entity and that generates the proving key and a verification key using the proving key I can then find the solution to the system and use the proven key to generate a prove that I correctly executed this computation and publish the result I sent these two things to the verifier and the verifier can then check whether i found the solution to the problem but the verifier cannot learn anything about the private inputs that I use in that case the verifier cannot learn anything about x and y he only knows set and that I know a factorization of set that's all he learns okay with the by center release theorem added support for ck snark verification that means three precompiled were added and that's elliptic curve education Edition and the parent check which is a kind of homomorphic cryptic wrap traffic operation used in proof verification but the big question remained for most people how do I use that that wasn't clear that's where Socrates comes in so the tool has the vision to provide a usable abstraction and tooling for a CK snark so that it can be used on blockchain more conveniently than specifying rank one constraint systems understand improve systems in depth and writing your own verification contracts in the theorem or whatever because that's quite tough to do it's supposed to support the complete process that means program code is specified and then it goes all the way until the proof regarding that program code can be verified on the blockchain it's built to seamlessly integrate with the theorem blockchain and it the another goal is for it to act as an integration platform because there's new proof systems evolving coming up and they work on the same abstractions so we could ideally in to create them also in here so that we can use other proof systems as a back-end and maybe move away from the trusted setup also there's new ways to specify circuits I've seen new approaches based on functional programming and it would be cool if we could just reuse circuits or programs that have been built and not work in silos so that's why it's also has a vision of being an integration platform so it comprises a high level domain specific language to specify computations in a way that's more familiar to regular developers than working with arithmetic circuits a compiler which transforms these programs into provable constraint systems and then further other tools that help along that way we see that in a minute okay the language is actually a quite simple imparative language the basic type we have is prime fumed elements and you can think of that as positive numbers they can be very large but always stay below a very huge prime number so just think of it as positive numbers for now and then there's imprinted statements assertions loops so the things you know from imperative programming languages also conditionals and functions okay and that's the I want to spend a little bit of time on that slide because that covers the overall process how the tool is used from a user perspective and what you can do with it so we start with high level code in the language I just told you we specify a program we want to prove and then we compile it and then we have so-called flatten code which is essentially not quite equivalent but close to a rank one constraint system which I can then use to do proofs on this flattened code goes into the setup phase and generates a proving key and a verification key based on that verification key I can directly export a solidity smart contract which I can then deploy to the blockchain to check proofs ok so that's what the tool already gives you smart contract you can use for unchain validation the flattened code also can be used to generate a witness and that essentially means finding a solution for the program you specified in the example we had that means for our system x times y equal set we just find three numbers that fit the system based on the witness and the proving key we can then actually generate a proof and that proof will be then delivered to the blockchain for verification together with the result of the computation so in our example x times y equals c that would mean we have a value for C plus a proof and that sent to the blockchain and can be verified with the verification smart contract which yeah what you see at the very bottom of the slide here ok I'm the on shape proof verification process so the proof itself it's rather small that's the succinctness properties of ck snarks it consists of with the proof system we're using at the moment eight elliptic curve points so that's not a lot it's actually quite brief and besides that there's the result the set in our case and potentially inputs we also want to expose to the public that could be for example we also want to expose the X in our computation then it would also be part of what is sent to the smart contract and that contract has a verification key included at seven elliptic curve points and it has a verify function that can verify proofs and also check whether the result is correct for the given program using the pre compiles that were introduced with Python or by Santiam at the moment with the proof system we're using that cost one point six million gasps so that's quite expensive and that's where I said it does not make sense to put very cheap very cheap object computations in that system there are new proof systems that get better there and then of course the the break-even point moves further down in terms of gas cost cost okay let's look at what we can do with it what can it be used for so on reddit about two weeks ago there was a post and there was a guy who wanted to give $10,000 to the person who could guess the correct permutation of a card deck with 52 cards that wasn't reddit so what what are the challenges involved here and why is it related to Socrates in any way so first that guy needs to pay the $10,000 to the contract and commit to a permutation of the car Tech by publishing a hash that's how usually commit to values and then as soon as they're published the hash can be checked on chain and you're paid out right but there's another challenge in this scenario and that's that you have to prove that you committed to a valid permutation without revealing the permutation because otherwise he could have just committed some hash that is not a hash of a valid permutation and there would never be solution so he essentially wants to show that there is a solution and this third part here is where Socrates comes in because what you can do with the tool actually so you check card validity you check card uniqueness and you hash the permutation and you return the resulting hash that's what you specify in a Socrates program and then people could check that there is actually a valid solution for the problem but they learn nothing but there that there is a valid solution to the program and that's checked on chain and a proof ok so what we found out looking at different use cases that are interesting oftentimes different cryptographic primitives are needed and that's a bit of a problem because we don't want to reinvent the wheel and implement all types of hash functions and encryption functions and stuff in the domain-specific language because that's painful to do it takes a lot of work and there are already implementations of that kind of stuff so what we focused on now is helping with integration of these primitives so we get hash functions encryption functions all that kind of stuff to the platform and can potentially have community contributors help out there so we can focus on the main platform maybe move to other proof systems but still enable use cases for that we implemented mother returns rank one constraint system importer and better semantic checks and integration tests so you can make sure the things actually work more conveniently now I want to talk about a couple of other applications or things you could do with it that come to mind so what we talked about a minute ago was where I I was proving the knowledge of a secret what I can also do with a tool like that is prove for example that I'm a member of the group without showing which member of the group I am it's also something I can do so generally fact some private data without publishing the private data is one use case what's also quite interesting for some applications is that I can do very brief Merkle tree membership proofs instead of using traditional merkel proofs where basically if I want to prove that D is part of the tree with this root ash I have to supply this and have to supply this and the larger the tree becomes the larger that prove that miracle proof also becomes so what we can do now because certain other fruits have fixed size we can just show that D oh sorry that D hashes with other private values which I don't even have to make publicly known to this root hash and that's just also a regular certain other proof and that becomes a very brief and that can be very interesting for on chain applications where hashing along a very long miracle path is extremely expensive to do in smart contracts you can implement shielded tokens like C cache as far as I know there's a couple of people working on that on on top of the theorem now and also a cool thing you can do it's a bit more abstract is you use the blockchain for what it's very good at and that's unchanged state so state is what block chains very good at because they're you know the data availability problem with all data that's off chain and you don't have that on chain by by definition so that's why probably a lot of state needs to be kept on the chain but state transitions all we need to know about state transitions is that say that they happen correctly there are no mistakes being made and they're valid so what if we kept the state on chain but made the state transition functions off chain and only showed that the state transitions that occurred were valid according to protocol then that would also law offload quite some work from the blockchain and that could also be a cool application here for Socrates a bit of a road map and where people could contribute also we're actively looking for for a bit of help here because it's basically a research prototype and we have some people who started contributing so if you're interested please feel free to talk to us and see where you can maybe help or fit in so big topics are integration at the moment that using all the or bringing together all the silos that have built up that all generate maybe rank one constraint system from different abstractions we're currently trying to agree on a rank one constraint system standard with a couple of people from C cash from credit and other guys I hope this works out we have a traffic person so that's good that can be imported also we look at other proof systems I think the next step would be to move to the cross 16 snark which makes the proofs much cheaper to verify because there's the the pairing checks reduced and the proof size also comes down and but it gives essentially the same guarantees we look at integration of a prototype of a distributed set up phase like C cache performed off chain but with support of an on chain coordinator as a smart contract essentially also we look at new proof systems they're a bit tough to use at the moment because the proofs are still quite big and with that not optimal to verify on chain but the cool thing about these new systems like bulletproof is they do not require trusted setup which would be a big step forward I would say and regarding the Socrates language there's also work to be done type extensions comes to mind here with that I would like to conclude my talk thank you very much for your attention and please feel free to try out the tool create issues in case there's any bugs or generally reach out if you're trying to contribute or want to use the toolkit thank you I was just wondering about that setup phase and whether that's something that's dealt with like by the individual user or is that like like compiled into Socrates already somehow and if so how in what way is it okay so about this setup here it's it's in Socrates so the setup operation that's command line operations you see written down on through here allows you to perform or trusted setup locally on your note so that might be fine for some users and some use cases but might not be fine in many other cases where you do not trust a person that you know you you interact with via the verification smart contract in the end so for that case that's what I was talking about in the outlook we're looking at distributed protocols to better work with with setup protocols that need only one participant out of a whole troupe to be honest to them be completely safe there is a cool new protocol by the C cash guys they're currently in the first phase of that protocol powers of tau but the problem with that is that they use a new elliptic curve and Ethier does not have two precompiled that are required to work on or two valid approves on that elliptic curve so we currently cannot use this setup phase done by C cash for the the proofs on the theorem so that might happen in the future I don't know what the foundation standpoint on that is I don't know yes so you mentioned one of the potential uses was being able to turn things like Merkel proofs from a login and 201 basically is where would you estimate the trade off pointers or the break-even point is there how big does your seat have to be for it to be more efficient to do it this way so I have not tested it but I talked to chest and trade recently who kind of had the idea and context of stateless clients and what we tested is that generating the proof took five seconds for Merkle tree of depth sixty four and I think in that case it's already a much shorter proof than having the many hashes so in that case it would already the prick of would already have happened so a miracle tree of depth 64 could enumerate every sound great on earth which is a bit of a large cap do you know like roughly what you're talking in terms of gas for verifying something like this so does the case not clarification is always equally expensive 1.6 million gas F naught I don't know how expensive it is to verify it on chain at the moment just using hashes and going along Myrtle path I have not tested it cool thank you hello I have a question which is probably related to the trusted seller but assuming that desert transit set up that happen how do you 75 versus equity itself because once you just commit to the affair on blockchain were verify your spot contract it just going to call a verify method that's in fact just an arithmetic circuit how do you trust that it does verify what you want because if anyone can set up a provocate how do you know that there's not even a bug in the compiler and verifier doesn't have loopholes how do you certify that I'm not 100% sure I actually got the question but let me try to answer anyway so the the setup phase happens specifically for one program and both of the outputs the verification key and the proving key they become public and the secret itself is quite hard to audit because not anyone can just look at the admitting secrete and says yeah it does verify an elliptic curve ad so how do you convince people that the secrete really does add points on the elliptic curves and that the verification is correct without just first testing or all inputs okay maybe there's two aspects so the verification key and the proving key they belong together very specifically and you can never create unless the setup phase was compromised which we assume it wasn't you can never create a prove regarding the execution of another program that would be verified by a verifier for a different program so a part of the check that happens in the verification smart contract is to make sure that actually the same arithmetic circuit was used so that is explicitly checked as part of the verification so I think what you sketched out that cannot happen but still still even if you're using the right imma take secret how do you know that this secret does the job you want it to do you have to trust the higher-level Socrates longer age and of trusted the compiler okay as a secret are you essentially asking whether I should trust the trusted setup because I have to trust not really the not Reva setup but the execution and verification because it's not it's not normal code that computer scientists understand by just looking at the code it's an arithmetic circuit so how do you know that an eidetic circuit that is supposed to check that a balance value is in a range really does check that apart from sending random inputs and convincing yours yourself with enough input but so what I'm not sure what you could maybe do is you distribute Asarco test code files every one compiles them for themselves and because it's deterministic you can check hashes on that and compare that maybe but I think that's a very general problem in computation and not specific to this system but if for example you have a secret that verifies that the balance is a data number is not more than a hundred thousand and if in fact you just in the secret you've a sacred just verified that it's not more than a 90,000 most people will think it works because on the input data still it works but in fact it doesn't that there's a kind of backdoor in there you say with every program right if the compiler does not work correctly if the compiler has box then what you execute is not what you specified so in that case of course you trust the compiler as you trust every compiler and we need to make sure it works as intended so all you could do to make sure is maybe then test it or something or for now trust that that is correct okay thanks okay we're out of time thank you very much [Applause]