We’re hiring for our Research + Engineering team! 

By Aaron Yoo, University of California, Los Angeles

As an intern at Trail of Bits, I worked on Solar, a proof-of-concept static analysis framework. Solar is unique because it enables context-free interactive analysis of Solidity smart contracts. A user can direct Solar to explore program paths (e.g., to expand function calls or follow if statements) and assign constraints or values to variables, all without reference to a concrete execution. As a complement to Solar, I created an integrated development environment (IDE)-like tool that illustrates the types of interactivity and analysis that Solar can provide.

The Solar UI has two main panels, “source” and “IR” (intermediate representation). The source panel displays the source code of the functions being analyzed and the IR panel translates those functions into an enhanced variant of SlithIR, our open-source IR. The green highlights show the lines of the function that are being analyzed. The two panes display similar information intended for different uses: The source pane serves as a map, aiding in navigation and providing context. The IR pane enables interactivity as well as visualization of the information deduced by Solar.

Analyses built on top of Solar are called “strategies.” Strategies are modular, and each defines a different mode of operation for Solar. Three strategies are shown in the above screenshot: concrete, symbolic, and constraint. Although each analysis has its own workflow, Solar needs all three to support the simplify, downcall, and upcall primitives, which are explained below.

Solar primitives

Simplify

The simplify primitive instructs the framework to make as many inferences as possible based on the current information. Solar can receive new information either through user input or by deriving it as an axiom from the program. In the screencast below, Solar axiomatically deduces the value of the constant, 2. If the user tells Solar to assume that the value of x is 5 and then clicks the “simplify” button, Solar will deduce the return value.

Downcall

The downcall primitive instructs the framework to inline a function call. Function calls are inlined so that the user can see the entire path in one pane. In a traditional IDE, the user would have to navigate to the function in question. In our framework, the downcalled function is inlined directly into the IR pane, and its source is brought into the source pane.

Upcall

The upcall primitive inlines the current context into a calling function. In other words, upcalling implies traversal up the call stack and is generally the opposite of downcalling. By upcalling, Solar can traverse program paths up through function calls, as demonstrated below. (Pay special attention to the green-highlighted lines.)

Together, these three primitives give Solar its defining properties: context insensitivity and interactivity. Solar is context-free (context-insensitive) because the user can start analysis from any function. It is interactive because the exact program path is determined by the upcalls and downcalls—which are chosen by the user.

Demonstration for reasoning about integer overflow

Solar can help a user reason about nontrivial program properties such as integer overflow. Consider the following program:

contract Overflow {
    function z(uint32 x, uint32 y) public returns (uint32) {
        uint32 ret = 0;
        if (x < 1000 && y < 1000) {
            will_it_overflow(x, y);
        }
        return ret;
    }

    function will_it_overflow(uint32 x, uint32 y) public returns (uint32) {
        return x * y;
    }
}

Here, we want to find out whether will_it_overflow will ever cause an integer overflow. Integer overflow occurs when the mathematical result of an arithmetic operation cannot fit into the physical space allocated for its storage.

Looking at the will_it_overflow function, it’s clear that integer overflow may be possible, as two 32-bit numbers are multiplied and placed into a 32-bit result. However, based on the call sites of will_it_overflow, if z calls will_it_overflow, there can never be an integer overflow; this is because z verifies that arguments to will_it_overflow are small. Let’s see how Solar would reach this conclusion.

Performing this analysis with Solar requires use of the constraint strategy, which works by attempting to find a single valid execution of the program. The user can constrain the execution with arbitrary polynomial constraints. To start the analysis, we select the will_it_overflow function from the left pane to indicate it as the desired starting point. Here is the initial analysis view:

Solar provides one possible execution that evaluates all values to zero. The next step is constraining the values of x and y. We can provide the following constraints (in terms of IR variables, not source variables) to the constraint strategy:

1.   x_1 < (2 ** 32)
2.   y_1 < (2 ** 32)
3.   x_1 * y_1 >= (2 ** 32)

The first two constraints bind x_1 and y_1 to 32-bit integers. The third causes the solver to try to find an execution in which x_1 * y_1 overflows. It is common practice to prove properties using an SAT/SMT solver by showing that the negation of the property is unsatisfiable. With that in mind, we are going to use Solar to show that there are no executions in which x_1 * y_1 overflows, thereby implying that will_it_overflow does not overflow. After simplifying the use of these constraints, we get the following:

Again, Solar provides a single possible execution based on the constraints. Upcalling once puts us at line 5:

Because the green-highlighted lines do not form a logical contradiction, Solar can still return a valid program execution. However, upcalling again returns a different result:

The question marks on the right indicate that the solver cannot find any possible execution given the program path. This is because line 4 contradicts the inequality we wrote earlier: x_1 * y_1 >= (2 ** 32). The above steps constitute informal proof that overflow is not possible if will_it_overflow is called from z.

Conclusion

I am proud of what Solar became. Although it is a prototype, Solar represents a novel type of analysis platform that prioritizes interactivity. Given the potential applications for code auditing and IDE-style semantic checking, I am excited to see what the future holds for Solar and its core ideas. I would like to give a big thank-you to my mentor, Peter Goodman, for making this internship fun and fulfilling. Peter accomplished perhaps the most challenging task for a mentor: striking the delicate balance between providing me guidance and freedom of thought. I would also like to extend thanks to Trail of Bits for hosting the internship. I look forward to seeing the exciting projects that future interns create!