In an effort to improve the overall security and stability of applications, Facebook has released Infer, a tool used to identify programming errors, under a BSD open-source license.
Infer is a static analyzer, software for finding bugs in other software without actually running the program in question. There are dozens of such tools available to scan code in a variety of programming languages; Infer, written in OCaml, can analyze Java (Android or otherwise), Objective-C, and C code.
For organizations focused on software-based products or services such as Facebook, Pinterest, and practically every other major Internet-oriented company, the ability to ship code quickly has become a competitive requirement. In a paper about its deployment practices, Facebook said it "operates in perpetual development mode, in which engineers continuously develop new features and make them available to users."
[ Need a small-scale database for your mobile apps? Read Filemaker 14: A Database For DIY Apps. ]
Facebook software engineers Cristiano Calcagno, Dino Distefano, and Peter O'Hearn explained in a blog post: "Each month, hundreds of potential bugs identified by Facebook Infer are fixed by our developers before they are committed to our codebases and deployed to people's phones. This saves our developers many hours finding and fixing bugs, and results in better products for people."
Infer was developed at a UK startup called Monoidics that Facebook acquired in 2013. Calcagno, Distefano, and O'Hearn co-founded the company.
Facebook has used Infer to improve the Facebook app for Android and iOS, Facebook Messenger, and Instagram by detecting null pointer access, resource leaks, and memory leaks -- errors that can lead to application crashes and can make programs vulnerable to exploits.
Using both static analysis and automated testing, Facebook is able to ship code as soon as it's ready, without waiting for the results of manual testing.
According to Calcagno, Distefano, and O'Hearn, the fix rate for issues identified by Infer in the past few months is about 80%, which they said is high for an automated tool. They said that Infer uses separation logic and bi-abduction to make inferences about how a large program will execute. These mathematical techniques allow Infer to consider only portions of an application, rather than the entirety of its code.
For Facebook, open-sourcing Infer represents a gesture of goodwill toward the developer community, a constituency that provides value to its platform, and advances the eventual goal of automated software verification. Doing so should also lead to improvements in Infer through external contributions.
In general, anything that improves code quality in an application reduces the potential for application crashes, lost data, and security vulnerabilities. And that benefits both the users and the developers of that application.
Commercial code analysis applications such as Coverity and Klockwork are widely used in many enterprises. However, these tools appear to be ill-suited for analyzing applications at the scale required by large Internet technology companies. In a paper about Google's internally developed static analysis tool Tricorder, Google software engineers Caitlin Sadowski, Jeffrey van Gogh, Ciera Jaspan, Emma Söderberg, and Collin Winter stated: "All of these tools have largely fallen out of use due to problems with workflow integration, scaling, and false positives."