Formally Verifying a Shielded Pool in Lean 4

Transcript

[music] [music] >> So before I really get into this talk, I want to sort of give you some form of disclosure. Oscar from our team was supposed to present this, but unfortunately he couldn't make it to India. So that's why I'm stepping in for him. And when we submitted the CFP for this, we thought it would just be lean four, but when we actually started formally verifying a lot of our shielded pool implementations, we noticed that that was a very one dimensional way to view things and there are a lot more components that need to

be formally verified as well, including off chain systems, etc. So I'm going to start with explaining the lean four side of things and then explain how we had to formally verify other parts or other components as well. How sure can you be that a confidential system does what it says it does? So we took one of our own, a shielded pool for private transfers on Ethereum and pushed formal verification as far as today's tools reach from written spec down to the bytecode running on the testnet.

This talk is about what that bought us, what it cost and where it stopped. This isn't just about the smart contract. We also take a we also looked at the circuits, the hash, the verifier, the wallet, the deployment and the spec that all supposed to follow. We designed this presentation for an engineer that is supposed to be shipping a pool like this or an engineer from a financial institution that wants to know what guarantees shielded pools have. When each systems launched, we published an article that said we are past crypto's YOLO phase and this is what we believe the next phase to onboard institutions onto

Ethereum. There are several kinds of evidence that a piece of software says or does what it should. They cost different amounts and catch different things. There are five of them, but we can be more exhaustive as well. Tests check the cases that someone thought of or even an agent might have thought of. A review or an audit adds independent eyes for a bounded time. Then you have a specification that writes down what the system is supposed to do.

You have a reproducible build that ties the bytes on chain to the source you read or to the tool tool chain that was used. And finally, you have formal verification, which is the most expensive of these. You state properties as mathematics and a machine checks a proof that the program or a model of it has that property. A test suite rarely tells you about the rule nobody wrote down. A proof about a model will not tell you that the deployed by its other ones that you prove things about.

You want more than one of these guarantees and you want to know which evidence each guarantee rests on. So we are going to explain how far today's tools get on one real system and what we found along the way. Verification needs a statement of what a software should do. So ours is a numbered specification written way before we even generated the proofs. Spec two, as we call it for shielded pools, describes a pool for confidential payments against the ERC 20 token interface, which permission token standards expose as well.

You deposit tokens and get a note that only you can spend. You transfer notes privately and you can withdraw them out of the pool. The requirements are numbered and written in must language so a reviewer can point at point the clause at a line of code that has to be satisfied. The spec states its trust model, threat model and compliance boundary. So an engineer, an auditor and a regulator can each read the same document and find what they need. The spec holds the system's meaning. Explicit requirements do not automate verification though.

Translating spec to model is still a human reading. When we started, nothing was machine checked. You have several properties of the system itself, which is confidential confidentiality, unlikability, no double spend, value conservation and selective disclosure. In this effort, we focused on the two core aspects of shielded pools, which is the no double spend and value conservation. Because if you get either of them wrong, someone could mint coins out of nothing or even spend certain assets twice.

And the reason we did this is because it actually happened in the past this year. So in 2022 Zcash's orchard pool activated and there was a flaw in the circuit from day one, but it was only detected this year. It was found by a researcher using an AI model and a custom audit harness. [gasps] In May in July Ion would followed with the circuit proved in lean and a concrete knowledge soundness bond. However, it is valuable to know that the flaw lived in the circuit, but not in their model itself.

A ledger theorem would not have seen it. Value conservation is what broke. It is part of why we started this whole effort of formally verifying our shielded pool implementation. And not to throw shade on the Zcash team, but they are really smart people. And if something like this got through even their human review and their extensive processes, then I think it's very possible that the rest of our systems also have some bugs in them and we should be looking at it more carefully.

I want to talk about how a withdrawal looks just to explain all the steps. So you have all the things that are filled in that are formally proved and you have the the light fills being things that have been checked and the ones that are dashed are outside the claims that we had when we were building the formal model for this deployment. So to go very quickly, the wallet holds a note and builds a proof that a proof with the withdraw circuit.

The pool contract asks the verifier contract, checks that the route is the one it recently held and the nullifier is unused, then pays it out. The Poseidon hash is the one piece that both the circuit and the contract use. Here we assume that the hash has no collisions. The verifier rejects false proofs and the contract behaves as the model says. These three will come back towards the end. So the model that we came up with is a small exact restatement of the rules, essentially translating the spec to lean.

The three flows that we focused on were deposits, transfers, and withdrawals. Deposit locks tokens and mints a note and the commitment that it generates must be new. Transfers spend two notes and mints two and the amounts must balance and value must be conserved. A withdrawal spends a note and pays out and the nullifier must be fresh. There are certain simplifications that we took and all of them expanded how we thought our system was built.

So let's look at actual lean code and translated to what it means in English. So for every set of supported tokens, every history of deposits and with transfers and withdrawals and every end state. If the pool starting empty accepts the history and ends in that state and no two notes or keys in the history collide and no note then that means no note in the history is spent twice. So that's the first theorem. The second theorem of value conservation has the same shape but ends differently.

Instead, we have the ending as for every token deposits equals withdrawals plus live value. Think of a note as an IOU with a secret serial number. No IOU is cashed twice and the books always balance provided no two IOUs in the history share the same fingerprint and no two keys open the same lock. So what does this proof actually rest on? We checked what code was generated in lean and the answer is lean's three standard axioms and nothing else.

The hash assumption is a premise of the sentence written into the statement, not an axiom underneath. So what does that premise actually cost us? It is the collision resistance of the hash restricted to the history at hand and we did not prove it. Whether Poseidon has that property at these parameters is a question for cryptographers and a bigger one than what we've built right now. So how do you believe a proof that was written by an agent that you actually did not review as much?

You can review a script that sort of executes or checks that all the proofs are complete and that would fail on any unfinished proof or any extra axiom or any changed statement. So we have a simple gate script that you can run uh which makes sure that planted cheats a sorry a smuggled axiom or a weakened statement are [clears throat] definitely caught. However, there are some issues that we found while using these verification tools.

So I think in the future slides I'm going to explain what bugs we found in the verification tools and how we fix them. The same table that I explained earlier, but now it looks like this. Two guarantees gained which is machine checked model beside tested for the no double spend property and the value conservation property. So anyone reading the spec can see what was proved and under what assumption. The level is not just machine checked, but it is machine checked model and that word in the brackets is the point.

And because of that we expanded what the CFP was for for this presentation because there was a lot more that we had to implement than just lean for. So what machine checked model actually means is it covers no implementation, doesn't cover field overflow, two encodings of one nullifier, circuit wiring or merkle tree binding. And if you look at that then what did we actually end up doing, right? So after we noticed that we had to ensure that we formally verified different components of the entire stack.

And to do that we had to be really selective about what was the critical path and I'm about to explain which parts were critical. So our circuits were written in Noir and we had our contracts written in Solidity, a generated verifier from Noir and EVM bytecode also. So each needed its own tool to be formally verified and here we have some status words. So proved in part, proved, checked, checked in part and checked.

We prove properties over the compiled form the prover runs. So every assignment that satisfies the compiled constraints has amounts in range, transfer inputs summing to outputs without wrap around and managing matching the token fields. The compiled circuit proofs of the sum rules are the layer that looks for the Zcash flow and value conservation is what it broke. The hash and Merkle equation stay outside this root and the translation of the constraints into lean is trusted.

We also proved that the hash across various implementations matches. So essentially we improve the trust model here as well. We also checked the verifier that was generated by Noir. So regenerating all three verifiers with pinned tool chains match the committed files identically. So there were again some simplifications that were made and that's all explained in slide later.

So we have to look at the exact gap between the contract and the model. The model has three atomic operations over lists and natural numbers which what's which is what makes the theorems even provable. The contract however has loops fixed with words and external verifier and external hash, a Merkle tree it updates in place callers gas and an owner. The model extra abstracts all of that away so the contract could diverge from it at any of these points.

I think continual formal verification of production systems something that is still being explored and would definitely require a keen eye to make sure that the model and the actual implementation don't drift too much. So here as I mentioned all the premises are written and named none have been proved for production and a toy instance shows that they can all hold together. There is another drawback here as well.

So the lean theorems say nothing about who can change the actual on-chain verifier. So if your shielded pool has a mutable on-chain verifier that an owner can modify then they could drain the pool which sort of invalidates the invariance that you're working with in some cases. We did find few bugs with the verification tools themselves and in our actual implementation. This well-understood pool had reviews during development and agent run audit we triaged and fixed and adversarial agent spec review and a colleague's peer

review. There were a couple of critical bugs that were discovered before we even started the formal verification effort but right now after being formally verified we expected no severe bugs and found none. There were three bugs in the pool that were relatively minor which is a route was banked mid transfer which is an intermediate state in the tree itself and there was a skipped range check which was fixed and there was no verifier time lock.

There were some bugs that we found in the verification tools like lamp and EVM Smith. Two of them have been patched upstream and one of them is still open. So the theorems were the easy part as in we were able to read the lean and make sure that it matched what the specification even said. But there are things that are not representable by the models that we worked with. So scoped effects the hash inside the circuit was outside the compiled route.

The verified no tool we used models it and a factor of Poseidon that we could not establish was uh the actual soundness of it in this case. AI agents wrote most of our proofs and Lean's kernel checked everyone. But that's not where the effort stops. A human must still be able to read the lean that was generated and try to align it with the exact business use case because the agent is not going to be able to interpret it the same way that you do.

So when should a spec stop asserting a property and start proving it? For the two failures that lose money right now, you can start with a spec with a guarantee table and an actual human in the loop that make sure that the business need is being met accurately and the agent doesn't go too far off the rails. So everything we've done is in the open right now and if you'd like to build systems holding other people's money on Ethereum, we'd love to work with you and if you build the verification tools, please find me and we can discuss in detail about what else went wrong.

So we have a write up, we have the specification and the model. It's all open source and the model is fixed at a pinned commit. Thank you. I think these questions are from the previous >> okay. >> Uh Ah okay. So Yeah thank you Ariman.

So we Yeah so we are ready for some questions. The first is what do you think are the gaps between this model and and realizing this as a contract? >> To closing the gap between model and the contract so you're definitely going to have to read both of them. I know that the entire narrative about writing lean and not reading it has been pushed a lot but I think you should be reading any of the code that's being generated so that you can be sure that it aligns with your

business use case. I would definitely be interested in some sort of tool that works as the project evolves and allows you to track differences between the model and the contracts or any other code that it depends on. >> So the next question is how do you formally verify Merkle tree state? >> This is a good question and I would be happy to take it off stage if the person wants to talk after.

>> Okay. >> Yes. >> And we just have another question. >> This is a good question actually. When using a high level language like Noir, how do you formally prove that the Noir execution itself is correct? So with Noir you can get an intermediate representation of the circuit which can then be sort of used. I think there are tools to do this. It should be there in our repository as well to make sure that the intermediate representation abides by what the model says it should.

>> Okay. >> So the next is about advice for how one would get into formal verification and learning lean. >> I mean you can ask your AI agent to explain the syntax of lean and definitely you should be reading it and understanding it. It can be difficult because it doesn't look like other programming languages, but this is my personal opinion at least with this. >> The next is how slow is the feature iteration loop for real applications?

Is it worth for complex use cases? >> This is a good question. So it truly depends on how much value is at stake, right? If you're building a system that would potentially have billions of dollars, then you might want to slow down in some cases so that you have a higher degree of probability of knowing what the system actually does. And I would say it is worth it for complex use cases. I mean we also formally verified one of our really simple open source libraries and we found six bugs in it. So I would definitely say it's worth it but in a measured way and only measured and

only formally verifying the critical parts of your code. >> So the next is a subjective thing I I guess. How do you define a spec is good? >> What is your definition of a good spec and how can a team ensure its specs are good? I think for specifications at least you want to make sure that your interfaces are solid. You want to make sure that you have security properties and any privacy properties that it must uphold and anyone who is trying to implement this system from scratch should be able to look at that specification and then implement it without looking at a reference implementation. So that that's

the level of detail that you need, but you should also make it concise without including arbitrary implementation details of your reference implementation if that makes sense. >> We have time for a quick question. Can Lean4 be integrated into CICD pipelines? >> Yes, so that script that I mentioned you can run it in CI and it should check that your model has no >> [music]