Facebook’s Infer goes open source
Free tests for everyone! That’s the premise behind Facebook’s decision to open source Infer, their static program analyser with an impressive bugfix rate. On top of sharing their wares, Facebook hope that being in the open will drive further development.
Infer, Facebook’s static analysis tool, has been open sourced in a bid to expand its deployment reach beyond Android and iOS. In a recent blog post, Cristiano Calcagno, Dino Distefano and Peter O’Hearn from the Infer team introduced the newly open tool to the world, which Facebook uses to identify bugs before mobile code is shipped to phones.
As a static analyser, Infer is an automated tool that spots bugs in source code by scanning programs without running them. O’Hearn confirmed via his own Facebook page that they’d been using it internally with some success, and are now going to continue its development in the open. Engineering manager Jim Purbrick lists Infer’s fix rate at 80%.
The tool focuses primarily on C, Java and Objective-C and signals null pointer accesses, as well as resource and memory leaks. Hello world examples on the Infer website show the tool working in plain code. The bug tracking that Infer completes is said to identify hundreds of potential flaws via separation logic and bi-abduction:
Separation logic is a theory that allows Facebook Infer’s analysis to reason about small, independent parts of the application storage, rather than having to consider the entirety of the memory potentially at every step.
Bi-abduction is a logical inference technique that allows Facebook Infer to discover properties about the behaviour of independent parts of the application code.
The decision to go open source stems from the large amount of work ahead that is needed for program verification, with O’Hearn noting that an increased idea-flow between their engineering team and the research community will be beneficial for future development.
By choosing to develop openly, the Infer team freely admit that their project is “1 percent finished”. Infer’s limitations mean that at present, a restricted collection of bug types is reported on, with the project’s initial scope focusing on the most pressing needs for Facebook’s mobile developers. An example of bugs that Infer doesn’t currently track is below:
- Array bounds errors
- Cast exceptions
- Leaking of tainted data
- Concurrency race conditions
For array errors, cast exceptions and leaks, Infer are already working on solutions. There are also some constraints when it comes to language features, with concurrency, reflection and dynamic dispatch all either not recognised or weakly treated.
Infer source code can be found on GitHub.