Where to Introduce Formal Verification on a DeFi Protocol like Aave - Part I

Transcript

uh hello everybody so I'm Ernesto as he introduced I'm from BD labs and and today I will be doing like a join talk slash workshop with Tomer from from sartora let me kind of work together so first a bit of what exactly is bgd Labs because sometimes it's a bit confusing so be large is is a team that I co-created which which can be considered like a bit of a spin-off from the avatar from the

other plot Google so for a bit of background before I I co-created the VD Labs I was a CTO at companies which was the the team that developed the double protocol like from the B1 version B2 currently B3 and then at the end of 2022 like following like the decentralization of of basically everything even of the organization and I I decided like to to create a separate team a development team and from beginning of 2023 so more than one year no from beginning of 2022 sorry

uh more than one year ago we actually have been the we passed like a proposal on the avidau to to be like the the official like development team doing providing services to the to the daudi so yeah this is the what is what is vgd labs and which is a relation with with other so uh Wow first of all like a bit of like the the style of the of my talk I I I saw and like I mean this is the the device security submit so the big majority of of the toll for what I see are are coming for from the top Security

Professionals that we have here I'm not really like uh like a security professional like I know certain things about security I think at this stage but I'm on the development side purely so um basically that is the idea of the of the of the joint call uh talk that uh I will explain with my my experience like with the formal verification like in uh quite production protocol we could call uh like Abe and um and then like Thomas will go into details like of exactly like uh how it really works in the practice like on the on the different projects somewhere like

uh sartora rules are are applied into into the other protocol so so yeah mine will be more like a high level bun and insights yeah so uh first of all like uh some com misconception is that like Abby is like this liquidity protocol on where people just goes deposites collateral bore against or some other just deposit multiple tokens and and earned yield on on them actually it's a bit more complex than that and a bit there is quite more variety apart from that so yeah there is

the liquidity protocol and that is the the thing that we have is more more well known for but apart from that there is like a governance system uh launching system of smart contracts like to boot and to actually take decisions on the on the other product itself of the liquidity and yeah that is like oh there's like incentives management like for which is quite separate from the protocol itself but connected to it so whenever like somebody wants to give incentives for using the liquidity protocol there is also like uh the so-called safety module which is a method of protection like if anything will go wrong on the liquidity protocol hopefully not the safety model on where

like Abby holders stake could actually be a slashed to to cover a potential loss and yeah the last last piece is a stable coin that actually will be live tomorrow I think if the depending on when the proposal payload gets executed but but yeah this is the last addition so to to the whole ecosystem so as you can see like a basically almost all the parts of the defy puzzle or even almost blockchain applications like were touched and they are covered by by having one way or another so yeah this is more about like the yeah

the insights of how exactly like um security is is managed in other how is our approach and especially how how it evolved over time because this we are doing this like for already I think in three years live since 71 and things have really changed I would say the same as with the security ecosystem itself so ah as the big majority I think is aware like this is important is before deploying smart contests as uh once once the protocol is live obviously there is

um way more other stuff to dig into account but before in deploying starting as Marco what exactly do we do like what we did like in in Abu back in the days what we are doing now in bgd labs and so on so we just start with testing with testing I I yeah I think almost everybody familiar I'm referring with unit testing like with certain integration testing of the of different uh independent systems of smart contractors sometimes not smart contests like so let's say the classical testing in software as everybody understands I think the peer review is pretty important like so internally the team whatever is the team like because with this with the

centralization sometimes is not exactly the same team but there is always like steps on where well you're really good of each other and you check that everything is as it should be uh the security reviews which yeah a lot of people call them like manual audits at the moment and this is basically let's say snapshot a reviews of external parties which are experts in security and yeah you once you think that the the code is ready peer review is finished testing is robust ideally everything a new four where are you engaged likes on third

party security auditor that that will like review everything and and check that nothing was nothing was forgotten or there is no go back and the final piece is the so-called formal verification and yeah it's important to to highlight that I'm just using like the informal way the formal verification concept to refer like mainly to what we are more familiar with and what we really use that is like the the sort of a property check so a bit of a also background of from where it comes like the the relation

between Avengers first well it actually starts with it before of the first step of rb2 um but B2 was the first formal step so back in the days when also tour I think was starting a they were reviewing like multiple live smart contests out there and one of the ones that checked in detail even if abedin really asked was like the app Smart contracts and well first of all like they found like some some interesting stuff and second like that the the approach that they brought to the table was quite different like to to

everything that we were doing before which nowadays maybe doesn't seem so special like but back in the days like when running rb1 and especially when when rb1 was really growing to to big numbers like we were just really looking for everything that that you can imagine in terms of security so after after this initial contact let's say uh with rv2 we already like when I was like on on Lobby on the Genesis team like we engaged with with sartora like for for basically like a review and also like for formal formal verification to apply their technology of property checking on the on the other protocol in this case the liquidity

product ah this continued with hobby E3 more or less the same so like property checking but to the new iteration of the protocol and things we got like even more interesting with uh I think yeah for sure like more than one year ago when uh sartora the same as bgd Labs like engaged directly with the with the abidal which basically with the smart contracts holding the holding the permissions and the funds of the system um four services like it really to to the Dow and basically obviously to the to the development contributors to to

the dark chairs so now yeah I think a bit of of the context uh so how exactly that is the the core here like how exactly do we tackle like for my verification and property checking on online so first of all like is it's important to understand like why with C value like on applying a property checking not only like what do we do so rb1 B2 and N3 a they are pretty complex system let's say so not really like comparable with some other traditional software I will say

but the the nature like the open Nature like the the type of accounting that it has tokenization different types of flows of user flows and basically everything that is built on top and makes it pretty complex like um to even tourism about so the quite uh quite difficult thing that I say is that when we develop like rbb1 and we released everyone I think we learn like fifty percent about wb1 once like it was running not so much about the environs but in terms of like how people was using rb1 then

because of this complexity and precisely because you don't even know how people is using the is going to use the system or how like I know different other smart contractors are completely are built on top is not really easy right to to just do traditional testing and especially be sure that your your testing will cover will cover all the cases and you will not have any problem and you will sleep at night when when you have like yeah 50 million dollars in the platform then obviously um we thought about fasting that I think it was explaining like in the two or three previous previous talks and for us

like we even we even implemented on rv1 like a really small engine of kind of us and let's say that we call scenarios and the idea was like to well if you don't you at least need to replicate certain conditions certain scenarios on the on the protocol that you envision and and test based on that and be able to generate those kind of scenarios automatically less not not exactly but automatically so we experiment a bit with that but yeah it gave us what we found during development problems using these scenarios it gave us way more confidence that is true but at the end of the day like we were not not completely happy

with with that because still like you you always have this insecurity that you don't really know how it's gonna get use your protocol out there then another point is that yeah we did multiple objectives of one we did more on our way to more on rv3 and still like we kept seeing the scene the same that is like the security reviews even from the top participants like on that I think a lot of them are around here like they were missing something and and not really missing because the war was not well done then is when we notice that it's just not so easy

to to notice which like this really educations then yeah so formal verification a one of the main themes of formal verification is that it catches certain types of bugs I mean it catches basically a lot of or the majority of the bugs depending on the code base but even with well-tested code bases like and and well audited code bases still it keeps it it catches lights from bugs that are pretty dark I would call it dark I refer that like you don't really think in that direction when you while you are developing like a system another point of of why formal

verification is that um well good practices within an early field like defy lack of or smart contract developments like they are always not so so good hours at the beginning for sure were not the best and improved a lot and the moment that we are starting in like incorporating formal verification to our code we we immediately noticed that we started thinking on having a better documentation better specification in some cases like we were yeah we were doing some kind of technical paper apart from certain white paper but it's not exactly the same because you are not really defining the specification of the code just the high level idea of what is

the system and the for me the the most important of of all is that hormone verification is a tool that allows you to protect against the what you don't know so they don't know and this is like the a quite critical point especially like in a system like also you will have like malicious entities like trying to exploit A system that holds a lot of user funds all the time in a completely open environment and with in some cases not so much chances like of having a solution one once the event happens so this is incredibly invaluable that if

you have if you can have any tool that gives you some yeah predictability that it doesn't matter what happens on top but the system should be safe always and you don't know what could happen so yeah it feels like the the Holy Grail here like formal verification and it should be applied by all the systems for everything and so on but well not exactly like that at least from our perspective sure you can apply formal verification um yeah I think almost any smart contract out there because at the end of the day is a is a way of like checking that your specification and the code

that you write are the same like kind of the same but I think it was mentioned in the in the previous in the previous talk that if you try to do formal very formally verify like any system like in a big percentage of the of the cases like first of all like the effort is incredibly High which translate in in cost of all types and well I mean at least from our experience in some cases it gives value but it gives less value than some others so so a bit of like a like rules of thumb of where we actually see like formal

verification methods in practice like shining so if the if the system is having accounting and with this like I mean tokens like or liquidity Protocols of any kind usually is is quite a good idea and this is this is for the simple reason that it testing accounting sometimes is I mean you can test accounting but certain edge cases like it's not so easy to test them and formal verification can really like tell you it's impossible that you will reach this kind of accounting problem and that is yeah it just simplifies a lot of other things

then um whenever like there is like a complex in and outflow of of assets of uh and in this case like mainly the five protocols uh this formalification is also quite quite useful because um you can Define like the properties based on how is the balance at certain point how should be how it should never be and and everything built upon those yeah another another type of systems this is a bit more abstract but uh what I call asymmetric systems and this is quite here it shines quite a lot and to put an example like other is a really

asymmetric system uh even if it has a lot of symmetric pieces like so what I mean is that on average you have like a borrow site you have a deposit site and you have a collateral side but then you have you can have situations somewhere like uh the same like an user deposits certain amount of tokens uh and another user deposit the same amount of tokens but one activates it as collateral and the other disables it as collateral true is basically it that creates an asymmetry of the system and when you combine those those asymmetries like with them borrowing Dynamics or with liquidation Dynamics or with flash loan Dynamics and then it becomes incredibly

difficult to to even understand what happens sometimes and and for sure to create like the the scenarios that I mentioned before to simulate the condition somewhere some backward up and then yeah when whenever like a system respects understand this is like the moves clear use case I will say because um yeah basically the property checking can be tried once more or less and then like whenever you inherit from for for the implementation of that standard like erc20 you can and and you put some custom logic you can plug the property checking existing already of your C20

and then add or customize your life for for your own thing so examples like of real systems on where like I can I can boot like for verification helps so iv3 for sure and there it shines really important [Music] 1.5 basically it's like the it's a token and it represents like the state tab on this backstop model we can call it the average HD module um SDK both of them I mean obvious the perfect example because it it groups all the previous things that I mentioned SDK

average basically an accounting system it was it has all swim flow an outflow a bit asymmetric to and yeah then yeah we did like some some wrappers mark on the drc4626 uh for yeah for the tokens of fog like day token so far we have this peculiarity that they grow in Balance so whenever somebody deposits an asset and there is yield like the the balance of a talk of your A2 Congress uh different to some other Implement if you like compound where the value grows and not the balance so we will a wrapper that transforms between both of them and

given that is really heavy on accounting this is the the key here like the former verification is is quite useful or yeah another another example is like the other token itself because the other token is I will explain a bit more later but it's an upgradable to like and it has like both in Dynamics like delegation Dynamics so like it's also having multiple types of accounting but I will go more in detail after then what is not so nice let's say with formal verification any content that has like purely arbitrary logic obviously is

difficult to prove how it should be the behavior because anything can happen so this is not even so much about like the formal verification itself is that you intentionally want to the system to be General so it's pretty difficult to try to limit or verify that the system is not General because it's by Design so that is pretty obvious then Crossing [Music] Crossing systems with this I refer that the is the sign that you do something on chain one network one and that reflects via some kind of preaching in the middle in network 2.

in this case is I mean it can be long like and and it's useful but for just the setup that you need to do and how you connect the the two networks like it it is a bit more complicated like to get formal verification like uh in a perfect way because it's more design like for uh like a system in isolation to start with and then yeah when whenever like there is like a certain really small developments like in the case of other every time that uh like a governance propulsion needs to be submitted and passed that is like a executable payload like so usually it's not so so useful

like to to formally verify or property check the payload itself it could be useful like and and it is useful like to do the same uh on the system that will get affected but uh not really on the on the pillow yeah and as examples of this uh so we build like on like this RBM standard Bridge which is basically a contract on where like you put a tokens of ethereum and it wraps them and bridges it to to start it and so this is purely crocheting as you can imagine and is

more challenging we did like a formal verification we we sort of but yeah it was more challenging than the others more extensively just after a but well this is challenging by itself because it combines the big majority of the steps that I say that are made difficult formal verification uh yeah and and certain proposal payloads on on the other governance like is the point of small developments not so much not so much reason to formally verified but something really important about

formal verification is that um I think together with the be secure about the the unknown I would say this is the the one that changes the most for for us in practice is the since we are like applying these techniques like we I feel that we understand better our code and we understand better our system because I mean it's a consequence of the good practices too like you kind of get forced like to have them Less overheads on the property side you get first like to Define natural language properties first of all so the moment that you start reasoning in terms of properties like it opens to discussions with the even internally

with the team and that leads you to to really understand better your your system yeah and now like for to to finish my part like before uh timer takes over like uh we have two examples and the idea is that I will present from the development side like how exactly the the system is uh and then tomorrow will go with some specific properties that they that were written like uh from the from the specific cage so yeah first of all like the the one I mentioned before that is it will be by the way like a good example like another

this just more challenging so the first is like the perfect one which is uh another token upgrade that we are planning to do and that we develop like the the code already so to refresh with the about what what is what has a special like uh just the token so token but is is upgradable by the Dao by the smart controls of the other itself M because of this yeah I mean as as it is about into like at least until now like it requires like

to have like the the so-called snapshots of balance like and also snapshots of Delegation because you can delegate your voting power to somebody else so uh due to this like um basically on every transfer of the other two and you need to do charting snapshots like which is boating a snapshot but also like for the call proposition power so it makes it like quite quite gas expensive like the the token itself and this hopefully could be optimized um with governance B3 and I I will explain it later but the the idea is that the the system doesn't require anymore like

a snapshot from the token to consider voting balance of an user at any point of time a m because of that like obviously we decided like to remove the the snapshot and make it cheaper like the the transfer of the token because it just doesn't give anybody to have it more space so what actually to take into account is that I participated like on on the development of the first version of the Abu Duke and time time ago and now I also participated on the on the new version of the token M before we were not applying for my verification now we are applying so what exactly changed

your life for us sure first of all is that the the writing of the properties like is what I said before like it made a big change for us like because even while we were developing the system uh now on this new version uh from almost the very beginning like we were thinking on first on the properties and also like in even the edge cases that were detected by other systems properties like so that that made like a big big change like on improving the quality of the of the development process then another thing is like that the it kind of compresses the tests like if we can call it that way so the idea is that

if you want to you have yeah pretty complex token that has delegation that has balance and that it has like a lot of different combinations of uh of how how those fields are so if you want to really test it like you need you need to have a huge test through it and like I'm simulate different scenarios and so on but in the case of the token is pretty straightforward let's say to to have like a property checking that is like with one property like you can cover like and have the same utility that like 100 tests like of different kind of scenarios buying a bit the the inputs let's say is did uh yeah and the well the last is that

for sure you give us way more uh confidence on accounting which when you look things into perspective like is is pretty important because you have like a token that is upgradable so we for example like um do modification of this even of the storage layout in this case and all of these will control the abeda which in turn controls the whole other thing so the moment that you don't have like good confidence on on what you are doing is not really a comfortable position like to the to develop with then on the other side let's see which is like the a bit more complex side of

the of of the formal verification we have the double Governor V3 which is radically different to the to the previous East so what is exactly Covenant between governance V2 is like I explained yes the smart contracts where people votes on proposal pillows if they pass they get executed and that creates like any kind of effect on the Abbey on that ecosystem is still exactly the same so a voting system of smart Contours with execution but well different to B2 B2 was running completely on ethereum that is where the other token lives and then using like

some some bridging to bridge decisions for change where obvious but now like Abby Robert V3 is cross-ching internally what that means is that the proposals can be created wherever like they need to be executed then or ethereum acts like a settlement layer um which as like the security but then voting doesn't happen actually on on ethereum it happens like on let's say cheaper networks because voting was really expensive and it was like a big big barrier so basically you have like this flow that this from Network a that goes to ethereum that then goes maybe to

network B to both a proposal then it comes back to ethereum and so so on and so forth yeah the this is not not so important in this context but it's based on storage proofs and that is how we do this how we move the voting to another to another network based on the balance of ethereum and the most important part like a in regards of for modification is a pretty complex State machine going to to the technicality so you have like a proposed life cycle and and then you have proposal created then is not active then it goes like on boating stay but that is

already in another chain then it comes back like it's a pretty complex steel machine a steel like what exactly like it it also improved like on our processes and how we see the in these improvements are so the verification of this state transitions like of the state machine like they become they became well more solid clearly because as you can imagine if you have like seven states and you want to properly test them you need to simulate like the different jumps from state to from one state to another like and and all the

combinations of those or majority of the combinations uh yeah and with formal verification it's a bit simpler like because we have like pretty big imbalance on the system the Tomer will will command I think so we just don't need to test some stuff ah then a as we have the property checked on like on during the development process is not just something that gets done at the end this in practice like allow us to discover bugs like while we were developing uh he he will also explain but like in typical cases that you create a PR and you do some changes that seem completely safe and then property checking yes it puts the signal that you

actually broke everything sure yeah and then this is actually quite quite important and and and people tend to it's not too simple to see but when you develop like something that has so many components like other governance B3 and you are reasoning in quite high level like on the on the development process you tend to oversee like things on the low level like at least I is something that I I I saw multiple times like not only on this so property checking as it is quite basic if if he's properly done of course but as it is quite basic like on on what exactly you define on the invariance

um when some problem appears is pretty low low level and and and basically that's like a like a seat belt let's say the the against your high level reasoning and this is pretty important so here an example is the yeah sometimes you forget about like the youth management like and there is maybe so much keys that it could be really problematic and you don't really think about it because it's maybe an edge case that most probably will never happen and and these kind of things but the property just detects it because it breaks an invariant and then you can follow the flow and actually you can improve the system just to to cover

the case [Music] a bit of summary like of the high level from the development perspective so on on level like we try to use the formal verification but not just like a hammer to to apply everywhere but we kind of think quite a lot on where we should and where we should not specialize in terms of priorities for example or projects because we have a bunch of them um understanding of the code is just game changing like yeah basically if you start to to write

the properties like in in a document you don't need any tool you don't need anything you you will for sure understand the way better your code again just jump into solidity so yeah some type of bugs are difficult to see even if you are the best developer out there yeah but but the form verification just helps um and yeah I mean good practices like it's just a side effect what I mentioned on on the initial point and the most important one again is this is like quite quite local forever but for anybody that is building a protocol that defy protocol especially that plans to scale

from personal experience I think I recommend that you apply all the tools that make you be more confident because there will always be like on open finance like a gnome there will always be some malicious actors even if they are not the majority and and well like having full confidence that nothing bad will happen is fundamental and yeah that's it now we'll go to the nitty-gritty details