Open-sourcing Facebook Infer: Identify bugs before you ship | Engineering Blog | Facebook Code
Novel techniques: Separation logic and bi-abduction
Facebook Infer uses logic to do reasoning about a program's execution, but reasoning at this scale — for large applications built from millions of lines of source code — is hard. Theoretically, the number of possibilities that need to be checked is more than the number of estimated atoms in the observable universe. Furthermore, at Facebook our code is not a fixed artifact but an evolving system, updated frequently and concurrently by many developers. It is not unusual to see more than a thousand modifications to our mobile code submitted for review in a given day. The requirements on the program analyzer then become even more challenging because we expect a tool to report quickly on these code modifications — in the region of 10 minutes — to fit in with developers' workflow. Coping with this scale and velocity requires advanced mathematical techniques. Facebook Infer uses two such techniques: 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. That would be a daunting task on modern processors with their large addressable virtual memories.
Bi-abduction is a logical inference technique that allows Facebook Infer to discover properties about the behavior of independent parts of the application code. By storing these properties between runs, Facebook Infer needs to analyze only the parts of the software that have changed, reusing the results of its previous analysis where it can.
By combining these approaches, our analyzer is able to find complex problems in modifications to an application built from millions of lines of code, in minutes.
History: From theoretical computer science to verification for a billion-plus people
Automatic verification of software has been a long-held goal in the computer science community. Facebook Infer builds on fundamental work in the area, including theories of Hoare logic and abstract interpretation. Before joining Facebook, we participated in the development of another fundamental work, "separation logic," as a response to problems in scaling verification techniques to real-world code.
Separation logic was a breakthrough for highly theoretical computer science — a new kind of mathematical logic used to describe mutations of computer memory (analogous to how Boolean logic describes circuits). We worked on applying and automating the theory, creating a series of research prototype tools (Smallfoot, Space Invader, Abductor) and underpinning inference techniques, culminating in the discovery of bi-abduction as a way to analyze programs modularly. (We retain university affiliations: Calcagno with Imperial College London, Distefano with Queen Mary University of London, and O'Hearn with University College London.)
Based on the success of these research advances, we formed a startup company, Monoidics, in 2009. Monoidics joined Facebook in 2013, and since then we have adopted the continuous development and deployment style practiced at Facebook and improved our analyzer based on an iterative feedback loop between our analyzer's development team and Facebook's mobile software engineers. We have demonstrated that verification technology can indeed thrive when applied to codebases at Facebook's scale and pace of change.
The future
Program verification is an area with an active research community and promising technology. At Facebook, we have a saying that this journey is 1 percent finished. In program verification, certainly, a tremendous amount remains to be done. But, with continued progress, we believe there is also much more value that can be unlocked for programmers. We look forward to a future in which, with your help, program verification technology can prove more and more useful in helping programmers develop reliable code, fast.
To find out more about Facebook Infer, download it and try it out, or check out fbinfer.com for more details.
Acknowledgements: The Infer engineering team @FB includes Sam Blackshear, Jeremy Dubreil, Andrzej Kotulski, Martino Luca, Irene Papakonstantinou, Dulma Rodriguez, and Jules Villard, in addition to Calcagno, Distefano, and O'Hearn. We thank our FB colleagues Mathieu Baudet, Dominik Gabi, and Pieter Hooimeijer for their help, and Bryan O'Sullivan, David Mortenson, and Jim Purbrick for their support. Outside of Facebook, we particularly acknowledge the scientific contributions of David Pym, John Reynolds, Hongseok Yang, and Josh Berdine.
More to Read
Read full article from Open-sourcing Facebook Infer: Identify bugs before you ship | Engineering Blog | Facebook Code
No comments:
Post a Comment