Ensuring Security : Formal Verification in Account abstraction

Transcript

okay hello I've been told that I can start so I'm going to go ahead and do that uh so I'm John I'm the CTO of verdice originally this talk was supposed to be given by our CEO yufeng but unfortunately he wasn't able to make it and so with a few days notice I had to take over and so this is going to be fun because I definitely know all the slides okay so let's go ahead and start talking about account abstraction so I'm sure a lot of you have been hearing a lot about account abstraction lately and so I'm just going to spend a little bit of time in the beginning to give a brief overview of how it works and so if we

look at like an eoa right now you have an individual and they've got a key and that key is going to give them access to several things so it's going to give them access to things like their current eth balance their nonce and so on however other than that there's a lot of things that an eoa doesn't get and so that's where smart contracts come in so with a smart contract uh you get a lot more things so you get all the things that you do with an eoa but you get access to some additional aspects so you get access to code and you also get access to storage which is great because that means that now uh you can do more things than you could with an eoa and that's why smart contracts have more

utility than just end users so the reason why account abstraction has become a thing is because eoas have several issues right so you end up having a key that is deeply coupled to an individual and so if you lose that key then you know you've lost tokens there are other issues that we can talk about but I will do that a little bit later and so here is that later so basically another issue is you can only pay for gas and stuff like that with eth whereas a lot of people would like to be able to pay with other tokens but in order to pay with other tokens they often have to do manual swapping and stuff like that and possibly incur fees that they weren't otherwise

expecting they can also only use a single type of curve in order to sign a particular transaction and so people who want different security models or perhaps greater security now have to use or are forced to use this particular ecdsa scheme and then finally uh there are other questions like what if you want someone else to pay your gas right now you have to pay gas there is not a very good way for other people to pay it uh for most end users and so that's where the eip4337 came in and so for those of you who don't know that is the standard that defines what

we call account abstraction and so the important part is here what you can see is account abstraction ends up defining a lot of different things it defines user operations uh entry points and so on and I'll get to what all of these mean later you don't have to read all of that the important aspect here is it has concrete roles for people to actually perform and it has descriptions of what someone should be doing in order to fulfill that role so the reason why that's important is because these entities and their interactions can be encoded into logic and then checked and so that's exactly what we're going to do we're going to take a look at the specification and code the behaviors that we see as logical

formulas and then use formal verification in order to ensure that people are actually following the specification correctly and so just to give you a little bit of a more of an overview of how this works essentially uh where this starts is you have a user previously a user would submit a transaction and when they submit that transaction uh they would do it directly with blockchain here they're going to take an operation called a user up and they're going to hand it to someone called a bundler that bundler is then going to be responsible for submitting all the transactions all of the bundled transactions to an entry point that entry point is then going to be responsible for one paying the

bundler but two it's also going to be delegating the user operations to the appropriate source so this could be like a payment Master the paymaster is going to be the one who pays the bundler fees for things like gas it could be sending the operation to a factory to create new contracts or sending the operation to a wallet and that wallet will be doing a number of operations like transferring funds to another user so if we look at some features of account abstraction it allows you to do things like pay for transactions and currencies other than eth so that's great because now rather than having to worry about how much eth you're going to be spending and having to make sure you trans for the or swap the appropriate

amount of usdt or something like that to eth you can just go ahead and spend your usdt it also allows you to ask other people to pay for gas that can also uh be really good if you're like let's say performing a service for someone or if someone is asking you for payment and finally it allows you to support different validation schemes so you're not now stuck to a single ecdsa curve you can now use a different scheme like multi-party signatures and stuff like that so and then finally there's support for additional recovery schemes but these are all the good features of account abstraction but there are things

that can go wrong and so we took a look at publicly available GitHub repositories and specifically issues that people had posted in these repositories and we're using that in order to determine some of these violations that I talked about previously so I'm going to show you a couple of these violations that were fixed by the developers of these repositories and also describe how they could have been found rather than you know manually by someone inspecting the code using formal verification so in this case what happened was you can see down in that red part down at the bottom uh there was a line that was removed and replaced with the line to

the right the reason why that happens is because in the specification it says that the max fee per guess is going to be the immense the minimum amount of fees that someone can accumulate however the function that would Max fees per gas replaced performed a minimum between uh Max fees per gas and another value which meant that technically someone could have uh someone could have been charged gas under the minimum that they specified which is against the particular EIP specification because there are reasons why you might want to pay higher gas in order to ensure that your transaction is being picked up correctly

another reason or another bug that we ended up seeing in here is one right here so this one is implied by the EIP specification but it's not exactly well defined so in the EIP it states that the stake value is expected to be above the men's stake value however you know a lot of things can be above the men's stick value and when people are performing operations like uh casting or uh you know ensuring that values fit into a particular int you can have overflows and so an important thing to note is that the EIP specification has a lot of specs that perform or that

provide safety properties but that doesn't mean that it is comprehensive there are other things that need to be checked so for example for values such as this one it's important to ensure that people are properly uh maintaining or properly checking the values of uh or the values that can be taken by individual variables and so finally this one here is also missing from the specification basically what you can see on the left is on the left it's performing an operation that should be guarded by a check of the user signature so essentially it's checking to see whether uh whether someone should

be paid however previously in the code there was no check to make sure the user was who they said they were they weren't validating that the signature was correct and so there are several locations where the signature needs to be validated otherwise someone could let's say submit a user operation claim to be a potential user with a bogus with bogus signature and if that's not actually validated then well they can actually end up scaling funds that way and so on the left hand side is the original code the right hand side is where they added in the specification or this code that ends up checking that the signature actually matches the one that or the signature for the operation

is correct okay and so now let's take a look at how we might be able to formally verify some of these properties that are both implicit in the EIP standard and explicit in the EIP standard so the way that we're going to do that is we first need to encode these specifications into some logical formula and so the way that we do that here is we can either just encode it as some sort of mathematical formula over the values of the contracts so that's what's done in the first case and the or what we can do is we can Define certain predicates that will help us will help us actually Define

relationships in the contract itself so that's what's done down below so if you're curious the one down below basically states that there's a data dependency between the user operation and the public key and then that in turn is control dependent on the return value so it basically states that somewhere someone has to actually check the return or check the public key in order to properly return with some value and so basically the specification used here will use linear arithmetic formulas as well as some custom predicates in order to allow people to encode these properties then what we're going to do is our tool is going to take in the source code as

well as the property that's going to be checked and it's going to use a technique called abstract interpretation so the important thing about abstract interpretation is it is going to reason very abstractly about the program but it needs to know how to do that and so that's where this abstract domain comes in I'm not going to go into depth about how abstract interpretation works but if you're curious you know catch me after and so after you know taking in those things it's going to reason about the source code itself and then it's going to report any potential violations of those specifications or common vulnerabilities so now let's take a look at the work that we've done so far so so far we've

developed a total of 71 specifications from the EIP standard we've collected 24 benchmarks with that are buggy from open source account abstraction wallets and this is going to include some popular account abstraction implementations such as ethereum's reference implementation and soul wallet and finally each Benchmark is okay so each Benchmark is going to correspond to a specification violation and so that's why the number of benchmarks that we have doesn't correspond to the number of specifications that we have because we are specifically looking here to see how we might be able to find violations and

so each Benchmark we're looking to make sure it returns a counter example so now if we take a look at the specifications uh most of them 56 I believe are explicit in the EIP standard however 15 of them we identified are implicit specifications like the public key specification I showed earlier in addition we found specifications over a number of the different entities that I showed you earlier and so some of them apply to user operations most of them apply to the wallet itself but basically it defines the behavior of all aspects of the account abstraction so if we look at some of the preliminary

results because this is ongoing work that we're doing currently we have evaluated 24 of those benchmarks and we have found that actually all but two which would be 22 are solvable and if you're curious about the size of the benchmarks that's shown on the right but essentially each one of the contracts I think has an average lines of or an average number of lines of code around 350. and so the important thing here is this can actually be used to identify bugs and in most cases it does so just to give you a little bit of a

takeaways uh the EIP standard does specify safety properties but it does not completely specify the necessary safety properties that one should check for it's um so in addition issues in these implementations can also be found by looking for specific specification violations from the EIP standard and uh basically it's possible to check your code by using logical reasoning like this formal verification method so in conclusion uh there are a couple of other talks that paradise will be given giving over the next couple of days so in I think a

couple of hours there's going to be a talk about Magi and which is a formal verification infrastructure for Cairo and then tomorrow there's going to be a talk about pikis which will automatically find under constrained bugs in ZK circuits in addition we partner with a lot of people in this space we're a security company notably we are one of metamask's uh preferred Auditors for their snaps and those are our socials if you want to learn more thank you [Applause] [Music]

thank you [Music]