From Production Rust to Lean 4 Proofs: A Verification Pipeline

Transcript

[music] [music] >> Hello, my name is Natalie. I work at runtime verification verification engineer and I was told that I should carry this heavy microphone because hands-free one is too big for me and I also have to say that it is pretty heavy. Okay, so today's talk is about verification pipeline we developed for Ethereum Foundation. It all started with project for Ethereum Foundation. It was collaboration of several big groups and our goal was to verify formally crypto libraries such as

Plonky2, Risk Zero and our task specifically was to build a pipeline which takes source rust, translates it to lean deterministically. It's not it was not allowed to translate code using AI because when you translate code with AI translation is non-deterministic and there is no way to prove or show somehow even with tests that translation is correct. Yeah so translate code to lean 4 that's our step number two.

So we did translation with deterministic instruments such as NES Hawks. We could use an instrument which is mature enough and once we have source code in mathematical model we can reason about it, we can state theorems and prove that code actually does what it should do in mathematical sense. For some pieces of code we've been writing shaped lemmas which were just behavioral lemmas and for complicated crypto we used libraries such as ArcLib and CompCert. They are also part of this big

project and they were created within this Ethereum Foundation initiative. And finally we had to prove that production Rust matches the mathematics. So the approach itself has three parts. First part is specification. This is one of the most important steps. We write specification in plain English. We discuss it with maintainers. We should have crypto specialists in the team because he should explain how exactly specification should be written.

Second, once we have mathematical model then code is translated to Lean, [gasps] we can reason about it as math. Then proof. We did all the proofs using AI. Like before AI era it was not so easy as it is now. Each and every proof we've been we've been writing manually and it could take even a month to write one single proof. [gasps] And today AI will do it in several minutes. Sometimes I have to say that some proofs are really complicated and even AI it takes several hours maybe up to 30 hours. That

was our biggest experience. And this is how approximately looks initial code and this theorem is behavioral lemma. This is how they look in Lean. So this is more detailed description of pipeline. It starts with Rust crate, then we translate it with existing instruments and ears Hex. Then we have Lean model, when we do the proofs and Lean Lean confirms that proofs went through Lean kernel, which is about several thousands lines of code, which is mathematical model behind. So AI

cannot hallucinate hallucinate when it does the proof. So each proof is checked by Lean kernel. And by the way, also all Mathlib is also checked by Lean kernel. So this is something we can definitely trust because it's mathematically proven. I mean Lean kernel. So what we should take on faith in this pipeline? First of all, specifications. Second of all, of course, compiler. We even have to trust hardware. A lot of things we should trust. And one of the most challenging problem for us is we should trust translation itself.

Building such translators from source code to Lean is pretty complicated task, which can take years of research because you have to decide what logic to contribute to. Is it separation logic? Is it many-sorted logic? You also have to decide what semantics you should use. It can it should be executable semantics. Perfectly, it should be executable semantics in Lean because if we have executable semantics, we can use, first of all, fuzzing to show that initial code and its mathematical model equal to show, not to prove. We even can prove that are equal, but to prove it,

we can For example, if we will go by induction, we can prove base case for little piece of code, right? Then by induction, we can show it it is that code equal for both versions by induction on biggest amounts of code. But this is separate serious engineering task, a research work with which also can take several years. And yeah, and what else? We also can rust compiler test suite on Linux version on on Linux, yeah? So since model is executable, we can run compiler test suite and this is another way to trust our translation.

So if we go even deeper within the pipeline in ES and Hucks, they take code from LLBC, its intermediate representation. And before and before LLBC would be formed out of mirror, which is also intermediate representation of rust. So as I said, behavioral and shaped lemmas we've been writing ourselves. And for cryptography, we don't write the spec by hand. We use specialized libraries from the same zero-knowledge EVM project. Our clip is the math of SNARK protocols written in Lean.

What Fry should do, how it will fold, how some check must compute. And we prove that the rust computes the same things as the definition. So we've been targeting we tried our pipeline on eight targets in Plonky2. Bug in its field arithmetic or in Fry folding silently breaks every proof virtual machine machine emits.

And everything is public. And the rust there is last rust Lean repo I mentioned in here. So this is the full list of targets. First column is target we tried to verify with our pipeline. Second column is instruments we used and finally what we managed to prove. Um yeah and best result was about fry folding but it was only one step of fry folding we managed to verify it next to our clips definition.

Yeah I just described that this was the most um the most interesting result we achieved. We also of course proved a lot of behavioral lemmas and I have to say that many security audits stay at this level and when we prove crypto versus our clip we actually go one level level higher. So what about AI? We used AI on each and every step uh at every stage starting from research and exploration for we used it for writing specs but I

have to say that we definitely cannot trust AI when it writes specs itself verification engineer of course he should check each and every specification because AI keen to write sometimes vacuous specification which is very easy to prove and which means nothing which is useless actually. So also AI can take can take some optimizations which we have in Plonky free it it can think that it is actually a bug but in practice it's not a bug it is optimization which is intended behavior

it and it was planned by maintainer so that is why we should write our specifications initially in plain English and discuss it with maintainers because we should understand very very precisely what this code should do. So collaboration with maintainer is very important. This is what we learned. Uh what provers we used? We didn't use just Claude, we also used specialized provers such as Aleph for example. Aleph uh it's from logical intelligence.

It splits an obligation into sub problems and proves each problem separately. It can also submit PR. You you just give it theorem, give it repo and it submits PR once proof is done. Uh we also tried Aristotle and I have to say that they both Aleph and Aristotle are really good but finally we decided that probably Claude would be enough especially with latest models. Our our work happened like seven or eight months ago and today we have models from Claude and we just do not specialize lean AI

based provers anymore. Well at least in our case. So what limitation we faced? First of all seven months ago Comp Poly and Arc Leap both these crypto libraries with crypto specifications they were not ready yet. They were not mature enough and there were a lot of bridge lemmas which we had to write and prove ourselves to fulfill gaps in our specifications.

Next big limitation we faced was limitation of tools themselves. Anies and Harks they do not support yet low level unsafe async rust and Plonky2 full of asynchronous code. Uh so we also faced for problem like algebraic identities were you have to pick the right mafly blemas.

Yeah and version drift. Version drift also big problem because we had to build this um lean project which works with our clip compoli hex or an yes. And each of them had different lean version, right? And mafly also should have one and the same lean version which our instruments in the pipeline had. So how we fixed it? We collaborated with maintainers. We tried them to align instruments so we could use one and the same lean version and they were actually very responsi

responsive and we managed to build this pipeline and to go through it. [snorts] And as for extraction gaps gaps as I said well for now we don't even have unions being supported in in an yes though I know that maintainers working on this. So in different languages we have different limitations with different tools which can translate production code to lean. We have all kind of limitations. So we

started to work on our own instrument. So this is the tool we are building at the moment. And on the left you see C version and on the right you see lean four version. As you can see, translation is very similar. Uh, we contributed to semantics which was developed at runtime verification for NASA.

And we to express side effects of C code, we used free monad in Lean. Um, so how can we trust this translation? Our semantics is executable. So we can run differential fuzzing C C versus Lean or we can run compiler's test suite uh or we can even work on research and figure out how to prove uh code equality equality, but this is this would be really big research work because um

there are a lot of challenges and it is possible that we will hit the wall. AI is not able to do it yet. I mean write such instruments, make translation from initial code to Lean deterministic. [snorts] There is even more reasons why it should be deterministic, I mean translation, even very basic one. If we have a bug in translation, we only can figure out what kind of bug it was and fix it if translation was deterministic. And if it was made by AI, behind AI we have non-deterministic algorithms, so we will not be able to

to catch this bug like never. Mm. So everything is public and all the code is in GitHub. And we also write papers and several blog posts about this work. Uh, please if you have any questions, I'll >> [applause] >> Great talk. Let's go through the questions.

So the first one like can you give an example of an optimization that I misclassified as a bug? >> colleague worked on this one and he was extremely happy. He said, oh my god, I found bug in Plonk free. Oh my god, I did it. I found that. And then maintainers we collaborated with them and they said, nah, that's not a bug. I am sorry man, it's just optimization. We did it on purpose. This is how we can make it work faster. Yeah, my colleague is not here so what specific bug was taken?

>> Next question. >> And the second one is like Question number two. An Eos cannot translate arbitrary rust code to lean automatically. In such cases what we do? How we model the code? We model it manually. We just write write it. For example, when we faced problem with unions we had to rewrite the code in the type which Eos can handle.

[gasps] [sighs] Yeah, we we we've been collaborating with Eos maintainers. We asked them, let us contribute, let us build this union which we need. And they said, no, it will be just it will support just little subset of unions we need. Our approach to support everything it's more research work and as long as I know this work is in progress. And yeah, and right now we work on formal verification of Linux kernel. And we actually recently found a bug in Linux kernel. It was fixed. It was we we suggested patch. It was bug in Linux

isolation kernel. And we suggested patch. It was applied. Isolation kernel isolation layer Linux isolation layer where all the AI's actually run. It was secure security bypass. And we also found several more bugs using our pipeline. And yeah, you probably will ask how do you work with C code? Linux is in C, right? Not just there is just 5% of Rust in Linux and like 95% of low-level C code. Well, we again use our pipeline. We translate C to Rust and we do differential fuzzing to show that C and

Rust equal. And when we go to LLVM and do the proofs. Of course, for C that is why actually my example last example was in C. Low-level C with mutexes, multi-threaded and with translation I showed it was deterministic. >> Okay, the next one which Rust features cause the most difficult difficulty during extraction and how much did you refactor the production code? Yeah.

>> run out of time if I'll keep listing them, but of course we were we hoped that [clears throat] well, biggest problem is async code, multi-threaded code in C, async code in Rust, go routines in Go. This is what is not being supported. As long as I know in in years like year ago there was an experiment they tried to integrate Iris and they tried to tried to work with separation logic to verify async code, but

I don't know how it ended right now. Async code is not supported. So we can work only with some subset of rust, safe rust. It's pretty big actually. So we can translate all arithmetic easily. Even in Linux there is huge amount of code which can be translated with our pipeline and verified. But async is the biggest pain. Async code. >> Yeah, then >> takes us >> the next one why hash base and all lattice base um >> I don't understand >> I I think he's asking about the PQ question.

>> hash base? >> Uh the okay the next one um so AI makes a spec a mass breeding and AI proving easy. What does an engineer ignorance or formal verification do to verify that spam math is not sort of um PQKD if reading uh spec math too hard. >> Um we're not hiring. >> [laughter] >> No, no she like like the question why is is kidding like because if someone wants to do it right, we probably need the expert like you.

>> We cannot trust AI. We always should have verification engineer in the pipeline and he should check each and every specification. >> So basically the answer is to hire you. Like the expert to really like sort of help us do the proof. Okay we >> [music]