On September 5, at the POD Conference Security Forum hosted by Odaily and co-organized by 36Kr Group Strategy, Yang Wenyu, a security expert from the Cheetah Blockchain Research Center, delivered a speech entitled Smart Contract Automated Audit Technology.
Yang Wenyu introduced the current status of smart contract development. Most people think that the blockchain is now in a cold winter period, but according to the statistics of the Cheetah Blockchain Research Center, in the past month, the number of new smart contracts was 1317 per day. Among the projects included in the research center, blockchain infrastructure accounts for 9.38%, games and VR 4.44%, commerce and retail 3.6%, and social media and communications 3.4%.
While the number is growing steadily, smart contracts are also facing security issues. From 2017 to June 2018, smart contract vulnerabilities broke out frequently, causing a lot of financial losses, and also made some developers or users of the blockchain and even smart contracts question the security of smart contracts, which also hindered the development of Ethereum after Ethereum. development of.
In addition, when Fomo3D was on the rise, a large number of counterfeit contracts appeared on the second day only. The copycat Fomo3D game developers have changed the logic of active distribution, causing most of the invested funds to flow to copycat contract developers, which also hinders the development of DApps.
In this context, how to effectively guarantee the security of massive smart contracts? Yang Wenyu believes that the best way is to reduce the complexity of manual audits and use smart contracts to automate audits.
Specifically, automated audit methods fall into three main categories:
The first is feature code matching, which is to extract and abstract malicious code, and form a matching module to detect the source code to be detected. The advantages are fast speed and rapid response to new vulnerabilities, but the disadvantages are limited scope of use and high false negative rate.
The second is an automated audit method based on formal verification. It was first provided by Hirai in 2016, and improved after Grishchenko and Hildenbrandt, using F*framework and K framework to convert EVM into a Formal model. Formal is a common formal verification framework in the aerospace field, while K framework is a semantic transformation framework.
The last is the most commonly used method today, based on symbolic execution and symbolic abstraction to automate auditing. When analyzing smart contracts, EVM OPCODE can be formed by compiling the source code, and then input to the automatic analysis engine, converted into CFG, and then analyzed using these two methods. The typical ones are the Oyente and Securify systems, which can reduce the false positive rate and false negative rate, but the analysis methods are cumbersome and time-consuming.
However, Yang Wenyu also pointed out that the current automated audit method is in a very immature stage and mainly faces three major problems: high false alarm rate, low degree of automation, reliance on manual secondary audit, and relatively long audit time.
The following is the full text of Yang Wenyus speech, enjoy:
Thank you, everyone. It is a great honor to participate in this conference today. The topic of my speech today is to analyze the current smart contract automation security detection technology. My speech today may be divided into two parts. First, we will discuss the first part Let’s take a look at the current status of smart contract development on Ethereum. The second part is based on this status quo, and then describes in detail some methods involved in smart contract automation.
First of all, let’s take a look at the current status of smart contract development. According to our platform, we can know that in the past month, the number of smart contracts has been growing steadily at an average growth rate of 1317 per day, which may be consistent with our understanding The blockchain is now in a cold winter period, so the growth rate is relatively stable. Secondly, we use some NLT methods to divide the field of smart contracts. Except for some sensitive areas, smart contracts are now widely used in infrastructure, commercial retail, games, social media and communications. This is the status quo of smart contracts. What is the security status of smart contracts now? Maybe the two guests have already described them in great detail. From 2017 to June 2018, this kind of smart contract vulnerabilities frequently broke out. , each time brings a large amount of financial losses, and also makes some developers or some users of the blockchain and even smart contracts have some high doubts about the security of smart contracts, which also hinders the development of Ethereum.
In addition, we can also see that Fomo3D was mentioned by the guest just now. In addition to the basic smart contract security, security is now receiving great attention. When Fomo3D was on the rise, a large number of smart contracts appeared on the second day. In this kind of game, the developer actually changed the logic of active distribution, so that in the process of playing the honeycomb game, most of the invested funds flowed to the developer of the copycat contract, which also contributed to the development of the DApp. cause hindrance.
Now we are facing a problem of how to effectively ensure the security of massive smart contracts, which is also the issue we will discuss today, and the second part I want to share with you the development of the current smart contract automation audit technology.
Looking back, as of 12:00 noon yesterday, there are a total of 1.93 million smart contracts in Ethereum, and the daily growth rate is growing steadily. Now the audit methods include manual audits and automated audits. Among the massive smart contracts, our best way is to reduce the complexity of manual audits, so that more can be done through automated audits. We divide automated auditing into three parts. First of all, the first type is feature code matching, the second type is sub-duty auditing method based on situational verification, and the last type is automatic auditing based on symbolic execution and symbolic abstraction.
First look at feature code matching. It can be clearly understood from the name that it extracts and abstracts malicious code. We are a semantic match that matches static original code. The advantages of the audit method are obvious, for example, the speed is very fast, because Perform a string match on the source code, and the second can quickly find a new vulnerability. If a new vulnerability occurs in his audit, we can quickly submit some new matching patterns. What are its shortcomings? Let’s take a look again. We understand that the current blockchain should be open and transparent, but the actual situation is not like this. We probably made a statistics. The current code opening rate only accounts for 48.62%. , That is to say, on Ethereum, more than half of the contracts are not open source, only the code is exposed. The guest just said that they also spent a lot of effort to establish the code. This limitation leads to the scope of use of this method Limited, the traditional static audit method, such as App detection, will call some unique functions in a library to audit them. Some functions and features in smart contracts are more variable, so the vulnerability rate is relatively high.
The second method, let’s discuss the popular automated audit based on formal verification. Formal verification audit smart contract security was first provided by Hirai in 2016. Logical interactive prover, through Isabelde Lem-Language->Formal-model, through formal model verification, to judge whether there is a problem in the code logic, the last two of this work further reformed the formal aspect, they gave up Lem-language It is also a relatively inefficient conversion method. They use F*framework and K framework to convert EVM into a Formal model, and Formal may be a framework that often does some formal verification in the aerospace field, while K framework is a Semantic transformation framework, these two representative technical researches, if you want to have a deeper understanding, you can refer to the following papers.
The third point is that I want to focus on communicating with you today, and some of the most commonly used methods are automated audits based on symbolic execution and symbolic abstraction. Let’s take a look at this automated auditing. When we analyze a smart contract, we must first Clearly analyze what the object is. Like we explained the feature matching code just now, we know that most of the smart contract codes on the EVM are not public. We now analyze the object and confirm that it should be EVM OPCODE. After passing some source code, we compile , can form EVM OPCODE, input to the automatic analysis engine. In this automatic auditing framework based on symbolic execution and symbolic abstraction, there are some common features. OPCODE will be converted into a CFG when input into the engine, which is a control flow chart one by one. Through this CFG, you can simply understand this CFG What does it mean? CFG is to package the logic in the contract code into a fast one. When the logic inside is forked, the contract on the left forms a very large and complete CFD, so that programmers can better understand and execute some logic.
After the generation of CFG, there are now two analysis methods. The first type is the verification based on symbolic execution. This type is more representative. Everyone is familiar with Mythril, Oyente, and Maian. A publicly available symbolic abstract analysis method is Securify. Today I will mainly talk about the specific architecture and implementation methods of the two systems Oyente and Securify. First, let’s look at Oyente. We can see the logic of Oyente from the left. In CFG After the application, the first is an explorer, which will verify each process in the code and perform a formal verification. Just like this, we verify whether we have an X, so that X not only satisfies the conditions of C1, C2, and C3. At this time, we can Determine whether the status is no or yes, so as to verify the flow of the entire logic. The second core analysis is actually the most core part of Oyente. It converts the explorer path just output, and only performs some vulnerability verification. Currently, it only provides TOD, Timestamp dependency and Mishandled exceptions, these three Verification. In the end, this system can guarantee the rate of false positives and false negatives. It uses Microsofts open source verifier to encapsulate the overall architecture. In the process we just described, you should also understand that the CFG to explorer verification Sometimes, we need to cycle through him, and each time is a verification, so this analysis method is particularly time-consuming and may not be successful. This is where Oyente currently has a huge problem.
On the basis of this problem, like Securify, they provide another method. They believe that the current contract code is actually particularly easy to decouple. Unlike traditional code, the coupling is particularly high, such as some relatively fixed forms of contract code. We do not need to conduct an inspection of the entire contract logic. We analyze each module of the contract decoupling to improve the degree of automation. The picture on the left shows the entire verification process. The contract bytecode is passed through the domain language Then there is a verification module, especially like the pattern matching mentioned before, which converts some vulnerabilities into a verification language pattern matching framework, and verifies whether the semantics are compatible with this. Finally, a report is also given. Through this automated audit method, the manager who can finally output the wallet can be modified.
A more specific point is how to do semantic analysis. In fact, the analysis of this explorer code is from two dimensions, the first is logic, and the second is data. The logical method defines two kinds of logic. The first is called MayFollow, and the second is called MustFollow, MayFollow means that L2 must have a path following L1, and MustFollow means that every path of L2 must follow L1. These two differences define the entire logic framework.
The second is data. How to define data changes in the contract uses three types. The first MayDepOn is two factors, one is called Y and the other is called T. When T changes, Y may or may not change. The second is Eq, that is, Y is determined by T. The third one is DetBy, Y and T are in one-to-one correspondence, as long as T changes to Y, it will definitely change, here is a more vivid way to imagine, in fact, Maydepon is like our T variable is time, in a period of time , Y may be a value, T changes, Y may not change, the third is a one-to-one relationship, just like we calculate hash, as long as you change T, Y must change, through the two dimensions of logic and data , they conducted some verification, and the final verification module now provides about six or seven smart contract vulnerability verification languages. This language is written in plug-in, and other security developers can continue to enrich the verification language of vulnerabilities. .
In the end, when we evaluate the automatic audit, we need to provide this matter from the degree of automation, the rate of false positives, and the rate of false positives. We now know that the data can be bound, and the detected data still needs to be manually confirmed again. This work is very cumbersome, and the false positive rate can be reduced through this method. These two automated audit methods of symbolic execution and symbolic abstraction.
Finally, to review, there are currently three types of automated audit methods, feature code matching, formal verification, symbolic execution, and symbolic abstraction. Looking back at the entire analysis process, we can clearly know that the current automated audit method is in a very immature stage and mainly faces three major problems. The first is the high rate of false positives, which cannot be fully automated and requires manual participation. . The second is that the degree of automation is relatively low, and it needs to be audited continuously, and the third is that the audit time is relatively long.
The last is to review our entire analysis. First, let’s clarify the development status of smart contracts and test the automated audit methods. There are our technical exchange groups on the left and right. Interested children are welcome to join, and we can have a more in-depth discussion together. This is what I am doing today. Thank you for sharing the content.
