Abstract Many compilation stages of smart contracts on the Ethereum blockchain have been transitioned to the intermediate language . Tasks such as smart contract optimization and bytecode generation are—or will soon be—performed directly at the level in the compilers for the higher-level languages such as Solidity. In this paper, we develop a formal semantics of programs in Rocq, suitable for verification, which allows formal reasoning at the level of code or generation tools processing programs. Our semantics is expressive enough to be the basis for formal verification tools, and simple enough to make the development of such tools feasible. In order to prove its adequacy for verification, we develop in Rocq a checker (and associated soundness proofs), based on our semantics, able to verify the results of the liveness analysis stage of the official Solidity compiler , which opens the door towards formally verified Ethereum’s smart contracts compilation. Experiments on more than 1,500 smart contracts show that we are able to automatically verify ’s liveness analysis results in negligible time.

Context: Superoptimization is a synthesis technique that, given a loop-free sequence of instructions, searches for an equivalent sequence that is optimal wrt. an objective function. Superoptimization of Ethereum smart contracts aims at minimizing the size of their bytecode and the gas consumption of executing the contract’s functions. The search for the optimal solution poses huge computational demands –as the search space to find the optimal sequence is exponential on the given size-bound – being the main challenge for superoptimization today to scale up to real, industrial software. Even if the underlying problem for finding the optimal solution is decidable, practical tools often prioritize efficiency over completeness. This means they might be implemented to find a sub-optimal solution or even time out. Objective: This work aims at leveraging superoptimization to a real setting: Ethereum blockchain. This paper proposes a neural-guided superoptimization (NGS) approach which incorporates deep neural networks using (supervised) learning into superoptimization to improve scalability by predicting: (1) if a sequence is already optimal and hence the search can be skipped; (2) the size-bound for the optimal solution in order to reduce the search space. Method: We have downloaded over 13,000 smart contracts deployed on the blockchain for training and testing the machine learning models, and a disjoint set with 100 of the smart contracts with more transactions to prove our scalability gains and impact for the Ethereum community. Results: Incorporating DNNs resulted in a 16x overall speedup (12x for gas) with only 12% optimization loss (14% for gas), or a 3-4x speedup with no optimization loss. For the 100 analyzed contracts, this approach reduced the average compilation time to 3 min per contract and achieved monetary savings of $1.24M. Conclusions: The integration of machine learning models mitigates several limitations of traditional superoptimization by drastically reducing execution times while maintaining most of the original optimization gains.

Program optimization is a key factor for green software. In the context of the Ethereum blockchain, optimization is particularly relevant because there is a fee to pay for each EVM (Ethereum Virtual Machine) instruction executed and also there exist bytecode-size limitations for deploying the software on the blockchain. Still, optimization of EVM code is not as widely spread as one could imagine. This is at least partly due to the lack of trust in the correctness of the tools, as security is even more relevant than efficiency in the blockchain context in which bugs may cause huge economical losses. This article develops a formal verification framework using Coq to ensure the security of EVM optimizations performed on jump-free sequences of EVM bytecode. By means of Coq’s theorem proving capabilities, we are able to automatically verify/certify that an optimized jump-free sequence of EVM opcodes is semantically equivalent to a given original one. We also present an extension to our framework that can handle inter-block optimizations that propagate global information across blocks. We have applied our tool to successfully prove the security of peephole optimizations performed by the standard Solidity compiler, and also to existing EVM superoptimization tools (namely GASOL and Superstack) in which we have found bugs that have been reported and fixed.

Abstract The efficiency and the security of smart contracts are their two fundamental properties, but might come at odds: the use of optimizers to enhance efficiency may introduce bugs and compromise security. Our focus is on (Ethereum Virtual Machine) block-optimizations , which enhance the efficiency of jump-free blocks of opcodes by eliminating, reordering and even changing the original opcodes. We reconcile efficiency and security by providing the verification technology to formally prove the correctness of block-optimizations on smart contracts using the Coq proof assistant. This amounts to the challenging problem of proving semantic equivalence of two blocks of instructions, which is realized by means of three novel Coq components: a symbolic execution engine which can execute an block and produce a symbolic state; a number of simplification lemmas which transform a symbolic state into an equivalent one; and a checker of symbolic states to compare the symbolic states produced for the two blocks under comparison. Artifact: https://doi.org/10.5281/zenodo.7863483

Abstract This paper presents a new framework to synthesize lower-bounds on the worst-case cost for non-deterministic integer loops. As in previous approaches, the analysis searches for a metering function that under-approximates the number of loop iterations. The key novelty of our framework is the specialization of loops, which is achieved by restricting their enabled transitions to a subset of the inputs combined with the narrowing of their transition scopes. Specialization allows us to find metering functions for complex loops that could not be handled before or be more precise than previous approaches. Technically, it is performed (1) by using quasi-invariants while searching for the metering function, (2) by strengthening the loop guards, and (3) by narrowing the space of non-deterministic choices. We also propose a Max-SMT encoding that takes advantage of the use of soft constraints to force the solver look for more accurate solutions. We show our accuracy gains on benchmarks extracted from the 2020 Termination and Complexity Competition by comparing our results to those obtained by the "Image missing" system.

Abstract In order to automatically infer the resource consumption of programs, analyzers track how data sizes change along program’s execution. Typically, analyzers measure the sizes of data by applying norms which are mappings from data to natural numbers that represent the sizes of the corresponding data. When norms are defined by taking type information into account, they are named typed-norms. This article presents a transformational approach to resource analysis with typed-norms that are inferred by a data-flow analysis. The analysis is based on a transformation of the program into an intermediate abstract program in which each variable is abstracted with respect to all considered norms which are valid for its type. We also present the data-flow analysis to automatically infer the required, useful, typed-norms from programs. Our analysis is formalized on a simple rule-based representation to which programs written in different programming paradigms (e.g., functional, logic, and imperative) can be automatically translated. Experimental results on standard benchmarks used by other type-based analyzers show that our approach is both efficient and accurate in practice.

Abstract Control-flow refinement refers to program transformations whose purpose is to make implicit control-flow explicit, and is used in the context of program analysis to increase precision. Several techniques have been suggested for different programming models, typically tailored to improving precision for a particular analysis. In this paper we explore the use of partial evaluation of Horn clauses as a general-purpose technique for control-flow refinement for integer transitions systems. These are control-flow graphs where edges are annotated with linear constraints describing transitions between corresponding nodes, and they are used in many program analysis tools. Using partial evaluation for control-flow refinement has the clear advantage over other approaches in that soundness follows from the general properties of partial evaluation; in particular, properties such as termination and complexity are preserved. We use a partial evaluation algorithm incorporating property-based abstraction, and show how the right choice of properties allows us to prove termination and to infer complexity of challenging programs that cannot be handled by state-of-the-art tools. We report on the integration of the technique in a termination analyzer, and its use as a preprocessing step for several cost analyzers.

This article presents a may-happen-in-parallel (MHP) analysis for languages with actor-based concurrency . In this concurrency model, actors are the concurrency units such that, when a method is invoked on an actor a 2 from a task executing on actor a 1 , statements of the current task in a 1 may run in parallel with those of the (asynchronous) call on a 2 , and with those of transitively invoked methods. The goal of the MHP analysis is to identify pairs of statements in the program that may run in parallel in any execution. Our MHP analysis is formalized as a method-level ( local ) analysis whose information can be modularly composed to obtain application-level ( global ) information. The information yielded by the MHP analysis is essential to infer more complex properties of actor-based concurrent programs, for example, data race detection, deadlock freeness, termination, and resource consumption analyses can greatly benefit from the MHP relations to increase their accuracy. We report on MayPar, a prototypical implementation of an MHP static analyzer for a distributed asynchronous language.

We investigate the problem of verifying the absence of zeno executions in a hybrid system. A zeno execution is one in which there are infinitely many discrete transitions in a finite time interval. The presence of zeno executions poses challenges towards implementation and analysis of hybrid control systems. We present a simple transformation of the hybrid system which reduces the non-zenoness verification problem to the termination verification problem, that is, the original system has no zeno executions if and only if the transformed system has no non-terminating executions. This provides both theoretical insights and practical techniques for non-zenoness verification. Further, it also provides techniques for isolating parts of the hybrid system and its initial states which do not exhibit zeno executions. We illustrate the feasibility of our approach by applying it on hybrid system examples.

Summary This article presents a novel cost analysis framework for concurrent objects. Concurrent objects form a well‐established model for distributed concurrent systems. In this model, objects are the concurrency units that communicate among them via asynchronous method calls. Cost analysis aims at automatically approximating the resource consumption of executing a program in terms of its input parameters. While cost analysis for sequential programming languages has received considerable attention, concurrency and distribution have been notably less studied. The main challenges of cost analysis in a concurrent setting are as follows. First, inferring precise size abstractions for data in the program in the presence of shared memory. This information is essential for bounding the number of iterations of loops. Second, distribution suggests that analysis must infer the cost of the diverse distributed components separately. We handle this by means of a novel form of object‐sensitive recurrence equations that use cost centres in order to keep the resource usage assigned to the different components separate. We have implemented our analysis and evaluated it on several small applications that are classical examples of concurrent and distributed programming. Copyright © 2015 John Wiley & Sons, Ltd.

In this article, we study the complexity of the problems: given a loop, described by linear constraints over a finite set of variables, is there a linear or lexicographical-linear ranking function for this loop? While existence of such functions implies termination, these problems are not equivalent to termination. When the variables range over the rationals (or reals), it is known that both problems are PTIME decidable. However, when they range over the integers, whether for single-path or multipath loops, the complexity has not yet been determined. We show that both problems are coNP-complete. However, we point out some special cases of importance of PTIME complexity. We also present complete algorithms for synthesizing linear and lexicographical-linear ranking functions, both for the general case and the special PTIME cases. Moreover, in the rational setting, our algorithm for synthesizing lexicographical-linear ranking functions extends existing ones, because our definition for such functions is more general, yet it has PTIME complexity.

In heap-based languages, knowing that a variable x points to an acyclic data structure is useful for analyzing termination. This information guarantees that the depth of the data structure to which x points is greater than the depth of the structure pointed to by x. fld , and allows bounding the number of iterations of a loop that traverses the data structure on fld . In general, proving termination needs acyclicity, unless program-specific or nonautomated reasoning is performed. However, recent work could prove that certain loops terminate even without inferring acyclicity, because they traverse data structures “acyclically.” Consider a double-linked list: if it is possible to demonstrate that every cycle involves both the “next” and the “prev” field, then a traversal on “next” terminates since no cycle will be traversed completely. This article develops a static analysis inferring field-sensitive reachability and cyclicity information, which is more general than existing approaches. Propositional formulæ are computed, which describe which fields may or may not be traversed by paths in the heap. Consider a tree with edges “left” and “right” to the left and right subtrees, and “parent” to the parent node: termination of a loop traversing leaf-up cannot be guaranteed by state-of-the-art analyses. Instead, propositional formulæ computed by this analysis indicate that cycles must traverse “parent” and at least one between “left” and “right”: termination is guaranteed, as no cycle is traversed completely. This work defines the necessary abstract domains and builds an abstract semantics on them. A prototypical implementation provides the expected result on relevant examples.

In this paper we study the complexity of the Linear Ranking problem: given a loop, described by linear constraints over a finite set of integer variables, is there a linear ranking function for this loop? While existence of such a function implies termination, this problem is not equivalent to termination. When the variables range over the rationals or reals, the Linear Ranking problem is known to be PTIME decidable. However, when they range over the integers, whether for single-path or multipath loops, the complexity of the Linear Ranking problem has not yet been determined. We show that it is coNP-complete. However, we point out some special cases of importance of PTIME complexity. We also present complete algorithms for synthesizing linear ranking functions, both for the general case and the special PTIME cases.

Cost analysis aims at determining the amount of resources required to run a program in terms of its input data sizes. The most challenging step is to infer the cost of executing the loops in the program. This requires bounding the number of iterations of each loop and finding tight bounds for the cost of each of its iterations. This article presents a novel approach to infer upper and lower bounds from cost relations . These relations are an extended form of standard recurrence equations that can be nondeterministic, contain inexact size constraints and have multiple arguments that increase and/or decrease. We propose novel techniques to automatically transform cost relations into worst-case and best-case deterministic one-argument recurrence relations. The solution of each recursive relation provides a precise upper-bound and lower-bound for executing a corresponding loop in the program. Importantly, since the approach is developed at the level of the cost equations, our techniques are programming language independent.

ABS is an abstract behavioural specification language to model distributed concurrent systems. Characteristic features of ABS are that: (1) it allows abstracting from implementation details while remaining executable: a functional sub-language over abstract data types is used to specify internal, sequential computations; and (2) the imperative sub-language provides flexible concurrency and synchronization mechanisms by means of asynchronous method calls, release points in method definitions, and cooperative scheduling of method activations. This paper presents COSTABS, a COSt and Termination analyzer for ABS, which is able to prove termination and obtain resource usage bounds for both the imperative and functional fragments of programs. The resources that COSTABS can infer include termination, number of execution steps, memory consumption, number of asynchronous calls, among others. The analysis bounds provide formal guarantees that the execution of the program will never exceed the inferred amount of resources. The system can be downloaded as free software from its web site, where a repository of examples and a web interface are also provided. To the best of our knowledge, COSTABS is the first system able to perform resource analysis for a concurrent language.

We present the concepts, usage and prototypical implementation of MayPar, a may-happen-in-parallel (MHP) static analyzer for a distributed asynchronous language based on concurrent objects. Our tool allows analyzing an application and finding out the pairs of statements that can execute in parallel. The information can be displayed by means of a graphical representation of the MHP analysis graph or, in a textual way, as a set of pairs which identify the program points that may run in parallel. The information yield by MayPar can be relevant (1) to spot bugs in the program related to fragments of code which should not run in parallel and also (2) to improve the precision of other analyses which infer more complex properties (e.g., termination and cost).

In this article we study the decidability of termination of several variants of simple integer loops, without branching in the loop body and with affine constraints as the loop guard (and possibly a precondition). We show that termination of such loops is undecidable in some cases, in particular, when the body of the loop is expressed by a set of linear inequalities where the coefficients are from Z ∪ { r } with r an arbitrary irrational; when the loop is a sequence of instructions, that compute either linear expressions or the step function; and when the loop body is a piecewise linear deterministic update with two pieces. The undecidability result is proven by a reduction from counter programs, whose termination is known to be undecidable. For the common case of integer linear-constraint loops with rational coefficients we have not succeeded in proving either decidability or undecidability of termination, but we show that a Petri net can be simulated with such a loop; this implies some interesting lower bounds. For example, termination for a partially specified input is at least EXPSPACE-hard.

The task level of a program is the maximum number of tasks that can be available (i.e., not finished nor suspended) simultaneously during its execution for any input data. Static knowledge of the task level is of utmost importance for understanding and debugging parallel programs as well as for guiding task schedulers. We present, to the best of our knowledge, the first static analysis which infers safe and precise approximations on the task level for a language with async-finish parallelism. In parallel languages, async and finish are basic constructs for, respectively, spawning tasks and waiting until they terminate. They are the core of modern, parallel, distributed languages like X10. Given a (parallel) program, our analysis returns a task-level upper bound, i.e., a function on the program's input arguments that guarantees that the task level of the program will never exceed its value along any execution. Our analysis provides a series of useful (over)-approximations, going from the total number of tasks spawned in the execution up to an accurate estimation of the task level.

Resource guarantees allow being certain that programs will run within the indicated amount of resources, which may refer to memory consumption, number of instructions executed, etc. This information can be very useful, especially in real-time and safety-critical applications. Nowadays, a number of automatic tools exist, often based on type systems or static analysis, which produce such resource guarantees. In spite of being based on theoretically sound techniques, the implemented tools may contain bugs which render the resource guarantees thus obtained not completely trustworthy. Performing full-blown verification of such tools is a daunting task, since they are large and complex. In this work we investigate an alternative approach whereby, instead of the tools, we formally verify the results of the tools. We have implemented this idea using COSTA, a state-of-the-art static analysis system, for producing resource guarantees and KeY, a state-of-the-art verification tool, for formally verifying the correctness of such resource guarantees. Our preliminary results show that the proposed tool cooperation can be used for automatically producing verified resource guarantees.

The accurate prediction of program's memory requirements is a critical component in software development. Existing heap space analyses either do not take deallocation into account or adopt specific models of garbage collectors which do not necessarily correspond to the actual memory usage. We present a novel approach to inferring upper bounds on memory requirements of Java-like programs which is parametric on the notion of object lifetime, i.e., on when objects become collectible. If objects lifetimes are inferred by a reachability analysis, then our analysis infers accurate upper bounds on the memory consumption for a reachability-based garbage collector. Interestingly, if objects lifetimes are inferred by a heap liveness analysis, then we approximate the program minimal memory requirement, i.e., the peak memory usage when using an optimal garbage collector which frees objects as soon as they become dead. The key idea is to integrate information on objects lifetimes into the process of generating the recurrence equations which capture the memory usage at the different program states. If the heap size limit is set to the memory requirement inferred by our analysis, it is ensured that execution will not exceed the memory limit with the only assumption that garbage collection works when the limit is reached. Experiments on Java bytecode programs provide evidence of the feasibility and accuracy of our analysis.

The peak heap consumption of a program is the maximum size of the live data on the heap during the execution of the program, i.e., the minimum amount of heap space needed to run the program without exhausting the memory. It is well-known that garbage collection (GC) makes the problem of predicting the memory required to run a program difficult. This paper presents, the best of our knowledge, the first live heap space analysis for garbage-collected languages which infers accurate upper bounds on the peak heap usage of a program's execution that are not restricted to any complexity class, i.e., we can infer exponential, logarithmic, polynomial, etc., bounds. Our analysis is developed for an (sequential) object-oriented bytecode language with a scoped-memory manager that reclaims unreachable memory when methods return. We also show how our analysis can accommodate other GC schemes which are closer to the ideal GC which collects objects as soon as they become unreachable. The practicality of our approach is experimentally evaluated on a prototype implementation. We demonstrate that it is fully automatic, reasonably accurate and efficient by inferring live heap space bounds for a standardized set of benchmarks, the JOlden suite.

This paper describes the encoding of a telecommunications feature subscription configuration problem to propositional logic and its solution using a state-of-the-art Boolean satisfaction solver. The transformation of a problem instance to a corresponding propositional formula in conjunctive normal form is obtained in a declarative style. An experimental evaluation indicates that our encoding is considerably faster than previous approaches based on the use of Boolean satisfaction solvers. The key to obtaining such a fast solver is the careful design of the Boolean representation and of the basic operations in the encoding. The choice of a declarative programming style makes the use of complex circuit designs relatively easy to incorporate into the encoder and to fine tune the application.

A logic program consists of a logic component and a control component. The former is a specification in predicate logic whereas the latter defines the order of subgoal selection. The order of subgoal selection is often controlled with delay declarations that specify that a subgoal is to suspend until some condition on its arguments is satisfied. Reasoning about delay declarations is notoriously difficult for the programmer and it is not unusual for a program and a goal to reduce to a state that contains a subgoal that suspends indefinitely. Suspending subgoals are usually unintended and often indicate an error in the logic or the control. A number of abstract interpretation schemes have therefore been proposed for checking that a given program and goal cannot reduce to such a state. This article considers a reversal of this problem, advocating an analysis that for a given program infers a class of goals that do not lead to suspension. This article shows that this more general approach can have computational, implementational and user-interface advantages. In terms of user-interface, this approach leads to a lightweight point-and-click mode of operation in which, after directing the analyser at a file, the user merely has to inspect the results inferred by the analysis. In terms of implementation, the analysis can be straightforwardly realized as two simple fixpoint computations. In terms of computation, by modeling n ! different schedulings of n subgoals with a single Boolean function, it is possible to reason about the suspension behavior of large programs. In particular, the analysis is fast enough to be applied repeatedly within the program development cycle. The article also demonstrates that the method is precise enough to locate bugs in existing programs.

This article presents a heap space analysis for (sequential) Java bytecode. The analysis generates heap space cost relations which define at compile-time the heap consumption of a program as a function of its data size. These relations can be used to obtain upper bounds on the heap space located during the execution of the different methods. In addition, we describe how to refine the cost relations, by relying on escape analysis, in order to take into account the heap space that can be safely deallocated by the garbage collector upon exit from a corresponding method. These refined cost relations are then used to infer upper bounds on the active heap space upon methods return. Example applications for the analysis consider inference of constant heap usage and heap usage proportional to the data size (including polynomial and exponential heap consumption). Our prototype implementation is reported and demonstrated by means of a series of examples which illustrate how the analysis naturally encompasses standard data-structures like lists, trees and arrays with several dimensions written in object-oriented programming style.

This article makes two contributions to the work on semantics-based termination analysis for logic programs. The first involves a novel notion of type - based norm where for a given type, a corresponding norm is defined to count in a term the number of subterms of that type. This provides a collection of candidate norms, one for each type defined in the program. The second enables an analyzer to base termination proofs on the combination of several different norms. This is useful when different norms are better suited to justify the termination of different parts of the program. Application of the two contributions together consists in considering the combination of the type-based candidate norms for a given program. This results in a powerful and practical technique. Both contributions have been introduced into a working termination analyzer. Experimentation indicates that they yield state-of-the-art results in a fully automatic analysis tool, improving with respect to methods that do not use both types and combined norms.

This paper focuses on the inference of modes for which a logic program is guaranteed to terminate. This generalises traditional termination analysis where an analyser tries to verify termination for a specified mode. Our contribution is a methodology in which components of traditional termination analysis are combined with backwards analysis to obtain an analyser for termination inference. We identify a condition on the components of the analyser which guarantees that termination inference will infer all modes which can be checked to terminate. The application of this methodology to enhance a traditional termination analyser to perform also termination inference is demonstrated.

This note illustrates theoretical worst-case scenarios for groundness analyses obtained through abstract interpretation over the abstract domains of definite (Def) and positive (Pos) Boolean functions. For Def, an example is given for which any Def-based abstract interpretation for groundness analysis follows a chain which is exponential in the number of argument positions as well as in the number of clauses but sub-exponential in the size of the program. For Pos, we strengthen a previous result by illustrating an example for which any Pos-based abstract interpretation for groundness analysis follows a chain which is exponential in the size of the program. It remains an open problem to determine if the worst case for Def is really as bad as that for Pos.