The Sixth Workshop on Tools for Automatic Program Analysis
Satellite workshop of SAS 2015
8 September 2015
In the last ten years, a wide range of static analysis tools have emerged, some of which are currently in industrial use or are well beyond the advanced prototype level. Many impressive practical results have been obtained, which allow complex properties to be proven or checked in a fully or semi-automatic way, even in the context of complex software developments. In parallel, the techniques to design and implement static analysis tools have improved significantly, and much effort is being put into engineering the tools. This workshop is intended to promote discussions and exchange experience between specialists in all areas of program analysis design and implementation and static analysis tool users.
Previous workshops have been held in Perpignan, France (2010), Venice, Italy (2011), Deauville, France (2012), and Seattle, WA, USA (2013), and Munich, Germany (2014).
The technical program of TAPAS 2015 will consist of invited lectures together with presentations based on submitted abstracts.
We welcome presentations on all aspects of program analysis tools including, but not limited to the following:
- design and implementation of static analysis tools to check, prove or infer properties (including practical techniques used for obtaining precision and performance);
- components and other reusable infrastructure of static analysis tools (front-ends, abstract domains, solvers, analysis algorithms, frameworks, etc.);
- integration of static analyzers (in proof assistants, test generation tools, IDEs, etc.);
- experience reports on the use of static analyzers (both research prototypes and industrial tools);
- challenges for static analysis tools, such as new properties to address or bottlenecks to overcome;
- usability of static analysis tools (including user interfaces and other tools helping to exploit static analysis results); and
- tool demonstrations, and comparisons, by tool authors or experienced users.
Patrick Cousot, New York University
Sound Verification by Abstract Interpretation
Abstract: Automatic program verification tools have to cope with programming language and machine semantics, undecidability, and mathematical induction, and so are all complex and imperfect. The ins and outs of automatic program verification will be discussed in light of the theory and practice of abstract interpretation.
Biography: Patrick Cousot received the Doctor Engineer degree in Computer Science and the Doctor ès Sciences degree in Mathematics from the University Joseph Fourier of Grenoble, France.
Patrick Cousot is Silver Professor of Computer Science at the Courant Institute of Mathematical Sciences, New York University, USA.
Before he was Professor at the the École Normale Supérieure, Paris, France, the École Polytechnique and the University of Metz and a Research Scientist at the French National Center for Scientific Research at the University Joseph Fourier of Grenoble, France.
Patrick Cousot is the inventor, with Radhia Cousot, of Abstract Interpretation.
Patrick Cousot was awarded the Silver Medal of the CNRS (1999), a honorary doctorate from the Fakultät Mathematik und Informatik of the Universität des Saarlandes (2001), the Grand Prix of Computer Science and its Applications of the Fondation Airbus Group attributed by the French Academy of Sciences (2006), a Humboldt Research Award (2008), and, with Radhia Cousot, the ACM-SIPLAN Programming Languages Achievement Award (2013) and the IEEE Harlan D. Mills Joint Award (2014). He is Member of the Academia Europaæ, Informatics section (since 2006).
Pascal Cuoq, TrustInSoft
Verifying the Absence of Undefined Behavior in a Minimal but Realistic Configuration of PolarSSL
Abstract: Software bugs of all nature are unpleasant. Functional bugs require a functional specification before they can be automatically detected, or their absence formally proved. For an under-specified programming language such as C, one implicit expectation is that the program's execution will not run into undefined behavior. This expectation is convenient because it can be formalized with only a few rare points of disagreement with C developers' own view of the C language. At the same time, this implicit expectation is a useful one to verify formally: in the context of C programs taking inputs from an unfriendly outside world, undefined behavior sometimes end up giving the attacker more control over the host computer than the developer intended.
The authors verified the absence of undefined behavior in a minimal but realistic configuration of PolarSSL 1.1.8. Since an SSL/TLS server does not provide Remote Procedure Call-like functionality to outsiders through defined behavior, the only way it can provide this functionality is through undefined behavior. Indeed, as found during the verification, PolarSSL 1.1.7 probably provided remote code execution functionality to outsiders for some compilations and target platforms (CVE-2013-5914).
The authors used analyses available in the Frama-C platform for the verification, with additional proprietary plug-ins for tracking the properties being verified and applying sanity checks to the results. This presentation provides insights into the process and the results of this verification.
Biography: Pascal Cuoq first studied static analysis with Marc Pouzet during his PhD, and became more interested in Abstract Interpretation during his post-doctoral year with Kwangkeun Yi. For ten years he worked in CEA LIST's Software Reliability lab, initially on the software verification tool CAVEAT, and then as one of the initiators of Frama-C. In 2013, together with Benjamin Monate and Fabrice Derepas, Pascal Cuoq founded the company TrustInSoft to transfer Frama-C from the world of safety-critical software, where it has its roots, to the world of software security, where some formal assurances seem much needed.
Don Sannella, Contemplate & University of Edinburgh
ThreadSafe: Static Analysis for Java Concurrency
Abstract: ThreadSafe is a commercial static analysis tool that focuses on detection of Java concurrency defects. By restricting attention to concurrency bugs, ThreadSafe can find bugs that other static analysis tools, both commercial and freely available, miss or are not designed to look for. Its findings are generated from information produced by a class-by-class flow-sensitive, path-sensitive, context-sensitive points-to and lock analysis, with heuristics to tune the analysis to avoid false positives. It has been successfully applied to codebases of more than a million lines.
Biography: Professor in the School of Informatics at Edinburgh University, Don Sannella was educated at Yale, UC Berkeley, and Edinburgh University. He is Editor-in-Chief of the journal Theoretical Computer Science and a Fellow of the Royal Society of Edinburgh. In 2009, after 30 years of academic research on formal specification, verification and refinement, static analysis and security, Don (together with David Aspinall) founded Contemplate, where he is currently CEO, to develop tools for programmers to improve the quality of software products, building on the results of a research project on static analysis for Java. Contemplate's product ThreadSafe is used by companies worldwide to identify and avoid software failures in complex Java applications.
Max Schaefer, Semmle
Analysing Software Engineering Data
Abstract: Semmle offers a static analysis platform centred around two key concepts: database-backed program analysis, and analysis of non-code artifacts. The former means that analyses are implemented as queries written in QL, a high-level, declarative, object-oriented dialect of Datalog, which run on a relational database representing the code base under analysis. The latter means that this database is enriched with all kinds of meta-information associated with the software development process, such as source control information, issue tracking data, or test coverage metrics, which can be analysed in conjunction with the code itself.
We will demonstrate on a few examples how QL empowers static analysis experts and ordinary developers alike to implement both quick syntactic checks and deeper semantic analyses. We will also show how the seamless integration of code and non-code artifacts can be leveraged to improve analysis results, and how it enables us to ask and answer questions that lie outside the realm of classic static analysis.
Wolfgang Ahrendt, Laura Kovacs and Simon Robillard.Loop Analysis Using Theorem Proving and Symbol Elimination
In 2009, the symbol elimination method for loop invariant generation was introduced. Symbol elimination exploits the power of first-order theorem proving, in particular of the Vampire prover, to generate quantified loop invariants, possibly with quantifier alternations, of program loops over arrays. Symbol elimination is fully automatic, that is it does not require the user to provide additional predicates or templates. Symbol elimination relies on so-called extended expressions, which are symbolic representations of the value of a program variable as a function of the loop iteration counter. First-order formulas with extended expressions form a rich language, with which one can express many interesting loop properties, for example by using some lightweight static analysis over program variables. Once these loop properties with extended expressions are collected, the next step of symbol elimination is to use the saturation engine and consequence elimination capabilities of Vampire. This way, logical consequences of the loop properties with extended expressions are derived; however, these consequences contain no extended expressions and are expressed using the language of program expressions. Therefore, these properties describe loop invariants and can be used in the context of Hoare logic–based verification or other verification systems.
In this paper, we describe a new implementation of symbol elimination and loop analysis in Vampire. We also extend symbol elimination by using the pre- and post-conditions of loops. We use these specifications to get more precise invariants and to select invariants relevant to the correctness proof of the loop. Together with the loop specification, the properties generated by symbol elimination capture the information needed to directly verify the partial correctness of the loop. This way, symbol elimination offers an automatic alternative to, for example, the classic Hoare rule–based verification for loops.
Our implementation of symbol elimination and loop analysis in Vampire is not limited to a specific programming language, but instead takes as input a simple guarded command language. As an example of the usability of our work in the context of a real language with more complex semantics, we interfaced our tool with the KeY verification system. KeY formalizes the correctness of annotated Java programs as dynamic logic formulas, and tries to automatically prove these formulas. In the case of programs containing loops, user-provided invariants are usually required in order to apply the dedicated dynamic logic rule. We exploit symbolic execution, already used by KeY to prove properties of programs, to obtain a semantically correct translation of Java code into the language used by our tool. We then use this translation to either produce invariants to be used in the dynamic logic rule or delegate the proof of correctness of that part of the program to Vampire.
We have successfully evaluated our work on a number of examples coming from KeY, thus providing interesting and realistic case studies of using symbol elimination in the static analysis of loops.
Georges Dupéron and Roland Ducournau.k-l-CFA: A Practical Implementation
We have implemented k-l-CFA (control-flow analysis) for a real-world object-oriented programming language. We present how we handle some features of the language which interact with the analysis, and compare the precision of the results obtained via different ways of handling them. These features include generic types, delegates (closures encapsulating a method pointer and its receiver object), as well as covariant arrays.
We have compared the results obtained in our analysis with those produced by an independently developed implementation. This mutual black-box comparison enabled identification of other variation points in the CFA algorithm and additionally, assessment of the quality of both implementations.
Colin Runciman and Simon Thompson.Demur: Checking Functional-program Properties Using Bounded Recursion
The Demur tool translates programs and properties expressed in a large subset of Haskell to decidable models in Z3. These models use a bounded-depth representation of recursive function definitions, where the bound is increased from zero as checking proceeds. An explicit and distinguishable representation of undefined parts of data values enables Demur to maximize property-checking power despite approximation – for example, by using parallel three-valued logical operators. Several case-studies present a mixture of successes and failures in comparison with current widely-used tools for property checking. Possible routes to improved performance are identified. Comparisons are drawn with other Z3-based tools with functional-language translators, such as Leon and Halo.
Boris Yakobowski.Fast Whole-program Verification Using On-the-fly Summarization
We present an on-the-fly summarization mechanism, employed by the Value Analysis plugin of Frama-C to significantly speed up its analyses. When a function call has been fully analyzed, the analyzer memorizes (1) the variables that were read during the analysis, (2) those that were written, and (3) the values for those input and output variables. This forms a summary of this particular call, which is saved in the hope that it may be reused later. This is the case when another call occurs with unchanged values for the input variables. We implemented our technique within Frama-C/Value. Using an agressive strategy that catches indiscriminately all function calls, we routinely obtain ×15 speedups in analysis time, with reasonable overhead w.r.t. memory consumption.
|26||June||2015 (anywhere on earth)|
Venue, Registration, and Accommodation
Please refer to the SAS 2015 website.
|9:00 – 10:00||Pascal Cuoq||Verifying the Absence of Undefined Behavior in a Minimal but Realistic Configuration of PolarSSL|
|10:00 – 10:30||Boris Yakobowski||Fast Whole-program Verification Using On-the-fly Summarization|
|11:00 – 12:00||Don Sannella||ThreadSafe: Static Analysis for Java Concurrency|
|12:00 – 12:30||Georges Dupéron and
||k-l-CFA: A Practical Implementation|
|14:00 – 15:00||Patrick Cousot||Sound Verification by Abstract Interpretation|
|15:00 – 15:30||Wolfgang Ahrendt,
||Loop Analysis Using Theorem Proving and Symbol Elimination|
|16:00 – 17:00||Max Schaefer||Analysing Software Engineering Data|
|17:00 – 17:30||Colin Runciman and
||Demur: Checking Functional-program Properties Using Bounded Recursion|
|Microsoft Research (chair)|
|Software Engineering Institute, Carnegie Mellon University|
|T.U. Madrid (UPM) and IMDEA Software Institute|
|NICTA, University of New South Wales, and Red Lizard Software|
|LIAFA, University of Paris Diderot, and CNRS|
|Chalmers University of Technology|
|University of Freiburg|