Post-Quantum Transaction Signature Breakout #11

Transcript

Antonio Sanso: Hi, Ellen.

Hi, OHE, Ricardo, Alessandro.

Yoichi: Hi. Thank you for the invitation.

Antonio Sanso: Sure. It's, just for your… today's topic, it's really near your heart, UHG, but in case you're interested about the post-quantum.

Yoichi: So I am, I am, you know, at JK Security, we have been reading about the latest crypto schemes, and also, like, of course, hash things, so yeah, I'm interested.

Antonio Sanso: It's every two weeks happens. Now, maybe we might have some little break in the summer, but otherwise, like, this is the 11th call. Every Wednesday, Every two weeks, and just in case there is a, They're… it's recorded, so it's on the…

Yoichi: promos. Thank you.

Antonio Sanso: Just try to do some progress, Every week, let's see where this will bring. It's a… It's a challenging topic. If it suits.

Yoichi: Let's see, like, you know, I don't want to, like, interrupt so much, but, like, I will, you know, somehow indicate, like, how far I followed, and we can start from there. Like, you can recommend me to read some syndata or stuff like that.

Antonio Sanso: For sure. Today, again, like, actually, after the presentation, since you're a kind of leading expert in the topic, I'm really, like, keen to hear your opinion. We wait a couple of more minutes, and we'll start. My… a few more people might join.

Yoichi: There can be some kind of miracul about formal verification, like, that's difficult, that, you know, everyone is saying that, but nobody's doing it, or whatever, yes.

Antonio Sanso: Oh, no. Anyway, let's wait for the presentation. Ricard is here. We'll present it.

Ricardo Perello: Hey, everyone.

Antonio Sanso: Usually, I start with a quick presentation, two, three slides, and then we'll see. One more minute, we'll start. Do you see my screen, right? Just in case.

Gustavo Frederico: Yes, we do.

Alessandro Baiocchi: Yep. Yes, yeah, yeah.

Antonio Sanso: Alright, let's start. Today's the 11th occurrence of post-conduct transaction signatures. This is a little bit of recap of what happened in the previous. They're not all covered, but the team of some of the most important calls. Previous one was about MPC Multisig, today is about formal verification. In the agenda, we have only one presentation today, and hopefully we have some interesting discussion. There's Yoichi in the crowd, that is one of the expert, word expert on formal verification, so I'm really, really keen to hear his opinion. But the… Before having the open discussion, I'm happy to have here Ricardo Perello. that is gonna show his attempt, or successful attempt, I must say, to formally verify the first contract done by Riva Labs.

And really, without any further ado… I'll give you the stage. To Ricardo, thanks a lot for joining, Ricardo.

Ricardo Perello: Hi everyone. Let me share my screen, because I have a presentation. Alright, so… let me introduce myself first. I'm Ricardo, I'm a student at EPFL. And I, I was introduced to formal verification a few months ago, and after ZK Proof, I decided to… Give it a go, and try to do some formal verification on some interesting stuff. So I decided to try and verify the… the verifier, like, the FORS+ verifier that, Riva Labs, developed. Let me start by saying that the concrete result is that we have formally verified that the Contract. Recovers the signature for every possible input. And also by saying that I am still quite new to this formal verification world, so…

No hard questions, please. So… Let's, Let's go, by starting on the two options that we had to formally verify this. There was a contract that was deployed by Riva Labs. Which is quite efficient, but it utilizes inline assembly. So it's quite hard to, like, check just by looking at it. And the other option was to go the other way, which is, there's a… Lean model for a… forest verifier, and using Verity, we have the opportunity to compile that into Yule, but that isn't… too efficient, so I decided to just try to formally verify the efficient one. Now… Before that, let's look at what the contract does.

The main, function is called recover. And it gives you, given a signature and a digest. it returns which signature, which signer, made the signature. It doesn't say whether the signature is correct or wrong, so… Just remember for later, we have to check that the address is the expected address. This is a… this constructs 25 Miracle trees, and it's done in inline assembly, so the class of bugs that we're trying to formally Proofs that don't exist are, like, Mistakes in, how we recover the trees, and how we build stuff up. It's not necessarily We're not trying to prove that the hash-based scheme works. Per se, we're just trying to prove that it's implemented correctly. Yeah, so here I was explaining the type of tests that we are looking for, so…

for example, wrong offsets, or swapped Merkle trees, or… basically We want to show that for every possible signature, we return the correct output. Here is essentially the big picture. The horizontal line is, the Solidity compiler pipeline, so you give it… a Solidity source code, and it turns that into an intermediate representation in Yule. Then it goes in a loop, trying to optimize the fuel. When it's convinced, though, that it's optimized, then it, compiles that into EVM bytecode, and that's what essentially gets put on-chain. Now, our proof, runs on the optimized UL, not on the EVM bytecode. Which means that we have to trust the Solidity backend, the Solidity compiler backend, sorry, to… we have to trust that it is able to compile from, Yule to bytecode correctly.

But our proof shows that The assembly was constructed correctly, and that it's the correct implementation. So the way we are going to do this is we are going to… take this Yule artifact, and we're going to put it into something called EVMYul, which we're going to see later. And we're going to compare how that works. Versus a… clean model in Verity, or sorry, in, lean, It's our reference of how force is supposed to behave. So… The tool… the most important tool here is EVMYulLean, which is a product that Nethermind, made, which allows us to run a UL contract inside lean, and it gives us semantics to reason over what the EVM state is going to be.

After each iteration. And what we're trying to do is compare this, lean… Implementation of the EVM with… The reference, which is, like, a clean model of the scheme. I understand that all of these, proofs can be hard to read sometimes, so I tried to make one really easy statement. So that we can understand what we're going for. So the first line says that the contract that we are looking at, so the optimization. is… Parse to exactly what lives inside the EVMU Lean runtime. So it just means that we're looking at the correct thing. The second line says that for every representable signature and digest, the runtime will return The reference is address.

And the last line shows that we are… Modeling correctly, that if… if the signature is bad, then we return the zero address. So let's go through it a bit… oh, sorry. Here. Now, if anyone wanted to review this, the idea would be to first review this, Theorem, then look at the reference that we are using. And, look at the actual boundaries of… How this is, all connected together. And finally, Look at the… bridge between, like, what Solidity compiler outputs and what's being ran inside the EVM Unit. I've also made a little script that runs every… Proof, and There's also a second script that allows us to check

a, contract on chain to see if it has a… Same, Yule. That's the one thing we're checking right now. So, to summarize, What we are checking in Lean is the… EVM, behavior for this, assembly, reconstruction of the signature. And, we are trusting the Solidity, like, the last part of the Solidity compiler pipeline, which turns Yule into bytecode. We're also assuming that the wallet is going to do correct Key rotation, and You know, you'd be checking that the address is exactly what I'm expecting. And finally, what we're not claiming at all is a proof-of-care check. We're not claiming… Unforgeability of the signature, which is showing that it's a correct implementation of the signature.

And that the wallet itself is good. So, the way I did all of this was basically using AI to write the proofs. But as some of you may know already, We don't trust the AI, we just trust the… Lean, kernel. And yeah, the next steps for us are going to be to try to prove that the actual bytecode that will live on-chain is, exactly… what we expect, that the Solidity compiler doesn't… Mess up and introduce any bugs. Which should be fine, because EVMYulLean also provides us some tools to work with pipe code instead of lean… instead of Yule, sorry. But that's a bit in the future. We'll see when I am able to do that.

Yeah, that's exactly what I just said. Yeah, so… There's also another… Question to be asked, which is… At the beginning of this whole, idea, we were considering the two options, which were to proof the, the efficient contract in lean, or to derive a contract from a lean model. And, it remains to be seen whether we are able to produce an efficient contract an efficient code from the lean, so from Verity, basically. And that's it, so thank you for… listening, if you have any more questions, or if you have any questions, I have some… Slides about the axioms that we're using, and the…

And our surface for theorems and stuff like that, but if… If not, then that's it.

Antonio Sanso: Any question? If not, if you don't want to talk, the slide and the chat is open as well.

Yoichi: So, I have a basic question so that I could… So this one is for recovering the address, and there's… there's a separate thing for, like, checking the validity of the signature, and the intended use is to call post, like, when you are trying to Check signature that you received, and… Then you have to use both of these primitives.

Ricardo Perello: So, what am I… The point I was trying to make is that the recover function doesn't just say, yes, this is valid, or no, this is valid. Recover only tells you the address that signed. So, in your contract, you have to basically call Recover and then say. recovered address equals the expected address, and then that's your Boolean for yes or no. And this work, what we're trying to prove is that the recover function works as expected, or the assembly code that we wrote. Hmm.

Yoichi: Yeah, I was wondering about this, because maybe this is a malleability thing, like, once you see a valid signature, you can create another very valid-looking signature, or that's why you won't, like, accept only the canonical thing. Is that the… Yeah, it's valid. I am still a bit confused about why it is to… Operations exist.

Ricardo Perello: Sorry, which operation? Like, check…

Yoichi: Yeah, this…

Ricardo Perello: The address?

Yoichi: Recover, and it's valid sync.

Ricardo Perello: I'm not sure what visitor.

Matteo Vicari: Okay, yeah, we try to explain, because it is our contract, so it's better to explain. So, it's like a chira cover for, for each EDSA. So, you can recover a public address from a message. We do this because we have to confirm this address with what is stored inside our smart contract forward that say, okay, if you try to make a message using the next designer that it can sign the transaction. Okay, we are good, and the transaction is approved and executed inside the wallet. This is the idea. Oh, it's work. It's like, EC Recover for, for HDSCA, but it's do with a PQ sign, for make the wallet PQ.

Yoichi: Okay. Oh… Yeah, so, like, I guess, you know, this work uses, like, two very defined boundaries. One boundary is the eulosemantics, and the other boundary is this, specification of force C. And, So, yeah, I'm… but I'm guessing, like, yeah, how much of a bigger picture you want to cover using formal verification? At the end, like, there's a property of the wallet. That they want a guarantee. And, there's, yes, this primitive about the recovery in the address, and… So… Yes, and then, like, I… yeah, I guess the bigger challenges remain in this gap between the molec property

And this primitive. Do you have some plan or ideas how to tackle these kinds of things?

Ricardo Perello: So, as far as I understand, there's a separate effort to try to prove the whole signature scheme with, SLH-DSA. And that's a work in progress right now. And then… The next step on top of that would be to integrate the wallet, that uses SLH-DSA. But that's… Also in the future.

Yoichi: Yeah, I see, I understand. About, this work itself, how… Hmm… Like, I want to kind of get a feeling of how complicated it is, like, in terms of, say, like, how complicated is the case analysis? Like, is the… does the code contain lots of case analysis, or is it more like a straight line code, or… Another metric would be, of course, like, you know, how many lines of proofs got generated by AI, so another thing is, like, yeah, well, so I guess you didn't have to assume anything about K-Check, is that correct? I mean, I…

Ricardo Perello: I did have to assume that check was working correctly.

Yoichi: Okay.

Ricardo Perello: Hmm. Yep.

Antonio Sanso: This kind of… I mean, the KC has been inside the AVM for years, so, I mean, I can't say it's back free, but I'm not too much concerned about this layer of availability.

Yoichi: Okay.

Antonio Sanso: A good question for you, Yoichi, actually. I mean, and it's the same question I actually asked privately, you know? Do you think that the flow… I mean, probably you're the most experienced in this call about formal verification buying it up. Do you think the flow that Ricardo followed is the… is a legit one? I mean, like, he's starting to compare, width and lean implementation written… I don't know, probably by hand. So, in this kind of situation, I always wonder myself, this is the… that, let's say, the ground truths you compare against. But what about if death has a bag? You know what I mean? I mean, how… how is really, like…

Yoichi: I see. I mean, so in the end, you know, in the end, like. What is correct, like, I mean, in the end, like, Okay, so maybe you want to anchor this against a document or a paper written by somebody? Like, I mean, what happens in other places, like, they… people look at, like. NIST document, like, fibs, and then try to argue this is the correct thing, but in the end, like, when you're, like. trust… when your anka is an English-written document, then, like, somebody needs to read and, like, yeah, everybody who is concerned needs to, like, read and compare the English document against the link code. So, I mean, that gap always exists as long as the official, like, canonical document is

not in a formal language, like, if the official thing is in English, then, like, people need to, like, keep comparing the English thing against the formal thing. That's the… That's not avoidable. Unless, like, you know, you somehow convince the official source. of truth, to use the Lin or other formal languages to, like, describe their definitions. The demonstration kind of improves for formal verification people, but usually, like, the definition is written somewhere else in English or something, so, like, you really need to compare things.

Antonio Sanso: And this is the next question for the Riva Labs guys. How did you actually code this Solidity stuff, manually, or you made the AI generate the… the… The contract… no, sorry, the lien implementation. from the… from the PDF. So you give a PDF, the AI spits the solidity… sorry, no, the lean, the lean. equivalent of the PDF, or you brought manually the lean… Stuff.

Ricardo Perello: Well…

Alessandro Baiocchi: I can answer a little bit, regarding the, the, the…

Antonio Sanso: Question for Matt, probably, because you… But yeah, for Mateo, for Alessandro.

Matteo Vicari: Yeah, yeah, he's speaking Alessandro, yeah. It's Alessandro.

Antonio Sanso: Sorry, Alessandro.

Alessandro Baiocchi: No, okay, so, actually, the… we did a little bit of lean, but not that much. Actually, we just… we… the… our main implementation was written directly in Solidity. The, the little bit of lean that we wrote. was mainly done by, like, AI-assisted. That's to be admitted. And when you said, like, the implementation of the… Solid Vilifier was, I'd say… like, half and half, maybe? Like, it was AI-optimized, but, written.

Antonio Sanso: Because what I understood is, like, that eventually Ricardo, what did Ricardo is, like, said that the… Solidity, or the Yule, is equivalent to a handwritten LIN that… I guess, the handwritten LIN, or, like, machine-generated lean, was written by you, no? Is it for C3? I think so.

Alessandro Baiocchi: Okay, so wait, we have… we had some vague tryouts in the repository. I don't know if Kikatu was referring to those ones, maybe? Yes?

Ricardo Perello: No, so I think what we're saying here is that my reference for which I'm comparing, the Yule is basically this one, the reference that we're talking about, and I think Antonio's saying. If we're checking, something against a reference that is also written by AI, we have to manually check it. Before we trust it. Is there a warrant anything?

Antonio Sanso: Yeah, I mean, at the end of the day, it's like, Ricardo, you say that the UL spitted by the contract is, like, equivalent to a lean version, and if I remember correctly, the lean version was in the Riva Labs repo, no? Or I'm confused.

Ricardo Perello: Yes. Yeah, yeah.

Antonio Sanso: I'm asking, I didn't realize, guys, how do you ride this lien?

Alessandro Baiocchi: Yeah, okay, so I think that's the… yeah, this lean version was part of our experimentation with Verity, and it was, yeah, mainly written by AI, yes.

Antonio Sanso: But how do you do it? Like, you gave today a PDF, and they spit Lynn, or…

Alessandro Baiocchi: When we do… when we did that, I think we… we gave them the, like, a lot of context about, FORS+, like, standard decisions, like, yeah, what the signature is, and then we gave them the… the verifier, and the… in Solidity, and then the… the goal was to have, like, The goal that we gave the model was try to build, a lean version of this, of this implementation. That's just the… That was the goal, I think. Yeah.

Matteo Vicari: Yeah, and this, and when we start doing this, we don't use the optimized version right in UL, because it's hard for LLM to retry, to try to to the lean, the lean for something is, written in Yule, like, Ricardo do. He do a very good job, expert of us. We try just to have, a simplified version right in, pure solidity. That are not optimized, so, follow better step, and it's also easy to read. For, for us, for, have a check on the lean spec, we try to do, also using LLM. And then we arrived there. The problem is, we can't, have a way to match, the,

the bytecode of our implementation, because the goal, but we don't achieve this, and we are far from this, is have, the contract, that we call in our system is, 100%, to… what is the bike code that we verify with LINA? This is our goal, but… there is a lot of time, there is a lot of stuff going on. For example, all the complexity behind to have the LIN also for the compiler stuff. This is really hard, and Verity tried to build, something that do this. But we… we not, arrived yet on this. So… yeah.

Ricardo Perello: I had a… I had a look at different ways that we could prove the CVM bytecode. And… To me, the simplest option was either, try to directly prove that EVM bytecode inside the EVMYulLean, which is possible. Matches the reference. Or we can try to say that EVM bytecode inside EVMYulLean equals optimize Yule inside EVMYulLean, and then down the proof path. But I think it's much more complicated to formally verify The last part of the compilation, like. Formally verifying this part would be… Like, a lot of work. Yeah, yeah. It's much easier to prove this.

Matteo Vicari: Another stuff that Verity tried to do is have, deploy bytecode that is come from LIN directly. And then you can use on-chain this bytecode directly. So, this is another way to do. This can be helpful, because you can have your code written directly in LIN. But, it's a little different for Tiz, you have to use a very specific form of LIN that is from Verity, I don't remember Alessandro, it's called.

Alessandro Baiocchi: It's not… it's, it's just a relatively lean CDSL. It's basically just a sub… sub-language of… but it's… So, basically, Verity… validity superhum.

Matteo Vicari: And then you just deploy, the bytecode that are… come from the verity, the validity implementation. our, our contract of the FORS are simple, because the FORS are not much harder. Doing all this stuff, for, SLH-DSA, it's really hard, so, we are also…

Antonio Sanso: This has been done. This has been done already by… I think by the Verity guys, actually.

Matteo Vicari: there is some assumption on this, Ricardo, I think I have a look.

Antonio Sanso: I'm gonna say, like, the last information I got from Nico is that they managed to actually formally refine the full sphinx. Boom. But it's, again… great stuff so far, guys. I still… me, I'm still, like, having some perplexity in general, not about this work, this work is fantastic. We still really need to be careful. When are we gonna do this, for the final version? willing to pay attention to the ground truth, because, I mean, if the ground truth is wrong, then, like, it invalidates everything, you know what I mean? Like, really, at a certain point, we really need to understand, or someone needs to, you know. Try to figure out If the source of truth is true or not, somehow, right?

Yoichi: Yeah, for this, you know, one thing I can point out is, like, it's kind of easier to… I hope it's easier to read the specification of the recover function. than to read the URL code, or than to read the EVM byte code. I mean, so instead of reading the error code, you can read the int function, that's a progress already. And another thing is, like, there has to be some security proof about this scheme. Like, if somebody can forward your signature, then they can also do the, like, pre-image or whatever. And once you do this kind of proof, using this recoverRAW function indeed. Then, like, you don't worry so much about, you know, if this DIN function is exactly the same described in the PDF, because, like, now you have… you get confidence from another source, like, this DIN function.

That is, this dean function has a very good property. If you break it, you break the pre-image of a check, or whatever. So… Then, like, you know, that's another way to get confidence about this lean specification.

Antonio Sanso: It, Bandit, I see you in the crowd. I mean, we have this kind of stuff, right? For force.

Benedikt Wagner: I mean, we have this for hash-based signatures, yes. The question is. what level of detail do you care about? Because you can have a security proof that just shows asymptotic security, and then maybe we are happy with that, but if you want concrete security levels, it's a bit more complicated, but I think even that can be formalized in lean. So I think there's this new CryptHOL paper by Alex and co-authors, where they give, like, a framework to formalize security definitions and security proofs of signature schemes in Lean. So I think this can be very helpful. And then I… at that point, then I totally agree.

Antonio Sanso: Nice. Now it makes sense. Thanks, Eugene. This is actually a really good thing. So, you're saying, now we have this, this lean signature of Britain in… I mean, this, this, this, sorry, this fourth signature of written in LIN, that is our ground truth. We can actually expand it with some proof of the security assumptions in Lean that will make our ground truth even stronger. That's what you want.

Benedikt Wagner: There's… there's still, there's still, something to be checked, because, of course, you can prove security of a scheme that you formalize in lean if the security notion, the definition of security. is meaningless, for example. So, we still have to check as sort of a crowd truth that the security definition that is formalized in lean matches what is current… what is accepted as a valid definition of security.

Antonio Sanso: But as far as I understood this, all this formal verification path is that to have the manual inspection as small as possible. So, the thing that people need to actually inspect and visualize, like, manually should be as short as possible, so it's easy to verify. This is my understanding of all this formal verification game. Maybe it's the wrong one, but this is what I… how I depict this in my mind.

Yoichi: Yeah, so how I depict it is, like, you know, there's a rare implementation that's used in the Morit, and the Moret has a user, and maybe the more it has an off-chain component, on-chain component, and so on, and that whole thing needs to, like, correspond to, like, the game. That's defining the security property. Otherwise, the, you know, your statement of the security property doesn't correspond to what people are doing, and that's very problematic. So, like, yeah, getting, getting more powerful and… more powerful statements in the end. That's closer and closer to what people are actually doing is another dimension, I think.

Antonio Sanso: Okay, cool. Pretty cool. Now, now it makes even more sense. So, Ricardo, just like, to recap, again, great stuff so far, a lot of what I've seen. Probably, if you still have some cycle to spend on this project, then we can be in touch, later. The addition on this will be, like, to… to do a… add this new dimension of proving the assumptions. Does that make sense to you?

Ricardo Perello: Yeah, so it's… it's two things, it's… Proving some security… assumptions about this, like, if I… if I break force, that means… I broke a check, and also trying to get the EVM bytecode And not just the optimize your verified.

Antonio Sanso: Right. I… for some reason, at the moment, I even more… Keen on the first one, then the second, somehow.

Ricardo Perello: Okay.

Antonio Sanso: Because I think that, you know, again, for me, like, having a strong ground… ground truth is really the thing, you know, like, if that stuff is… if you don't have confidence in this, you can prove everything, basically, right? So, I think, like, the first thing you mentioned is, like, having a strong basement to build on top, you know what I mean? But great progress so far. I'm pretty pleased to see what we've seen today. Right. Anyone has any other question? Alright, if I take, like, a note, so I will… I'll give you back 20 minutes of your time, if it's the case, and We're gonna see in two weeks. I will thank again Ricardo for representing the Riva Labs guys that, gave the…

the basis of this work, and Yoichi, thanks a lot for… for swing by and give a suggestion. Benedict as well, thank you for… Prompt. answering the question. See you in two weeks!

Benedikt Wagner: Thank you, see you.

Antonio Sanso: Alright.

Ricardo Perello: Right, goodbye, everyone.

Matteo Vena: Bye, everyone, see you.

Alessandro Baiocchi: Thank you, see you.

Transcript adapted from ethereum/pm, CC BY-SA 3.0.