Securing Web3 with the Push of a Button / Andreea Buterchi

Transcript

today's I'm going to introduce you to our security the service platform and show how users can use it to secure their web tree projects but before I'm talking about our platform let me give you an overview of what we do at very dies so uh there are two main components to veritise this business logic and one of these components is performing web security audits how what we do at Veritas is to go beyond auditing and we are also building tools that can automatically detect bugs and vulnerabilities in webg projects and we build the security the service platform

for the generals so what I'm going to focus on in this talk is the security is a service platform we've been building and show how the users can use it to secure their projects at each development stage all right so at a high level the very nice SAS provides instant access to push button security analysis tools that are based on state-of-the-art formal methods and that allow developers to get audit results in real time and uh the main question is here what is formal methods so formal methods is a set of mathematically rigorous techniques for automatically finding

bugs and constructing proofs about software correctness and we can classify this formal methods techniques as either dynamic or static and in particular the dynamic techniques execute the program on interesting input and monitor what happens and with with the goal of finding a particular bug while the static techniques don't run the program but they analyze the program basically stare at the source code and try to reason about all execution paths all right so now that we clarified what is the difference between this two formal method techniques we can zoom in on our SAS platform and show how users

can interact with it so basically the users have to provide two things the source code and a configuration file which indicates what tool to run and some additional parameters required by that specific tool and under the hood our SAS platform will run that tool and output a report that contains all all the findings so before diving deeper I would like to highlight some Salient features of our platform first of all it is powered by multiple security analysis tools with complementary strengths as we will see in the next slides and it's offer support for multiple black blockchain

languages because it was built in this blockchain and then with diagnostic way and it also allows checking for common vulnerabilities as well as custom specifications all right so um on the next slide we will explore how formal methods tools can be useful for preventing the defy attacks and for that we will use a case study which involves running this so-called flashlights so for those of you that are not familiar with the flashlight term it is a type of loan where a user borrows assets with no upfront collateral and then they return the borrowed assets in the same

transaction and if that doesn't happen namely the funds are not returned the flash loan is supposed to revert okay so let's start analyzing this flash on contract which implements the erc2156 standard so I will walk you through the uh relevant parts of it and we'll focus on this flashlight method first so this method implements the key functionality of The Flash loan contract and it takes three parameters the receiver of The Flash loan the token uh the flash currency and also the amount

to to borrow and let's see what this function actually does so in this code snippet this function checks if the amount to be borrowed is less than the balance of the of the flash on contract and if that's the case then the receiver is approved to uh to use their old allowance plus the requested amount next this method invokes this on flashlight method which allows the receiver to to use the the funds and finally this method will will check if the the receiver

returned the the expected amount which is basically uh the amount they are using within this own flashlight method plus some transaction fee all right um so this looks like a reasonable implementation of the flashlight on contract however let's ask the very nice tools if this contract has bugs okay so the first tool that we are going to use is Vanguard a static analysis tools that can check for common vulnerabilities such as re-entrancy flash loans and so on and the users can interact with it by providing the source code and the list of detectors and then

Vanguard under the hood will will run the source code against this list of detectors and will output a list of potential issues all right so we prepared a demo of Vanguard and let's see introduction oh really oh it's not available [Music]

okay so now Vanguard runs and we'll output some helpful information for for the user for the users while it runs and in a couple of seconds we'll see the output of it and it indicates that it found three entrance of vulnerabilities all right so let's see what Vanguard is telling us more precisely so it says that when the flash on currency is ERC 777 then the transfer from function of it invokes on a known callback and after this callback is runs then the balances field is updated based on a potentially stable value

and we are asking if this is actually a vulnerability because um we know that this kind of tool static analyzers can also output post positives and for that we are going to use another tool which is orca to investigate further so Orca is a specification guided advising framework that can generate concrete evidence of exploitability so basically the users provide the source code and a specification and orca if it finds a violation we'll output this counter example which consists of a set of transactions along with their with their input that led to to this

violation of the specification all right so we also prepared a demo for Orca so let's see it in action we will check if the balances of this flash loan contract are preserved so the next step is to run Orca against the same code base as we're on around Vanguard on and to provide a specification we can provide a custom specification or we can choose one from our specification Library so as you can see here we have specifications for the most common ERC standards so we will choose one of them we will I will show it to you on the next slide all right so now we let Orca run during the execution it will output some

information regarding the the remaining fuzzing time and the number of transaction issued and in the end uh Orca informed that that it found a country example and it provides us with concrete information about uh how to initialize the environment and what transactions to perform in order to reproduce the country example okay so if you are wondering um find this country example well this is the the specification we provided it as an input and it is written in a specification language developed at very dies called V so in plain English this uh this specification says that it's

never the case that after a successful call to the flashlight function the balance of the flash loan contract decreases basically no one can still found from from the flash on contract all right so that information uh you saw on the previous slide can be translated to this uh uh to to this attacker contract and uh let's analyze uh it on the next slide so basically this uh this is how Orca initializes the contract involved in this attack and then it provides the flash on contract with some tokens to uh to loan and then it deploys this attacker contract so let's see what

this attacker contract contains all right so one important thing to note here is that it uses this erc77 token as the flashlight currency and um since the transfer from method of the erc77 makes a call to the tokens to send um if it is registered we see that the attacker does that such that it can perform that that call during um during the attack and next it uh its initial it initializes the attack uh and borrows 65

tokens from the flash on contract okay so let's see how these two contracts interact we come back to the flashlight contract and we see that it invokes the on flash loan method and this on in this on flash method as I mentioned initially the attacker is supposed to to use the borrowed Fund in in some way so let's see what happens in this method if we go back here in the attacker contract we see that the attacker does absolutely nothing with the flash loan and it simply returns this callback success which will bring us back to the flash loan contract so we move to the next code snippet and

we see here that the flashlight method tries to transfer from the the receiver The Borrowed amount plus some fee but um if we um if we remember the the attacker didn't do anything with the fund and the amount that has to be transferred back is only the fee right also recall that the erc77 makes a call to the tokens to send off the attackers so let's see what happens in this tokens to send method so in this method we see that the attacker does something very sneaky and transfer 42 tokens from The Flash loan to themselves and this is successful

because there is a bug in the flashlight contract so because the defeat to be transferred is less than the current valency of the attacker which is 42 now because they transferred they stole the the money from the flash loan they call succeeds and the flash on complete successfully and yeah so the conclusion here is that the attacker stole 42 tokens because the allowances were not set to the initial value before the transfer from call all right so despite looking reasonable this contract contained a subtle bug that was caught by by our SAS platform

and just a recap of what we did today so we started by using two tools in the SAS platform to find this serious issue and first we use this inexpensive static analysis uh tool called Vanguard to scan for potential problems and then we used a filing tool called Orca to investigate further and generate a concrete exploit right so we anticipate that this will be a typical usage for uh for our SAS platform in the future all right so the main takeaway here is that the automated formal method techniques can augment human

intelligence and make it easier for developers and Auditors to catch critical bugs and if you are interested in testing our tools we wanted to let you know that we accept better clients for our SAS platform so make sure you contact us after Disco talk okay so um forget that we are also performing audits how we audit in the past device ammas stable coins wallets and also zero knowledge proof circuit and here is a list of our previous clients okay that was all for today thank you very much and if you have questions I'm happy to

address them so um is it possible for the API tool because this is basically an API tool right yeah um is it possible for it to also detect the type of the contract for example I just upload a solidity file and it says okay this is this is a flash loan contract or this is some other sort of contract can I do that as well not checking for security vulnerabilities but just for the type of the contract something that it can do that right now

but it's an interesting feature so yeah are you looking into that because that okay yeah and also uh what would be the do you have an like approximate cost estimation for the SAS tool like how much would it cost for now it's like it will be free for three months right for the better cost after that we'll figure out how much we will the customers for for our services okay yeah based on the usage and so on and the complexity of the projects there are many you know criteria here and are you looking into publishing the uh the public

uh some open source versions okay yeah that would be cool as well because I used to use it a lot and now you made it private and that's a big bummer because we are you know open source and which part would be uh integrated with the SAS awesome okay any other questions can I but so if I will use your apis expected can I pause withdrawal contract I subscribe to your service SAS service

and I receiving some other message like can I pause my video contacts if restaurant will attack will be detected on another attack will be detected can I pause my uh is it possible to post the withdrawal contract if there is an attack I'm not sure like we are only detecting the issues like we are like our 2019 degree to be the main network if that's our question right uh I think that that depends on you right it doesn't run all the time it doesn't run continuously but you need to literally create the request for running the audit at a particular time on a

particular contract like it's not running in the background uh automatically and once it detects the vulnerability you're the one who actually takes needs to take action on the contract and then you can pause it I suppose but yeah I see so yeah that's the main purpose of our SAS platform right you can use it uh before deploying your contracts to secure your product right to make sure that once you deploy it it will be secured and yeah yeah right um yeah I think that's my that's my answer to your question any other questions um

just one question um since this is entirely off chain have you thought about maybe storing the data you retrieved by the API on chain because then you could use it on chain for example if you store the security of a or the security of a flashlight contract that you audited on chain then are they could theoretically query that data and basically block any malicious contracts have you thought about that as well clone the stage so basically we can also audit contract that are deployed on the

main Network right and we can clone that particular State and you know run our tools on on those contracts but we don't have these features like report no potential issues existing on the main Network already but we are looking into that because yeah because that would be tremendous for the web 3 ecosystem because right now um smart contracts are entirely in the blind on chain when it comes to security and you have off chain PDF documents which store audits but they're entirely useless on the blockchain itself because you and um if you could do that on the blockchain itself you could actually well make a security ecosystem right

yeah that's true yeah yeah thank you uh just one thing I heard there's a very nice uh tool in the making called turtleshell.xyz you can check it out um yeah basically it basically tries to do that it basically it basically it basically tries to store that data on chain to make it workable so yeah we would like to okay so thank you guys that's all for now [Music]