Formal Verification of the INTMAX2 Protocol

Transcript

thank you so much yeah hello can you hear me yes uh thanks um hi so I'm Denisa let me oh is this working okay yeah let me present myself uh a bit so I am with nethermind not with itms but we work for uh with with itms um so I'm a conservative researcher at NE mind I'm also an associate professor at the University of Bucharest where I teach uh formal verification and functional programming and that's my corner if you want to check it out um so yeah

well okay so today as I said I'm going to speak about inmax 2 and how we what we did at nethermind with the wonderful team behind um inmax which is actually we formally verified um their um their white paper but so I will touch a bit on the formalization which is um we are wrapping it up but I would like to focus more on trying to sell you Inox and show you what the cool solution it is and the protocol is extremely beautiful and their white paper is just a beautiful piece of mathematics so I invite you all to to look at it so now if you should I be closer to it

yeah okay so now what is in Max what can it do it's us I think probably if you try to put it in a box you can think of it as a based um validium rollup but it is a scaling solution for ethereum and let's leave it as is uh which has amazing performance um so they are claiming five bytes on chain and I will try to convince you of this the beauty part from a consensus researcher and I will be without job probably is that it is stateless and permissionless so that we don't need an underlying uh consensus protocol it just has to rely on the consensus protocol on dl1 um I will not touch today much on

the Privacy using ZK proof so I will just show the Easy Flow the simplest version of the of the protocol and I will just show at the end that you can use um uh ZK proofs now it is by nature sensorship resistant and it is among the fewest protocol I've seen that by design it is sensorship resistant and I will try to prove this um for the moment they say with the current block size on ethereum they can they have a limit of uh 7,500 transaction per second but there is a very nice twist here because actually a transaction is just a batch of transactions in which a single send

uh sender can send as many any uh transactions or tokens to a lot of other participants right so I will try to convince you of all this points and why they're valid now at our at um nethermind we have a very strong team on formal verification and you have Julian there who is the head of formal verifications so for all the technical questions you can go to Julian so we as I said we are formerly verifying the their white paper and we're doing this in Lin 4 so the code actually mimics and mirror the white paper um and here you can have for

example when we show that the that the balance is like we will manage to compute that um is monotonic in the in the first argument um the formalization will be open source and we are wrapping it up so it will be um available soon and the white paper will contain references to the formalization and for the moment we have around uh 3.3k of uh lines of lean but now let's dive a bit into the protocol and see which are the key insights that lead to this um to this nice scaling solution right so first of all if you look at payments it's true you don't need underlying

consensus and it's necessary to make available on dl1 only a commitment to a set of transactions and to the set of senders who have signed the commitment and the nice part is that they delegate the da um aspect of the protocol on the user side so it will be the responsibility of the users to compute the balance of of their accounts to compute the um to keep track of how much money they spent how much money they received now the only part in which you have to check that everything is sound is like when you have to do a withdrawal and you have to compute that from scratch and I

will try to show you how you do this okay I think I would just be more efficient and stay here hope okay so in Max is a as I said it's a permissionless block building um that can be performed in parallel and it matters only the order in which they will be the blocks they will be stored in um on the L1 contract but know that here a block is not in the sense of a traditional blockchain because it doesn't have to refer to the previous block and so on it's just a storage um on the L1 now the

block Builders and this is important to understand is that they don't need to verify the validity of the transaction so it's stateless and you don't need to coordinate the builders they don't need you don't need to pick your uh uh a a leader for for for um for building a block so now users they have three actions they can deposit they can transfer and they can withdraw it's a payment solution now for deposits an L1 user will just send funds to an L2 address on the rollup contract on the underlying L1 which is going to be ethereum and that's stored in the contract storage now the transfer is the interesting piece of um um uh of the

design and it has two phases so first of all senders they have to pick an aggregator anyone can be an aggregator there can be several a aggregators you can and probably they they're going to use Rel layers in order to make sure that you don't have a malicious aggregator that can postpone uh uh posting your transactions and so on so let's say we pick an aggregator that we trust and the senders will start to send a bunch of transaction uh meaning that that send is just a function everything is a function uh they send um okay they announce to how many participants how many tokens they want to send they send this information to the aggregator the

aggregator creates a merker uh merker tree sends the proof to to U of inclusion to to the to the user to the sender the sender checks it classically it's signed send it back the aggregator collects a bunch of um valid signatures aggregate them and post this information on on dl1 right now the other part that is missing uh is the fact that so this is just me explaining that you have to have um a batch of a transaction bch now the other part the the phase two of the transfer protocol is that the senders have to send to the each recipient as uh a proof

that they actually send the transaction right so each each sender will send the meracle proof that they received from the aggregator to the recipient that they have in mind plus with previously proofs that he had at that point and that's not that's done directly not via the L1 contract nothing right now the withdrawals are quite simple but there is a Twist to it because in order to withdraw you have to even if I want to withdraw my own funds from the from the from the rollup I have to engage first in the transfer Pro protocol in which I will send the the transaction the the amount I want to to

withdraw I will send it to an L1 account and that will be posted on a on a transfer block and then I can use the proof that I built and give it to the and send it from from from an L1 account using this proof that I I I have send it to the rollup contract and you do the withdrawal so um as I said when you transfer the block you the the L1 contract doesn't automatically send the funds to dl1 you have to go through the transfer protocol before and uh after that you can do it you can trigger but in order to trigger the withdrawal you can you have to go through the transfer protocol

now what we are formally verifying is their security well the safety property saying that the rollup contract is secure if every withraw is um is fulfilled it's succeeds so um and we show that okay you have to have a TR assumption at at the point so breaking this security result is like either you collapse the HH function or you break The Binding of proper uh property of the um Au underlying authenticated um dictionary now let's look at the protocol right everyone can be an aggregator you can be your own aggregator it may be a bit more expensive for you but you can do it so

you don't need Escape hedges for this protocol by Design you have it so everyone can be an aggregator therefore you have censorship resistant modu of the sensorship resistant on the underlying L1 now the r contract as I was trying to show in the pictures manages deposits transfers and withdrawals right and for each type of the user action you have three different kind we call them blogs but as I said they they don't have to rely to to address uh the previous block and so on so the contract the rollup state is just a list of three kinds of entities which can be deposit blocks transfer blocks and

withdrawals now in order to convince you the of the five bytes on chain let's look at the transfer block which is put on the on the storage contract which this is the biggest part and it actually contains uh the an L1 address of the aggregator so 20 pites this extra data string is used for security reason such that you don't have um such that the um the agregator will not postpone on on on posting your blog then you have the a authenticated dictionary the senders who actually sign it and an aggregated signature and if you do the arithmetics at which I'm very bad you would obtain this information but now

notice that here you rely on the size of how many senders you have not on how many transactions you send and this comes from 96 because you use BSL signatures and now you can add compression I will not go too much into details you can add compression using a relayer contract and and if you with the current version of the block size on on L1 you get this number right and if it will increase if they will if you'll have more space on the L1 blocks you can reach this point which is even more than how much Visa transactions you can support at the moment but now what I want to get into is the magic behind the protocol because it seems okay but what

happens with double spending who is doing the verification a lot of paranoia can come up here right so the magic trick is balance function uh which uses a very nice algebraic structure um called latis ordered a billian groups and you have to use this balance function when user have computer balances or when you have to do when the rollup has to do a withdrawal now if you don't know what ltis order groups are is no problem there are some algebraic structure that they are used in fuzzy logic for example basically you have a group such that you can do uh you can add your tokens but

then you also have a lce order such that you can compare uh tokens between them but not it doesn't have to be totally ordered so you can have uncomparable uh tokens and you don't care about that right um and there are scenarios in which you can think and then usually you in a group you have positive con and negative con so obviously the balance of accounts they always have to live on the positive con of of the group now the balance function and how why does it work is the fact that you have to split the information between two parties you can have the the list the history of the rollup you can have

all the all the blogs that have been added to the rollup contract but without having a proove from a user side you can't retrieve the state of the of the accounts the balances of the accounts so you need two pieces of information you need a proof that comes from the user and you need the history of the rollup that is on the L1 um contract rollup right and a state will just compute this B here are just functions which says okay which is the uh how many tokens each account has and you have to compute this value right um and in order to do this you have to

split it in two parts first of all you have to if you have a proof but you don't know anything about it you can have partial information there it can it it can be Rish you don't know and then you have the list of the history right so first of all you have to extract the list of partial transactions from these two information and after this list of transaction you just apply a State transition function and you compute the balances this is not optimal but there is a version in in which this can be faster but I I will not go into that um here but the trick is because you are in an scenario in which you have partial

information the best thing you can do is just compute a lower bound of the balances actually and you reason against that and you make sure that you don't withdraw um more than this lower bound so let's look at an example right here B 0 it's a deposit block and let's suppose L is deposit 11 token in the rollup now we have two transfer blocks the yellow one one in which Alice sends seven tokens to Bob right so he she will go through this transfer protocol and she will get a a proof from the aggregator let's call it P1 now let's construct a different uh transfer in which Al is now want wants to send three tokens to

Charles so she will take a different proof from the aggregator P2 and Bob will send seven tokens to an L1 account he's preparing to do a withdrawal so that's P3 now if you look at their wallets which are this proofs that they have to keep up with Alice will will merge the two the two proofs P1 and P2 Charles will do the same while Bob will have the P1 received from Alice and the P3 um it receives from he receives from the aggregator and now if you unfold this one I know this is quite heavy you don't have to go through all of it but what I want to show is that

for example if Alice will send her wallet to the to the rollup contract and wants to compute the balances of all accounts against the history that happened this part here comes from the deposit it this part here comes from the second Block in which she sent seven tokens and all of this part here comes from the last block in which she showed that okay I send uh three tokens to C but in that Block B appears as well as a sender but Alice has no information about the proof that that uh Bob received so we compute this as a partial transaction we don't know anything what

happen we don't know what Bob did there Alice doesn't know and she shouldn't know right so we put this as bottom it's like undefined we don't know anything and then when you start to compute the balance function okay it does naturally so this is the account of this is the value of every account and okay for example here we are expecting that okay here after Computing the three transaction Alis has one Bob has seven and Charles has three right and this is the source account which is like the almighty account that is used for the rollup contract but now when you try to reason about the partial transactions of which you don't have enough information and they they don't know what Bob did

they will say okay I set the the account of Bob to zero and I will reason about this and as depending on how many blocks and how many entanglement you have in your blocks you will get this this part right now if you look at the information Bob has at this point and you try to compute the transactions that come up there so remember Bob had P1 and P3 right so Bob's received seven tokens from from Ellis but then on the second transfer blog Bob has no idea what Ellis did at that point right so here we have two partial transaction on what Ellis could have done right but we Bob knows like I want to send to this L1 account

seven tokens I want to do a withdrawal and you reason about this now the part is like how is the double spending happening right and now that the withdrawal step ensures that the user cannot double step spend the the withdrawal um the fun um to withdraw the same funds twice or to overspend and this is the very nice part of the mathematical behind the paper and I Let's Twist a bit the scenario and let's imagine that at the end Bob wants to send nine tokens initially he had just zero let's suppose he wants to withdraw nine Tok tokens right he wants to to to to send to an L1 account n tokens which obviously he doesn't have at this moment

and what happens if we go back and we we do the same process we compute the same balances and at the end the protocol at at this point will just set the the account of of Bob to zero but actually because they use latis order groups they are taking the minimum available between the the the the a all the time they reason about the lower bound the minimum of the values that they're possible to move so it will take the infimum between what Bob had in his account and how much he wants to send and all the double spendings are set like this you the protocol this magic balance function

will set everything will not allow you to overspend more than you want and everything is just doing Meats in latices and that's very beautiful and there is a very nice part because here it allows a partial transaction right it it withdraw just seven tokens because that it it is what he had in in the balance right um the protocol is so General that you can twist it and playing with the balance function you can obtain whatever design you want for your protocol so I invite you to look at their white paper look at our formalization and see the the beauty of the protocol now obviously what I presented here and I said from

the beginning for sure this design the simplified design lacks privacy because transa uh by the proofs they receive the users can see the accounts of um of other users and that's not okay but you can use ZK proofs for this and that's fine and nothing nothing bad will happen and then it's not super efficient because balance proof are large and are expensive to compute on chain and they have a very neat way of of solving this problem but I just wanted to show to go to the LA disorders and show you how how you can handle this okay and please reach out to us if you have further questions thank you thank you Dena