Professor of Software Verification
Our daily lives are completely influenced by computer systems, so it’s important they run correctly, and any errors are resolved quickly.
Errors in computer systems, commonly known as software bugs, often stem from memory violations within the computer software, and can cause issues including crashes or coding errors.
Traditionally developers would test computer systems by running through the software to check for any errors. To save time and resources, program verifiers were developed – automatic tools that scan programs to spot bugs without running them. However, previous past program verifiers have only been tested in programs with a small amount of code. Most systems are much larger, consisting of millions of lines of code, and they need a reliable program verifier.
By working with colleagues from Queen Mary and Imperial University, Professor Dino Distefano used his research on separation logic and bi-abduction to create Infer, an automatic program analyser now used across the world by a number of different companies to help find and solve software bugs.
Infer utilises logic to reason about the reliability of a computer system. However, reasoning at such a large scale on programs with millions of lines of code requires additional work, so the software uses a type of algorithm that provides partial decision procedures. This means it approximates some of the reasoning a human may do when looking at a program. To cope with the scale and velocity requires mathematical techniques – separation logic and bi-abduction.
Separation logic is the first effective theory for reasoning about computer memory, particularly in scaling verification techniques to real-world code. For its development, research on substructural logic from Professor David Pym and Professor Peter O’Hearn at Queen Mary together with work between researchers from Queen Mary and Carnegie Mellon University on heap structure (a type of data structure) developed the theory of separation logic.
Based on these theories, Professor Dino Distefano from Queen Mary produced the Space Invader tool, the first prototype program analyser based on separation logic. To develop Space Invader into a working tool suitable for real-world industrial code, several steps were necessary.
First, working with Professor Calcagno from Imperial College, and researchers from Microsoft, Professor Distefano developed a technique where an analyser can tune the precision of its analysis to different data structures of the analysed program.
Professor Distefano then worked closely with researchers from Microsoft to look at pointers – variables whose value is a location in the computer’s memory. Pointers are one of the main sources of error in memory manipulation in Linux and Microsoft device drivers. After this development, Professor Distefano and the team at Microsoft introduced a fully automated verification approach for object-oriented languages using separation logic.
Finally, Professor Distefano also proposed the idea of bi-abductive inference, which is a form of logical inference that automates the key ideas about local reasoning. This was a breakthrough that allows partial properties of entire open-source projects which contained huge amounts of code to be shown.
By utilising separation logic and bi-abductive inference, Infer is able to find complex problems in modifications to an application built from millions of lines of code in minutes, checking thousands of possibilities in the same frame of time.
Infer was marketed by Monoidics, a Queen Mary spin out company co-founded by Professor Distefano in 2009. In July 2013, Monoidics was acquired by Facebook to improve the quality and the security of their code base.
Since the acquisition, the development of Infer has been carried out at Facebook, where Infer is now an established technology for software quality. Facebook is used by billions of people, and as a result their source code is constantly evolving and updated on a frequent based, sometimes by many different developers at the same time. Due to the speed and size of the operation, Infer is run across all source code to check for any bugs.
In a regular day, it’s not unusual for more than a thousand modifications for mobile code to be submitted for review, and Infer is used to check every change made. Each month, thousands of potential bugs are identified by Infer and fixed by engineers, saving hours of work finding and fixing bugs, which results in a better product for many people. In the second half of 2017 alone, more than 25,000 bugs reported by Infer were fixed by Facebook developers.
Bryan O’Sullivan, director of Developer Efficiency at Facebook, said: “Today within Facebook, the verification technology originally designed by Professor Dino Distefano and colleagues contributes to the quality of the products we serve to over 2 billion people every day. Currently Infer analyses every applicable code change within Facebook and its family of apps (Messenger, WhatsApp, Instagram, Oculus). Every month, thousands of issues are fixed before these apps are shipped to users. Thus, Infer has saved Facebook engineers innumerable hours that they would have had to spend debugging the problems it detected, had those problems reached production.”
In 2015, Infer was open sourced, and since then has been used by many companies and developers around the world, including Amazon Web Services, Uber, Spotify, Mozilla, Sky and Marks and Spencer.
Infer has been used by Spotify for their user generated content apps, and the continuous development of their software as it is continuously released to users.
Deniz Türkoglu, Software Engineer at Spotify in 2016 said, “At Spotify we are continuously working on making our codebase better, and in the Android infrastructure team we use a lot of tools: static analysers, linters, thread/address sanitizers, etc. In our quest to make our code even better, we started using Infer. Infer found several legitimate issues that other tools had missed. Infer is a great add- on to a company’s toolbox. It’s not intrusive — you can simply add it to your flow and it will tell you where you forgot to close that cursor or leaked that context.”
Infer is also used by Amazon and Uber for their online marketplaces. Manu Sridharan, software engineer at Uber in 2016 said, "In 2016, Uber deployed the Facebook Infer tool for static detection of potential NullPointerExceptions (NPEs). Alongside our Runtime Annotation Validation Engine (RAVE) validation, the tool reduced the number of NPEs observed in our apps in production by an order of magnitude."
With a 130-year history, our School offers a vibrant, multi-disciplinary learning and research environment. Our enthusiasm for research defines our programmes, keeping our teaching exciting and relevant.