Infer Static Analyzer

Last updated

Infer, [1] sometimes referred to as "Facebook Infer", is a static code analysis tool developed by an engineering team at Facebook along with open-source contributors. It provides support for Java, C, C++, and Objective-C, and is deployed at Facebook in the analysis of its Android and iOS apps (including those for WhatsApp, Instagram, Messenger and the main Facebook app). [2]

Contents

History

Infer has its roots in academic research on Separation Logic, a theory for the formal verification of software. Work on automatic program verification based on Separation Logic led to a succession of academic tools, including Smallfoot and SpaceInvader. Building on the academic work, Cristiano Calcagno, Dino Distefano and Peter O'Hearn, three researchers at University College London and Queen Mary University of London, co-founded the verification startup Monoidics in 2009, and Monoidics developed the first version of Infer. [3] [4] [2] Monoidics was acquired by Facebook in 2013, [5] and in 2015 the code of Infer was open-sourced. [2] [6]

As of 2013 when Infer was open-sourced it was claimed that hundreds of bugs per month identified by Infer were fixed by Facebook's developers before reaching production. [5] By 2015 this had increased to over 1000 bugs per month. [7]

Spotify, Uber, Mozilla, Sky, and Marks and Spencer are among the reported users of Infer. [1]

Technology

Infer performs checks for null pointer exceptions, resource leaks, annotation reachability, missing lock guards, and concurrency race conditions in Android and Java code. It checks for null pointer problems, memory leaks, coding conventions and unavailable API's in C, C++ and Objective C. [1]

Infer uses a technique called bi-abduction [8] to perform a compositional program analysis that interprets program procedures independently of their callers. It is claimed that this enables Infer to scale to large codebases and to run quickly on code-changes in an incremental fashion, while still performing an inter-procedural analysis that reasons across procedure boundaries. [9]

Infer is wired up to the code review system at Facebook. Its deployment model is to comment automatically on code modifications as they are submitted for review, where it reports potential regressions. It does this by incrementally analyzing code changes via a job on Facebook's continuous integration system which runs in its data centers. [9]

Infer also has a domain specific language for abstract syntax tree linting, based on ideas from Model Checking for Computation Tree Logic. [10] [11]

Infer is mostly written in the OCaml programming language. [12]

Awards

Dino Distefano  [ it ] received the Royal Academy of Engineering silver medal in 2014 in recognition of the acquisition of Monoidics. [13]

Four Infer team members, Josh Berdine, Cristiano Calcagno, Dino Distafano and Peter O'Hearn, received the 2016 Computer Aided Verification Award, an award they shared with John C. Reynolds, Samin Ishtiaq and Hongseok Yang. [7] [14]

Peter O'Hearn was elected Fellow of the Royal Academy of Engineering in 2016, for his work on Separation Logic and Infer. [15]

Related Research Articles

In artificial intelligence, the frame problem describes an issue with using first-order logic (FOL) to express facts about a robot in the world. Representing the state of a robot with traditional FOL requires the use of many axioms that simply imply that things in the environment do not change arbitrarily. For example, Hayes describes a "block world" with rules about stacking blocks together. In a FOL system, additional axioms are required to make inferences about the environment. The frame problem is the problem of finding adequate collections of axioms for a viable description of a robot environment.

<span class="mw-page-title-main">Programming language</span> Language for communicating instructions to a machine

A programming language is a system of notation for writing computer programs. Most programming languages are text-based formal languages, but they may also be graphical. They are a kind of computer language.

In computer science, static program analysis is the analysis of computer programs performed without executing them, in contrast with dynamic program analysis, which is performed on programs during their execution.

OCaml is a general-purpose, high-level multi-paradigm programming language which extends the Caml dialect of ML with object-oriented features. OCaml was created in 1996 by Xavier Leroy, Jérôme Vouillon, Damien Doligez, Didier Rémy, Ascánder Suárez, and others.

<span class="mw-page-title-main">Abductive reasoning</span> Form of logical inference which seeks the simplest and most likely explanation

Abductive reasoning is a form of logical inference that seeks the simplest and most likely conclusion from a set of observations. It was formulated and advanced by American philosopher Charles Sanders Peirce beginning in the last third of the 19th century.

In computer science, program analysis is the process of automatically analyzing the behavior of computer programs regarding a property such as correctness, robustness, safety and liveness. Program analysis focuses on two major areas: program optimization and program correctness. The first focuses on improving the program’s performance while reducing the resource usage while the latter focuses on ensuring that the program does what it is supposed to do.

In computer programming, a type system is a logical system comprising a set of rules that assigns a property called a type to every "term". Usually the terms are various constructs of a computer program, such as variables, expressions, functions, or modules. A type system dictates the operations that can be performed on a term. For variables, the type system determines the allowed values of that term. Type systems formalize and enforce the otherwise implicit categories the programmer uses for algebraic data types, data structures, or other components.

In the context of hardware and software systems, formal verification is the act of proving or disproving the correctness of intended algorithms underlying a system with respect to a certain formal specification or property, using formal methods of mathematics.

<span class="mw-page-title-main">Model checking</span> Computer science field

In computer science, model checking or property checking is a method for checking whether a finite-state model of a system meets a given specification. This is typically associated with hardware or software systems, where the specification contains liveness requirements as well as safety requirements.

Software verification is a discipline of software engineering whose goal is to assure that software fully satisfies all the expected requirements.

Bunched logic is a variety of substructural logic proposed by Peter O'Hearn and David Pym. Bunched logic provides primitives for reasoning about resource composition, which aid in the compositional analysis of computer and other systems. It has category-theoretic and truth-functional semantics, which can be understood in terms of an abstract concept of resource, and a proof theory in which the contexts Γ in an entailment judgement Γ ⊢ A are tree-like structures (bunches) rather than lists or (multi)sets as in most proof calculi. Bunched logic has an associated type theory, and its first application was in providing a way to control the aliasing and other forms of interference in imperative programs. The logic has seen further applications in program verification, where it is the basis of the assertion language of separation logic, and in systems modelling, where it provides a way to decompose the resources used by components of a system.

In computer science, separation logic is an extension of Hoare logic, a way of reasoning about programs. It was developed by John C. Reynolds, Peter O'Hearn, Samin Ishtiaq and Hongseok Yang, drawing upon early work by Rod Burstall. The assertion language of separation logic is a special case of the logic of bunched implications (BI). A CACM review article by O'Hearn charts developments in the subject to early 2019.

Dynamic program analysis is analysis of computer software that involves executing the program in question. Dynamic program analysis includes familiar techniques from software engineering such as unit testing, debugging, and measuring code coverage, but also includes lesser-known techniques like program slicing and invariant inference. Dynamic program analysis is widely applied in security in the form of runtime memory error detection, fuzzing, dynamic symbolic execution, and taint tracking.

In program analysis, shape analysis is a static code analysis technique that discovers and verifies properties of linked, dynamically allocated data structures in computer programs. It is typically used at compile time to find software bugs or to verify high-level correctness properties of programs. In Java programs, it can be used to ensure that a sort method correctly sorts a list. For C programs, it might look for places where a block of memory is not properly freed.

<span class="mw-page-title-main">Peter O'Hearn</span> Research scientist (born 1963)

Peter William O'Hearn, formerly a research scientist at Meta, is a Distinguished Engineer at Lacework and a Professor of Computer science at University College London (UCL). He has made significant contributions to formal methods for program correctness. In recent years these advances have been employed in developing industrial software tools that conduct automated analysis of large industrial codebases.

CodePeer is a static analysis tool, which identifies constructs that are likely to lead to run-time errors such as buffer overflows, and it flags legal but suspect code, typical of logic errors in Ada programs. All Ada run-time checks are exhaustively verified by CodePeer, using a variant of abstract interpretation. In October 2014, CodePeer was qualified for use in safety-critical contexts as a sound tool for identifying possible run-time errors. CodePeer also produces detailed as-built documentation of each subprogram, including pre- and post-conditions, to help with code review and to ease locating potential bugs and vulnerabilities early.

Dawson R. Engler is an American computer scientist and an associate professor of computer science and electrical engineering at Stanford University.

This is a list of the individual topics in Electronics, Mathematics, and Integrated Circuits that together make up the Computer Engineering field. The organization is by topic to create an effective Study Guide for this field. The contents match the full body of topics and detail information expected of a person identifying themselves as a Computer Engineering expert as laid out by the National Council of Examiners for Engineering and Surveying. It is a comprehensive list and superset of the computer engineering topics generally dealt with at any one time.

References

  1. 1 2 3 "Infer static analyzer". Website.
  2. 1 2 3 Calcagno, Cristiano; Distefano, Dino; O'Hearn, Peter. "Open Sourcing Facebook Infer: Identify Bugs Before You Ship".
  3. ↑ Calcagno, Cristiano; Distefano, Dino; O?Hearn, Peter W.; Yang, Hongseok (1 December 2011). "Compositional Shape Analysis by Means of Bi-Abduction". Journal of the ACM. 58 (6): 1–66. CiteSeerX   10.1.1.420.2150 . doi:10.1145/2049697.2049700.
  4. ↑ Calcagno, Cristiano; Distefano, Dino (18 April 2011). Infer: An Automatic Program Verifier for Memory Safety of C Programs. NASA Formal Methods. Lecture Notes in Computer Science. Vol. 6617. Springer, Berlin, Heidelberg. pp. 459–465. CiteSeerX   10.1.1.421.9629 . doi:10.1007/978-3-642-20398-5_33. ISBN   978-3-642-20397-8.
  5. 1 2 Constine, Josh. "Facebook Acquires Assets Of UK Mobile Bug-Checking Software Developer Monoidics | TechCrunch". Techcrunch.
  6. ↑ Finley, Klint. "Facebook's AI Tool for Squashing Bugs Is Now Open to All | WIRED". www.wired.com.
  7. 1 2 O'Sullivan, Bryan. "Four Facebook Employees Win the Prestigious CAV Award". Facebook Research.
  8. ↑ Separation logic and bi-abduction, page, Infer project site.
  9. 1 2 Calcagno, Cristiano; Distefano, Dino; Dubreil, Jeremy; Gabi, Dominik; Hooimeijer, Pieter; Luca, Martino; O’Hearn, Peter; Papakonstantinou, Irene; Purbrick, Jim; Rodriguez, Dulma (27 April 2015). Moving Fast with Software Verification. NASA Formal Methods. Lecture Notes in Computer Science. Vol. 9058. Springer, Cham. pp. 3–11. doi:10.1007/978-3-319-17524-9_1. ISBN   978-3-319-17523-2.
  10. ↑ Churchill, Dulma; Distefano, Dino; Luca, Martino; Rhee, Ryan; Villard, Jules. "AL: A new declarative language for detecting bugs with Infer". Facebook Code Blog Post.
  11. ↑ Sergio, de Simone. "Facebook's New AL Language Aims to Simplify Static Program Analysis". InfoQ.
  12. ↑ "Infer Github Page".
  13. ↑ "Silver Medals for UK's brightest up-and-coming tech entrepreneurs". Royal Academy of Engineering. Archived from the original on 2014-10-26. Retrieved 2017-07-05.
  14. ↑ committee, CAV Award. "2016 Computer-Aided Verification Award". PRLog.
  15. ↑ "RAEng New Fellows 2016, Peter O'Hearn". Royal Academy of Engineering.
This page is based on this Wikipedia article
Text is available under the CC BY-SA 4.0 license; additional terms may apply.
Images, videos and audio are available under their respective licenses.