Shulou(Shulou.com)06/01 Report--

What is the working principle of Mythril, many novices are not very clear about this, in order to help you solve this problem, the following editor will explain for you in detail, people with this need can come to learn, I hope you can gain something.

Mythril is an intelligent contract security tool based on symbol execution technology. Its preset detection module can find some security problems in the contract, such as integer overflow and reentrant vulnerabilities. The purpose of this paper is to learn to understand the symbol execution mechanism of Mythril in order to develop our own Solidity security analysis module.

Learn DApp in your familiar language: Java | Php | Python | .net / C# | Golang | Node.JS | Flutter / Dart

One of the design goals of Mythril is to make security analysis tools easier to use. In other words, you don't have to be a PhD in computer science to benefit from symbolic analysis.

1. Overview of symbol execution

In order to illustrate how Mythril works, we need to first understand the core technology used by Mythril-symbolic execution (Symbolic Execution). If you already know more about the general idea of symbol execution, then this article will help you sort out the relevant concepts.

I think the easiest way to explain symbolic execution is to actually execute it and draw a graph to show what happens during execution. To do this, we will use the following solidity function as the goal of our analysis, and let's see if we can use symbolic analysis to get a function with a result of 10.

2. Specific implementation: Concrete Execution

Before we start the symbol execution, let's take a look at the results of the specific execution. We can execute the function execute (uint256) with several different inputs. For example, for input 4, the following execution process occurs:

Initial state (function entry):-currently executing: line 1-input = 4 step1:-currently executing: line 2-input = 4-result = uninitialized step2:-currently executing: line 3-input = 4-result = 0 step3:-currently executing: line 6:-input = 4-result = 0

The graphical representation of the above process is as follows:

We can try different inputs until we find an input that allows the function to return 10, which is called a Fuzzing.

3. Symbol execution: Symbolic Execution

Finally, we need to symbolize the execution of the program. This means that instead of bringing specific input (for example, 4) into the program execution, we use a symbol to refer to the specific input. Calling the symbol xPowerX can be any valid uint256 value. Now let's execute the program again.

The implementation of the first two steps is simple and straightforward and easy to understand:

Now let's get to the interesting part. On line 3, the input is compared to 10, but the input is x, which can be any specific value, so x > 10 and x

10, and the other corresponds to x 10. It is easy to see that the first constraint must be satisfied, and it is also easy to determine that x > 10 can be satisfied, for example, for input 11. I just manually found a value to satisfy the above constraints. In Mythril, we actually use a SMT (Z3) solver to find out whether these constraints can be satisfied, and Z3 can also give a concrete example that can satisfy the constraints, which allows us to build an actual input to let the function return 10.

As the conclusion of function execute analysis, we can say:

There is a possibility that the output is 10

You can use input 11 to get output 10

Is it helpful for you to read the above content? If you want to know more about the relevant knowledge or read more related articles, please follow the industry information channel, thank you for your support.

Welcome to subscribe "Shulou Technology Information " to get latest news, interesting things and hot topics in the IT industry, and controls the hottest and latest Internet news, technology news and IT industry trends.