Exploiting and Securing DeFi Projects with Formal Methods

Transcript

sure yeah very jealous of you guys in paris yeah so hi guys have you ever wondered how come those uh hacks hackers from last year called so many million dollar diva hacks you know are there any ways to discover them if you're interested in those questions thing you know you're in the right place because in the next 15 minutes i will show you how to explore and secure d5 projects with something you know uh called the formal message so first a little bit about myself my name is and i'm currently uh doing this aesthetic and uh we have certainly do things like auditing and crypto infra things like compilers and verification etc

so uh formal messages have always been kind of the password that you know one of the bathrooms that i will see him talk about if you do a google search you can find actually thousands of papers and you know under the blog posts about it you know with even dedicated channels and workshops but what exactly are those contents about let's take a look you know you see that everybody thinks that forum methods can solve everything and of course besides community enthusiasm not to mention people like us in the auditing business you know uh who are extremely bullish on forum methods

in formal methods using blockchain security so uh you know but what what does it look like in the decentralized finance world you know boom and boom the truth is who uh you know we who are so bullish on the former asset side did not deliver our promises to d5 community we have failed to find those vulnerabilities and we were wrecked and from methods are not used in d5 so uh the the formal methods community has produced many technologies up to now what we have here are things like steady analysis and

semantic formulation but uh now the real question is you know how can we use the mean design so before uh i i we go into an answer that question i want to first use an analogy to give sort of the teaser to you guys and convey a simple version of the idea of our answer you know because uh in the crypto community we have always been comparing uh building d5 protocols to assembling lego pieces and therefore goes my word money lego so what we have in mind here is to maintain this uh the piece of this uh and integrity of this uh fancy lego castle to prevent any potential problems when we are building

it and you know there are actually two kinds of problems the first one would be you know to find those broken lego pieces in this castle uh this corresponds to finding vulnerabilities in uh in one of the uh critical financial models and the other kind is you know this very prevalent from the composability issue what if there are some uh possible harmful and non-legal ways to compose those minor egos so how can we start with those two problems with what we have will have to make the expression within your financial model simplify easier what are financial models right uh let's take a look at a quote from a veteran auditor

uh if you're going to define audit without a full understanding about how options the derivatives work you're probably going about it all wrong so uh and here the understanding about options and derivatives is the financial model part that is extra to the traditional software security that we should now uh paste that pay special attention to so uh what about a concrete example you know let's look at the uh the balance hack with the stereo happened last year which perfectly illustrates how how weak our little castle can be when we find we have some unsung financial models so in this case

um the hacker first borrows flashlight for his initial capitals and and then he does all these seemingly meaningless transactions of repeatedly trading wath and the sda tokens back and forth you know but what he's really doing is taking advantage of stereotokens deflationary mechanism that you know you can see here every time the attacker does a swap involving a stair fda token on balance the balancer pro receives uh one percent less sta than what was expected and this inconsistency between balance of spoke and his actual uh and his actual holdings

ultimately uh led to the hack so at this point you're probably wondering how how we can find financial model hacks like the one that we just presented a natural solution is to model all those all the components the hacker had used step by step from the threshold dydx to tokens profit taking step and finally the money laundering stuff but how can we possibly verify something that involves so many lego pieces so here's our proposal we take a divide and conquer approach first we verify

each individual module this corresponds to the individual lego pro block broker problem and then secondly we uh on top of that research that if there are any vulnerabilities caused by the composition of those modules this can this corresponds to the illegal compensation problem so in local language this means that we only need to consider details in the blue block and other blocks that the blue block depends on are reduced to specification that is we only have the detailed implementation of the developer we want to verify for others in our specifications and then what is search so for the composability flaws we say that

if starting from a sensible state then if there is still exists a trace of cost to those manila eagles so that risk-free arbitrage can be performed then they essentially exist a hack so this seems like a very uh hard to prove properly right so then some optimizations we uh kind of we can do is to say that research on finance space and through nonsensical states that means that for example when we consider five factorial permutation setups to compose those labels so as a first step to demonstrate our approach at the device stage in the divide and

conquer strategy we present how to use you know deductive verification with smt servers to prove some basic theorems about initial v2 so essentially we proved three lemmas that we call swap pregnancy reserve synchronization the increasing product which basically captures the minimal features of a constant function market maker so and our implementation is called salvik which you know is based on the y3 verification language so uh zavik showed us that current smt methods proved some basic zooms but many other

d5 theorems use advanced mass so to take the same units of v2 protocol as an example it can also be proven to have some properties like immunity to oracle manipulation text and there are some previous works on this one but they're really done on pen paper which does not show hard evidence on the implementation practice and the formulation of current pen paper proof requires the use of some uh real analysis results which are beyond what smg's can solve so uh to do for use to be able to define uh arbitrary mathematical constructs we

bring proof assistance like clock onto the table specifically for our units of proof case enables us to use advanced math libraries like clock interval and in our proof specifically we use the general version of timer lagrange theorem formulas in the libraries columns required for the arc manipulation immunity property yay so uh here we have the uh so what we have here is the world's uh first formally verified default protocol and we were mechanic we were able to kind of verify the pen paper proof on the arc manipulation property you

know say that the custom manipulation token prices in the emm is high and compared with and paper proof this this formalized proof is more rigorous about integer approximation in the actual units of implementation you know for example consider all kinds things like running arrows and for the complexity composed about you know a thousand lines of cog and 400 lines of smart contract yay so we can do it so to conclude establish methods and existing courses from application can handle some

device rooms this means that broken lego pieces can be effectively eliminated and we don't have to worry about them because we know we can do it and don't talk we'll start just kidding you know but this is not good enough to move the needle as it does not consider the compressibility problem uh it's a the illegal composing duty lagos which is a major part of the fight security so even though it's our wish that defy security can be solved by just immunity broken blocks but you know we're not as a set which we should now consider the second stage in order

in our divide and conquer plan where we search for compressibility flows so our attack plan in one sentence is basically to use our tracking to search with reality we and we model you know the way we do it is to model depending default protocols using a domain specific language as the specification of the project's survey implementation if you remember the graph from early on this is a gray block that the blue block depends on yeah so specifically for our language we use we use deep c which is uh to extract and encode the programming

format suitable for mobile checking and to search it we research a refined version of the previous property so we can further optimize the composibility flow checking with insight that most e5 particles are forks with similar functionalities and uh you know i i'm sure you're all wondering is it really possible to search such a complicated property on the already complicated europe for the course well uh we actually don't need to search everything so for example from the balance and sda hack early on there were 27 swap function calls for wh

pair alone and 50 plus for the entire transaction we only need to consider the core of the hack which are the blue modules and there are only need to be a few sda token transfers to trigger the attack which is more than the transaction fees of balance so we were able to find attack with in a limited number of calls yeah so one further optimization we can do is to have the inside that you know many of those protocols all have the same same functioning i like adding liquidity masterchef style staking rewards or small mining blah blah blah and another thing uh you know this is because bsc has been accumulating

popularity for the past few months and you can see that most hacks on bsc are forks with some tweaks please down for the uranium finance one which is a tweak of the units of v2 counter contract yeah and then as result of those insights we are in the process of building a dsl model default library one which contains you know variants of the d5 projects with a tbr larger than 50 million gas dollars and i want to highlight that this is a non-repetitive work which means that it can design we can be used for divine conquer approach in the future so to conclude we

we have seen evidence that the spectrum of chromosomes ranging from direct verification to proof assistance and to moloch hacking works for d5 and at this time we can confidently say that we have the ability to build a legal castle that is strong enough to withstand the flow of the big bad wolf and their lego building tip was takeaway and actually in this time i want to call for a manifesto based on what we have just done that as a community we should really push for the full methods using fifa but it is it's more than that there's some deep ideological thing that we should all watch for here that embody the various foreign of crypto

by replacing trust in human auditors with the mechanics decentralized version of provable security so it really is about another step into the trust minimization process you know yeah so uh actually democrat has this defined gives the power back to the community so our strengths is stronger yeah so uh thank you all for listening and i hope my talk did not just inspire a bunch of hackers and so uh no skill anytime oh

you