22This is a report of my experience during a 2-month sabbatical I recently completed with the Facebook Infer static analysis team in London. During my sabbatical with my PhD students, we developed Inferbo, a static analyzer to detect C-like buffer-overrun/underrun errors which is now available via the Infer github. Its cost-accuracy balance is set to find some common overrun/underrun issues that I observed in Facebook’s codebase during the course of our work. Inferbo scales to Facebook-size code thanks to Infer’s amazing three-pillar infrastructure: its efficient modular analysis engine, its clean abstraction layer for other static analyses, and its fluent multi-lingual frontend. I found that Infer’s modular analysis infrastructure has opened new opportunities for static analysis to have impact on large, quickly changing codebases.

The experience of developing Inferbo shattered my mindset
Before my 2-month sabbatical visit with the Infer team, I had already been amazed by what I’d learned about Infer’s modular analysis technology. I was therefore eager to understand its details and how it is used inside Facebook. Until my visit, the abduction technology which Infer was based on sounded a bit esoteric to me. But the basic idea is simple. Rather than starting analysis of a program from the main procedure, you can start anywhere. As you analyze, you gather information that is needed for error-free execution to proceed. This information forms a precondition for the procedure. The consequence of this is that you can analyze little program parts without analyzing the entire program. Infer’s infrastructure stitches together the results of the many little program parts to give a picture of the whole. This opens the way the analyzer to keep pace with a large, fast-moving codebase. I came to believe that the static analysis community should take the opportunity in this direction that Infer has started.

I will describe Inferbo (bo for buffer overrun), a static analyzer to detect C-like buffer-overrun/underrun errors, developed on top of the Infer infra.

Status

• Findings? Inferbo detects a number of buffer overrun issues similar to ones I saw in FB, after they were manually injected into open source C source (spell, unhtml, spell++, bc, gzip). I also ran Inferbo on some internal Facebook code and Inferbo generated alarms in the third-party C source(e.g. open-ssl). Inferbo currently looks for buffer overruns on C-style arrays; a next step is to tailor it to the C++ and Objective C used in Facebook’s internal codebases.
• Scalable? Yes, thanks to Infer’s underlying modular analysis platform.
• Impact? Promising yet remains to be seen. We plan to continue working with Facebook engineers to further improve Inferbo and to deploy it inside Facebook’s programming environment.

Design
We designed Inferbo with a focus on common buffer-overrun issues I observed in Facebook code. Inferbo estimates the possible sizes of stack/heap-allocated buffers and the value ranges of the buffer access expressions, and generates an alarm when it concludes that a buffer access can be outside the allocated buffer area.

• Symbolic intervals. Inferbo uses the conventional program analysis technique of intervals for the range of index values and buffer sizes. Normally, interval analysis works with intervals [low,high] consisting of constants. For modular analysis of procedures we made an analysis where the bounds are instead symbolic. The bound expressions are restricted to be from linear arithmetic (+ but no *) with additional min and max operators.
• Heaps and arrays. Inferbo uses a simple alloc-site-based abstraction for heap memories. An abstract location is a tuple of allocation site, size interval, and the current offset interval.
• Summary-based. Inferbo analyzes each procedure going forward starting from a symbolic pre-state (memory image) for its parameters and free variables. As it goes forward it gathers constraints which in the end function as a precondition which dictates in symbolic form the safety conditions for buffer accesses inside the procedure. When Inferbo can resolve the symbolic safe conditions to be violated an alarm rings.

Examples
Let’s look at how Inferbo handles a few simple C examples. For each procedure, we’ll explain the return values and safe buffer access conditions that Inferbo computes.

First, let’s consider a simple example to understand Inferbo’s safety conditions:

void local() {   int *arr = malloc(9*sizeof(int));   int i;   for (i = 0; i < 9; i++) {     arr[i] = 0; // safe     arr[i+1] = 0; // alarm   }

For this procedure, Inferbo computes the safety condition [0, 8] < [9, 9] for the first access and [1, 9] < [9, 9] for the second. Each safety condition is about checking the index values to be within the target buffer area. The [0,8] in the first safety condition is the estimated interval value for the index expression “i” in “arr[i]”, and the [9,9] is the estimated size interval of the target array “arr”. Because all integers in [0,8] are non-negative and smaller than [9,9] Inferbo concludes the accesses are safe. On the other hand, the second access’s index expression “i+1” has an estimated interval [1,9] (= [0,8] shifted right by 1 because of +1). Because an index value 9 in [1,9] can overrun the array of size 9, Inferbo signals an alarm indicating that the second accesses can overrun.

This within-one-procedure reasoning is typical of what one finds in static program analysis.

Inferbo’s scalability comes from the way that Inferbo treats reasoning involving multiple procedures (interprocedural analysis, in the jargon). Inferbo computes a description of what a procedure does, its “summary”, in isolation from its context. The isolation is done by parameterizing the call contexts during the computation of the summary. Inferbo then computes an approximation of the global behavior of the program by stitching the procedure summaries in accordance with each call context.

Let’s see how this works by examining the summaries for a few procedures and then describing how they can be stitched together.

To begin we consider a dereference that involves formal parameters:

 void set_i(int *arr, int index) { arr[index] = 0; }

For this procedure, Inferbo-computed parameteric context is for the parameters “arr” and “i”:

arr |-> (offset: [s$0, s$1], size: [s$2, s$3]), index |-> [s$4, s$5] and the safety condition is [s$0 + s$4, s$1 + s$5] < [s$2, s$3].

The pointer parameter “arr” is an offset from the beginning of a buffer of some size. The offset is an symbolic interval [s$0, s$1] whose lower and upper bounds are respectively symbol s$0 and symbol s$1. The buffer size and parameter “i” are again symbolic intervals. The safety condition for the buffer access “arr[i]” is expressed as its offset “[s$0 + s$4, s$1 + s$5]” (the pointer “arr” [s$0,s$1] shifted-right by “i” [s$4,s$5]) should be non-negative and less than the buffer size [s$2, s$3].

Next, let’s take a look at at malloc wrapper to understand Inferbo’s post-conditions:

 char * malloc_wrapper(int n) { return malloc(n); }

For this procedure, Inferbo computes a procedure summary as

n |-> [s$6, s$7] ret |-> (offset: [0, 0], size: [s$6, s$7]). 

(For brevity, I don’t include the case that malloc fails.). The return value is a pointer whose offset is [0, 0] and size is the parameter “n” that is a symbolic interval [s$0, s$1].

Finally, let’s take a look at our original example, but using malloc_wrapper in place of malloc and set_i in place of direct writes:

 void interprocedural() { int *arr = malloc_wrapper(9*sizeof(int)); int i; for (i = 0; i < 9; i+=1) { set_i(arr, i); // safe set_i(arr, i + 1); // alarm } }

For each call, Inferbo instantiates the procedure’s symbolic summary by the actual call context and rings an alarm if it could conclude its, if any, safety condition false. From the actual parameter 9 in call “malloc_wrapper(9)” the symbolic interval [s$6, s$7] becomes [9,9], hence the array pointer “arr” becomes a pointer of offset [0,0] to a buffer of size [9,9]. For the call “set_i(arr,i)”, the actual parameters “arr” and “i” instantiates the symbolic summary of set_i into:

 arr |-> (offset: [0, 0], size: [9, 9]), index |-> [0, 8] and the safety condition is [0 + 0, 0 + 8] < [9, 9]. 

The safety condition is true hence Inferbo does not ring an alarm.

For the second call “set_i(arr, i+1)”, the newly instantiated summary of set_i is:

arr |-> (offset: [0, 0], size: [9, 9]), index |-> [1, 9] and the safety condition is: [0 + 1, 0 + 9] < [9, 9]. 

The safety condition is false because 9 in [1,9] cannot be smaller than [9,9], hence Inferbo rings an alarm.

So you see that we can analyze the original procedure just as accurately, when the specific dereferencing operations are abstracted by procedures, even though the procedures are analyzed independently. To do this we need an accurate-enough notion of summary, as well as a good means of stitching together summaries.

I hope these three examples have illustrated Inferbo’s modular analysis technique for buffer-overrun errors. Now, the following table shows some numbers from our experiments. We tested Inferbo to see if it detects buffer overruns typical of some I observed while inside Facebook. We manually injected hand-crafted versions of such buffer overruns into some open source applications to see if Inferbo detects them. Inferbo’s total analysis time (from parsing to the end of the analysis including the alarm reporting) is all less than a second.

Both false alarms and misses come from Inferbo’s double-standard for (or a balancing act between) its safety and accuracy. False alarms happen because of the safety. Inferbo over-approximates when in doubt, hence can conclude some spurious overruns. On the other hand, some misses happen because Inferbo post-filters some alarms that it heuristically consider false.

INFER: A great robot suit
Infer is an amazing robot suit for static analysis designers. Thanks to Infer my students, Kihong Heo and Sungkeun Cho, and I were able to quickly lift our Inferbo design to a realistic, scalable analyzer that operates at Facebook scale (millions of lines, changing quickly). Infer’s modular analysis engine is a rocket that shoots us to the mesmerizing modular analysis orbit, its extensible abstract interpretation framework is super-convenient to add a new kind of analysis like Inferbo, and its multi-lingual front end frees us from worrying about targeting varied source languages. An analyzer as realistic and modular as Inferbo in about 5 weeks? I would not have believed it before I knew the power of the Infer infrastructure.

What’s on my mind
I believe the static analysis community should take the opportunity that Infer has enabled. For some properties and for the right deployment models there exist a lot of opportunities for scalable summary-based modular analysis. I personally will ride the Infer robot suit to build such analyses. My team in Seoul will join forces by building a Sparrow robot suit; Sparrow is a scalable global analysis framework by temporal+spatial sparse technology, which I think is complementary to Infer in tuning the soundness and precision level for different deployment models from Facebook’s.

Kwang and the Facebook Infer team, from left to right: Sungkeun Cho, Seoul National University, Josh Berdine, Peter O’Hearn, Andrzej Kotulski, Cristiano Calcagno, Sam Blackshear, Jules Villard, Mehdi Bouaziz, and Dino Distefano, of Facebook, Kihong Heo and Kwangkeun Yi, Seoul National University, and Dulma Churchill, Facebook.

Thank you all
I thank every member of the Infer team. Without their help about Infer, Inferbo would have been impossible. I thank my graduate students Kihong Heo and Sungkeun Cho in Seoul. They quickly figured out Infer and implemented & debugged Inferbo with amazing efficiency.