Frequent security problems How can program analysis catch security leaks in advance?

Rice's theorem tells us that every non-trivial property of a program is undecidable, so how does static analysis bypass this question to answer "Is this program a security hole"?

If you are interested in blockchain technology, you may have heard of many incidents of large amounts of funds being stolen by attackers exploiting vulnerabilities in program code. For example, in the infamous DAO attack in 2016, attackers used a vulnerability called "reentrancy" to over-withdraw funds they could have withdrawn. Another more recent incident was the flash loan attack, which took place on April 17, 2022, resulting in a loss of $182 million in funds. While all attacks stem from security vulnerabilities in the underlying source code, the good news is that program analysis techniques are now available that can detect such vulnerabilities. In the next few blog posts, we'll explain what program analysis is and how it can help catch security vulnerabilities before deployment.

Introduction to Program Analysis

Program Analysis refers to a class of techniques used to detect security vulnerabilities in programs. There are two main forms of program analysis, dynamic and static. The goal of dynamic program analysis is to detect problems by executing the program, while static program analysis analyzes the source code without running the program itself. However, among these techniques, only static analysis can ensure that there are no vulnerabilities in the program. On the contrary, unlike static analysis, dynamic analysis can prove the existence of the problem, it cannot prove that the vulnerability does not exist.

At first glance, static analysis may sound cryptic: on the face of it, static analysis seems to violate a fundamental principle summarized in Rice's theorem, which states that every Nontrivial properties are undecidable. Here, semantic properties are properties about the behavior of programs (as distinct from syntactic properties), while non-trivial properties are properties that only some programs have and others don't. More relevant to the topic at hand, the existence of a security breach is a prime example of a non-trivial nature. So, with regard to the question, "Is this program vulnerable to security?" Rice's theorem tells us that no algorithm can finalize and accurately answer the question.

So, where does the feasibility of static analysis come from? The answer lies in the following observation: yes, no algorithm can give an exact yes or no, but there can be an algorithm that will always answer "yes" when the program has a security hole, and sometimes the algorithm may will also answer "yes". In other words, we can bypass Rice's theorem and undecidability as long as we're willing to tolerate some false positives.

Principles of Static Analysis

Let's take a high-level view of how static analysis works. The basic principle of static analysis is to "over-approximate" the set of states the program is in. We think of program state as a mapping from variables to values. In general, there is no algorithm that can identify the exact set of program states that might be caused by the execution of a program. But the set can be approximated, as shown in the following figure:

Here, the blue irregular shapes correspond to the actual set of states that can occur when executing some program, and the red areas correspond to "bad states" that indicate errors or security breaches. Due to undecidability, no algorithm can ever tell exactly what the blue area is, but we can design an algorithm to over-approximate this blue area in a systematic way, as shown above for the regular green area. As long as the intersection of green and red is empty, we have evidence that the program is not doing bad things. However, if our over-approximation is not accurate enough, it may cause the red areas to overlap, even though the intersection of the blue and red areas is still empty, as shown in the following image:

This situation results in so-called "false positives", false errors reported because the analysis does not correspond to the real problem. Generally speaking, the holy grail of static analysis is to construct over-approximation, i.e. (1) over-approximation is accurate enough so that we do not get very false positives in practice (2) over-approximation is computationally efficient enough so that the analysis can be extended to what we have Real-world programs of concern.

As a side note, static analysis algorithms can also be designed to approximate program behavior like this:

In this case, the green area (calculated by static analysis) is contained within the blue area (representing the actual state), as opposed to the other way around. This analysis is unreliable and means that real program bugs may be missed: as we can see in the image above, the intersection of green and red is empty, so even if the program is really vulnerable, the analysis will not Report a problem. This can lead to so-called false negatives, where real vulnerabilities are missed by static analysis.

In general, if we want provable security, we want reliable static analyzers that never have false positives, but also need to be accurate enough not to report in practice Too many false positives. The good news, however, is that decades of orthodox research have shown that it is possible to design such a static analyzer. In the next blog post, we'll go into more detail on how static analyzers work!

Summary

Program analysis is an effective technique for catching security vulnerabilities in various programs, including blockchain applications. In addition, the over-approximation of program behavior by reliable static analyzers ensures that there are no vulnerabilities in the entire class.