Cracking the Code: Uncovering DeFi Scams with Symbolic Execution

Transcript

hello everyone today we are going to talk about D5 scams and how with the power of symbolic execution we can detect and expose them let's get started my name is Alon Ram I'm the co-founder and CTO at redefine redefine is a web tree security company specifically helping users and institutions to manage and mitigate mitigate risks including device scams and hacks prior to that I worked for the Israeli government for many years doing cyber security and crypto we all love defy because it's a permissionless and trustless nature but

the trustless ain't always trustworthy because you depend on the security and The credibility of the smart contract now anyone can write smart contracts even bad people over the past three years more than two billions of dollars have been stolen in D5 scams there are more than one hundred thousand scam tokens most of them are traded on known taxes like uniswap rockpool is the most common scam it's when a scammer develops smart contracts uh with the back door convinces user to buy it and when the price goes up Suddenly he withdraws or pulled the rug out from under the investors causing

them to lose their Investments there are several types of such vectors like prevent selling hidden mint and force transfer will cover them all what is symbolic execution symbolic execution is a software testing technique that uses symbolic inputs to analyze all the potential execution Paths of a program it is used to detect bugs to to verify the correctness of a program in cult coverage and in security analysis we will see how symbolic execution can help to detect device camps

how does it work let's say we have a simple function with some computations and if statements the first step is to replace the concrete inputs with symbolic inputs the symbolic inputs can uh represent any given value any possible value in this example A and B are symbolic inputs then we execute the program symbolically operations in the program that involve these symbolic inputs are carried out symbolically in this example Z equals 2 times Y which translate to symbolic

expression Z equals 2 times B the symbolic engines create symbolic inputs and gather path constraints pet constraints are conditions derived from the if statement that the symbolic inputs must satisfy in order to follow a certain path in this example there are three possible paths and at the end of each path we can see what is the the pet constraints that defined is bad final step is to solve the model we use constraint solver also known as smt

to find concrete inputs that satisfy the contrast the constraints in this example there are two solutions let's take for example one a equals two and b equals one it means that if I put this input into this function the function would follow this path sounds complicated let's try to explain it in in a simple way imagine you are in a large maze full of twists turns and dead ends normally you would have to go through the path making decisions at every Junction and if we hit at that end you would have to go back

this is like traditional execution of a program you give it inputs and you see where you end up now imagine that you have a magic bird's eye view of the maze you can see all the possible paths at once you can see where each the each Junction will lead without having walking in this maze this is like symbolic execution you can see all the possible execution path of a program um let's see how simple execution can identify actually scam tokens their C20 is turned out only defines the interface

of uh small contract token and the functionality can be anything so uh here we have four steps the first one is to run the token smart contract symbolically like we've seen before then we add constraints on important variables of the token smart construct like balances total Supply allowances these variables plays essential role in the behavior of the smart contract and you want to make sure the behavior is fair by solving the model we will find concrete inputs that satisfy the constraints and will prove if the

behavior of the token smart contract is fair or not let's see two examples who can mint my token um the risk with an uncontrolled minting is inflation which can lead to a drop in price uh here we see a real world scam example where a scammer added a back door to the Token smart contract with a functionality to be able to Mint an infinite amount of tokens to use symbolic execution uh we should first Define the constraints the first constraint is increasing the total Supply which means the total Supply at

the end is greater than the total Supply at start the same as for the balance of the collar at the end should be bigger than greater than the balance of the order at start now main thing can be legitimate for example in route token and LP token so we need to find a way to differentiate differentiate between legitimate and illegitimate minting for that we insert we add another constraints minting for free which means the caller doesn't give any value in return for the minting so we also Define value equals zero and

allowance equals zero by solving the model we find that there is a specific input that satisfy the constraints that we defined earlier there is a burn function and if you give it a specific input amount equals to 11 . anyone can mean an unlimited amount of tokens if if you can see on the right the this is the source code of the the scam smart token smart contract token and you can see the if equals B if B equals 11 it returns a big number and the burn function uses this this function so actually instead of burning tokens

it's minting tokens the second example is who can steal my tokens let's um Define theft as a privileged caller who isn't the holder can reduce the holder's balance without an approved allowance without permission so we Define constraints the color shouldn't be the holder the balance of the caller at the end is less than the balance of the color at start and the allowance equals zero which means no probation has been given by solving the model we found that there is a function called approve with

capital A which isn't defined in the sc20 spec usually it's approved with the lower a and you can see here in the implementation of this function the owner can set the balance of any holder which means he can reduce his balance which means he can steal his tokens um to summarize there is a known phrase in crypto don't trust verify sometimes it's hard to do that even if you have the source code of the smart contract and sometimes the malicious functionality is hidden and we've seen yesterday several examples of how can we

trick the verification method of eaterscan um and what if you don't have the source code symbolic execution can fill that Gap it runs on the byte code of the smart contract and can prove if there is a some functionality of the program of the smart contract that is unfair that is a scam it's a necessary tool across the board developers Auditors security companies can use it can should use Simple execution at redefine we automated at scale we provide due diligence API for users for

exchanges for wallet providers recently we announced the integration with noses safe and every of their users can benefit from it if you want to know more please reach out thank you very much thank you so much this is great