Static Analysis

Frontmatter

Block Me If You Can!

Context-Sensitive Parameterized Verification

Abstract

We present a method for automatic verification of systems with a parameterized number of communicating processes, such as mutual exclusion protocols or agreement protocols. To that end, we present a powerful abstraction framework that uses an efficient and precise symbolic encoding of (infinite) sets of configurations. In particular, it generalizes downward-closed sets that have successfully been used in earlier approaches to parameterized verification. We show experimentally the efficiency of the method, on various examples, including a fine-grained model of Szymanski’s mutual exclusion protocol, whose correctness, to the best of our knowledge, has not been proven automatically by any other existing methods.

Parosh Aziz Abdulla, Frédéric Haziza, Lukáš Holík

Peak Cost Analysis of Distributed Systems

Abstract

We present a novel static analysis to infer the peak cost of distributed systems. The different locations of a distributed system communicate and coordinate their actions by posting tasks among them. Thus, the amount of work that each location has to perform can greatly vary along the execution depending on: (1) the amount of tasks posted to its queue, (2) their respective costs, and (3) the fact that they may be posted in parallel and thus be pending to execute simultaneously. The peak cost of a distributed location refers to the maximum cost that it needs to carry out along its execution. Inferring the peak cost is challenging because it increases and decreases along the execution, unlike the standard notion of total cost which is cumulative. Our key contribution is the novel notion of quantified queue configuration which captures the worst-case cost of the tasks that may be simultaneously pending to execute at each location along the execution. A prototype implementation demonstrates the accuracy and feasibility of the proposed peak cost analysis.

Elvira Albert, Jesús Correas, Guillermo Román-Díez

Backward Analysis via over-Approximate Abstraction and under-Approximate Subtraction

Abstract

We propose a novel approach for computing weakest liberal safe preconditions of programs. The standard approaches, which call for either underapproximation of a greatest fixed point, or complementation of a least fixed point, are often difficult to apply successfully. Our approach relies on a different decomposition of the weakest precondition of loops. We exchange the greatest fixed point for the computation of a least fixed point above a recurrent set, instead of the bottom element. Convergence is achieved using over-approximation, while in order to maintain soundness we use an under-approximating logical subtraction operation. Unlike general complementation, subtraction more easily allows for increased precision in case its arguments are related. The approach is not restricted to a specific abstract domain and we use it to analyze programs using the abstract domains of intervals and of 3-valued structures

Alexey Bakhirkin, Josh Berdine, Nir Piterman

SawjaCard: A Static Analysis Tool for Certifying Java Card Applications

Abstract

This paper describes the design and implementation of a static analysis tool for certifying Java Card applications, according to security rules defined by the smart card industry. Java Card is a dialect of Java designed for programming multi-application smart cards and the tool, called SawjaCard, has been specialised for the particular Java Card programming patterns. The tool is built around a static analysis engine which uses a combination of numeric and heap analysis. It includes a model of the Java Card libraries and the Java Card firewall. The tool has been evaluated on a series of industrial applets and is shown to automate a substantial part of the validation process.

Frédéric Besson, Thomas Jensen, Pierre Vittet

Cyclic Abduction of Inductively Defined Safety and Termination Preconditions

Abstract

We introduce cyclic abduction: a new method for automatically inferring safety and termination preconditions of heap-manipulating while programs, expressed as inductive definitions in separation logic. Cyclic abduction essentially works by searching for a cyclic proof of the desired property, abducing definitional clauses of the precondition as necessary in order to advance the proof search process.

We provide an implementation, \(\textsc{Caber}\), of our cyclic abduction method, based on a suite of heuristically guided tactics. It is often able to automatically infer preconditions describing lists, trees, cyclic and composite structures which, in other tools, previously had to be supplied by hand.

James Brotherston, Nikos Gorogiannis

Expectation Invariants for Probabilistic Program Loops as Fixed Points

Abstract

We present static analyses for probabilistic loops using expectation invariants. Probabilistic loops are imperative while-loops augmented with calls to random variable generators. Whereas, traditional program analysis uses Floyd-Hoare style invariants to over-approximate the set of reachable states, our approach synthesizes invariant inequalities involving the expected values of program expressions at the loop head. We first define the notion of expectation invariants, and demonstrate their usefulness in analyzing probabilistic program loops. Next, we present the set of expectation invariants for a loop as a fixed point of the pre-expectation operator over sets of program expressions. Finally, we use existing concepts from abstract interpretation theory to present an iterative analysis that synthesizes expectation invariants for probabilistic program loops. We show how the standard polyhedral abstract domain can be used to synthesize expectation invariants for probabilistic programs, and demonstrate the usefulness of our approach on some examples of probabilistic program loops.

Aleksandar Chakarov, Sriram Sankaranarayanan

An Abstract Domain to Infer Octagonal Constraints with Absolute Value

Abstract

The octagon abstract domain, devoted to discovering octagonal constraints (also called Unit Two Variable Per Inequality or UTVPI constraints) of a program, is one of the most commonly used numerical abstractions in practice, due to its quadratic memory complexity and cubic time complexity. However, the octagon domain itself is restricted to express convex sets and has limitations in handling non-convex properties which are sometimes required for proving some numerical properties in a program. In this paper, we intend to extend the octagon abstract domain with absolute value, to infer certain non-convex properties by exploiting the absolute value function. More precisely, the new domain can infer relations of the form {±X ±Y ≤ c, ±X ±|Y| ≤ d, ±|X| ±|Y| ≤ e}. We provide algorithms for domain operations such that the new domain still enjoys the same asymptotic complexity as the octagon domain. Moreover, we present an approach to support strict inequalities over rational or real-valued variables in this domain, which also fits for the octagon domain. Experimental results of our prototype are encouraging; The new domain is scalable and able to find non-convex invariants of interest in practice but without too much overhead (compared with that using octagons).

Liqian Chen, Jiangchao Liu, Antoine Miné, Deepak Kapur, Ji Wang

Verifying Recursive Programs Using Intraprocedural Analyzers

Abstract

Recursion can complicate program analysis significantly. Some program analyzers simply ignore recursion or even refuse to check recursive programs. In this paper, we propose an algorithm that uses a recursion-free program analyzer as a black box to check recursive programs. With extended program constructs for assumptions, assertions, and nondeterministic values, our algorithm computes function summaries from inductive invariants computed by the underlying program analyzer. Such function summaries enable our algorithm to check recursive programs. We implement a prototype using the recursion-free program analyzer CPAChecker and compare it with other program analyzers on the benchmarks in the 2014 Competition on Software Verification.

Yu-Fang Chen, Chiao Hsieh, Ming-Hsien Tsai, Bow-Yaw Wang, Farn Wang

Automatic Analysis of Open Objects in Dynamic Language Programs

Abstract

In dynamic languages, objects are open–they support iteration over and dynamic addition/deletion of their attributes. Open objects, because they have an unbounded number of attributes, are difficult to abstract without a priori knowledge of all or nearly all of the attributes and thus pose a significant challenge for precise static analysis. To address this challenge, we present the HOO (Heap with Open Objects) abstraction that can precisely represent and infer properties about open-object-manipulating programs without any knowledge of specific attributes. It achieves this by building upon a relational abstract domain for sets that is used to reason about partitions of object attributes. An implementation of the resulting static analysis is used to verify specifications for dynamic language framework code that makes extensive use of open objects, thus demonstrating the effectiveness of this approach.

Arlen Cox, Bor-Yuh Evan Chang, Xavier Rival

Invariance of Conjunctions of Polynomial Equalities for Algebraic Differential Equations

Abstract

In this paper we seek to provide greater automation for formal deductive verification tools working with continuous and hybrid dynamical systems. We present an efficient procedure to check invariance of conjunctions of polynomial equalities under the flow of polynomial ordinary differential equations. The procedure is based on a necessary and sufficient condition that characterizes invariant conjunctions of polynomial equalities. We contrast this approach to an alternative one which combines fast and sufficient (but not necessary) conditions using differential cuts for soundly restricting the system evolution domain.

Khalil Ghorbal, Andrew Sogokon, André Platzer

On Program Equivalence with Reductions

Abstract

Program equivalence is a well-known problem with a wide range of applications, such as algorithm recognition, program verification and program optimization. This problem is also known to be undecidable if the class of programs is rich enough, in which case semi-algorithms are commonly used. We focus on programs represented as Systems of Affine Recurrence Equations (SARE), defined over parametric polyhedral domains, a well known formalism for the polyhedral model. SAREs include as a proper subset, the class of affine control loop programs. Several program equivalence semi-algorithms were already proposed for this class. Some take into account algebraic properties such as associativity and commutativity. To the best of our knowledge, none of them manage reductions, i.e., accumulations of a parametric number of sub-expressions using an associative and commutative operator. Our main contribution is a new semi-algorithm to manage reductions. In particular, we outline the ties between this problem and the perfect matching problem in a parametric bipartite graph.

Guillaume Iooss, Christophe Alias, Sanjay Rajopadhye

A Progress Bar for Static Analyzers

Abstract

We present a technique for devising a progress indicator of static analyzers. Progress indicator is a useful user interface that shows how close a static analysis has progressed so far to its completion. Because static analysis’ progress depends on the semantic complexity, not on the code size, of the target software, devising an accurate progress-indicator is not obvious. Our technique first combines a semantic-based pre-analysis and a statistical method to approximate how a main analysis progresses in terms of lattice height of the abstract domain. Then, we use this information during the main analysis and estimate the analysis’ current progress. We apply the technique to three existing analyses (interval, octagon, and pointer analyses) for C and show the technique estimates the actual analysis progress for various benchmarks.

Woosuk Lee, Hakjoo Oh, Kwangkeun Yi

Sparse Dataflow Analysis with Pointers and Reachability

Abstract

Many static analyzers exploit sparseness techniques to reduce the amount of information being propagated and stored during analysis. Although several variations are described in the literature, no existing technique is suitable for analyzing JavaScript code. In this paper, we point out the need for a sparse analysis framework that supports pointers and reachability.We present such a framework, which uses static single assignment form for heap addresses and computes def-use information on-the-fly.We also show that essential information about dominating definitions can be maintained efficiently using quadtrees. The framework is presented as a systematic modification of a traditional dataflow analysis algorithm.

Our experimental results demonstrate the effectiveness of the technique for a suite of JavaScript programs. By also comparing the performance with an idealized staged approach that computes pointer information with a pre-analysis, we show that the cost of computing def-use information onthe- fly is remarkably small.

Magnus Madsen, Anders Møller

Reactivity of Cooperative Systems

Application to ReactiveML

Abstract

Cooperative scheduling enables efficient sequential implementations of concurrency. It is widely used to provide lightweight threads facilities as libraries or programming constructs in many programming languages. However, it is up to programmers to actually cooperate to ensure the reactivity of their programs.

We present a static analysis that checks the reactivity of programs by abstracting them into so-called behaviors using a type-and-effect system. Our objective is to find a good compromise between the complexity of the analysis and its precision for typical reactive programs. The simplicity of the analysis is mandatory for the programmer to be able to understand error messages and how to fix reactivity problems.

Ourwork is applied and implemented in the functional synchronous language ReactiveML. It handles recursion, higher-order processes and firstclass signals. We prove the soundness of our analysis with respect to the big-step semantics of the language: a well-typed program with reactive effects is reactive. The analysis is easy to implement and generic enough to be applicable to other models of concurrency such as coroutines.

Louis Mandel, Cédric Pasteur

Synthesis of Memory Fences via Refinement Propagation

Abstract

We address the problem of fence inference in infinite-state concurrent programs running on relaxed memory models such as TSO and PSO. We present a novel algorithm that can automatically synthesize the necessary fences for infinite-state programs.

Our technique is based on two main ideas: (i) verification with numerical domains: we reduce verification under relaxed models to verification under sequential consistency using integer and boolean variables. This enables us to combine abstraction refinement over booleans with powerful numerical abstractions over the integers. (ii) synthesis with refinement propagation: to synthesize fences for a program P, we combine abstraction refinements used for successful synthesis of programs coarser than P into a new candidate abstraction for P. This “proof reuse” approach dramatically reduces the time required to discover a proof for P.

We implemented our technique and successfully applied it to several challenging concurrent algorithms, including state of the art concurrent work-stealing queues.

Yuri Meshman, Andrei Dan, Martin Vechev, Eran Yahav

Speeding Up Logico-Numerical Strategy Iteration

Abstract

We introduce an efficient combination of polyhedral analysis and predicate partitioning. Template polyhedral analysis abstracts numerical variables inside a program by one polyhedron per control location, with a priori fixed directions for the faces. The strongest inductive invariant in such an abstract domain may be computed by a combination of strategy iteration and SMT solving. Unfortunately, the above approaches lead to unacceptable space and time costs if applied to a program whose control states have been partitioned according to predicates. We therefore propose a modification of the strategy iteration algorithm where the strategies are stored succinctly, and the linear programs to be solved at each iteration step are simplified according to an equivalence relation. We have implemented the technique in a prototype tool and we demonstrate on a series of examples that the approach performs significantly better than previous strategy iteration techniques.

David Monniaux, Peter Schrammel

Cost-Aware Automatic Program Repair

Abstract

We present a formal framework for repairing infinite-state, imperative, sequential programs, with (possibly recursive) procedures and multiple assertions; the framework can generate repaired programs by modifying the original erroneous program in multiple program locations, and can ensure the readability of the repaired program using user-defined expression templates; the framework also generates a set of inductive assertions that serve as a proof of correctness of the repaired program. As a step toward integrating programmer intent and intuition in automated program repair, we present a cost-aware formulation - given a cost function associated with permissible statement modifications, the goal is to ensure that the total program modification cost does not exceed a given repair budget. As part of our predicate abstractionbased solution framework, we present a sound and complete algorithm for repair of Boolean programs. We have developed a prototype tool based on SMT solving and used it successfully to repair diverse errors in benchmark C programs.

Roopsha Samanta, Oswaldo Olivo, E. Allen Emerson

An Abstract Domain Combinator for Separately Conjoining Memory Abstractions

Abstract

The breadth and depth of heap properties that can be inferred by the union of today’s shape analyses is quite astounding. Yet, achieving scalability while supporting a wide range of complex data structures in a generic way remains a long-standing challenge. In this paper, we propose a way to side-step this issue by defining a generic abstract domain combinator for combining memory abstractions on disjoint regions. In essence, our abstract domain construction is to the separating conjunction in separation logic as the reduced product construction is to classical, non-separating conjunction. This approach eases the design of the analysis as memory abstract domains can be re-used by applying our separating conjunction domain combinator. And more importantly, this combinator enables an analysis designer to easily create a combined domain that applies computationally-expensive abstract domains only where it is required.

Antoine Toubhans, Bor-Yuh Evan Chang, Xavier Rival

A Decision Tree Abstract Domain for Proving Conditional Termination

Abstract

We present a new parameterized abstract domain able to refine existing numerical abstract domains with finite disjunctions. The elements of the abstract domain are decision trees where the decision nodes are labeled with linear constraints, and the leaf nodes belong to a numerical abstract domain.

The abstract domain is parametric in the choice between the expressivity and the cost of the linear constraints for the decision nodes (e.g., polyhedral or octagonal constraints), and the choice of the abstract domain for the leaf nodes. We describe an instance of this domain based on piecewise-defined ranking functions for the automatic inference of sufficient preconditions for program termination.

We have implemented a static analyzer for proving conditional termination of programs written in (a subset of) C and, using experimental evidence, we show that it performs well on a wide variety of benchmarks, it is competitive with the state of the art and is able to analyze programs that are out of the reach of existing methods.

Caterina Urban, Antoine Miné

Region-Based Selective Flow-Sensitive Pointer Analysis

Abstract

We introduce a new region-based SELective Flow-Sensitive (Selfs) approach to inter-procedural pointer analysis for C that operates on the regions partitioned from a program. Flow-sensitivity is maintained between the regions but not inside, making traditional flow-insensitive and flow-sensitive as well as recent sparse flow-sensitive analyses all special instances of our Selfs framework. By separating region partitioning as an independent concern from the rest of the pointer analysis, Selfs facilitates the development of flow-sensitive variations with desired efficiency and precision tradeoffs by reusing existing pointer resolution algorithms. We also introduce a new unification-based approach for region partitioning to demonstrate the generality and flexibility of our Selfs framework, as evaluated using SPEC2000/2006 benchmarks in LLVM.

Sen Ye, Yulei Sui, Jingling Xue

Backmatter