SMT 2020

Solidity is the dominant programming language for Ethereum smart contracts. This paper presents a high-level formalization of the Solidity language with a focus on the memory model. The presented formalization covers all features of the language related to managing state and memory. In addition, the formalization we provide is effective: all but few features can be encoded in the quantifier-free fragment of standard SMT theories. This enables precise and efficient reasoning about the state of smart contracts written in Solidity. The formalization is implemented in the solc-verify verifier and we provide an extensive set of tests that covers the breadth of the required semantics. We also provide an evaluation on the test set that validates the semantics and shows the novelty of the approach compared to other Solidity-level contract analysis tools.

Constrained Horn Clauses (CHC) are a convenient intermediate verification language that can be generated by several verification tools, and that can be processed by several mature and efficient Horn solvers. One of the main challenges when using CHC in verification is the encoding of program with heap-allocated data-structures: such data-structures are today either represented explicitly using the theory of arrays, or are transformed away with the help of invariants or refinement types. Both approaches have disadvantages: they are low-level, do not preserve the structure of a program well, and leave little design choice with respect to the handling of heap to the Horn solver. This abstract presents ongoing work on the definition of a high-level SMT-LIB theory of heap, which in the context of CHC gives rise to standard interchange format for programs with heap data-structures. The abstract presents the signature and intuition behind the theory. A preliminary version of the theory axioms can be found in the appendix. The abstract is meant as a starting point for discussion, and request for comments.

Recent work in extending SMT solvers to higher-order logic (HOL) has not explored lifting quantifier instantiation algorithms to perform higher-order unification. As a consequence, widely used instantiation techniques, such as trigger- and particularly conflict-based, can only be applied in a limited manner. Congruence closure with free variables (CCFV) is a decision procedure for the E-ground (dis-)unification problem, which is at the heart of these instantiation techniques. Here, as a first step towards fully supporting trigger- and conflict-based instantiation in HOL, we define the E-ground (dis-)unification problem in λ-free higher-order logic (λfHOL), an extension of first-order logic where function symbols may be partially applied and functional variables may occur, and extend CCFV to solve it. To improve scalability in the context of handling higher-order variables, we rely on an encoding of the CCFV search as a propositional formula. We present a solution reconstruction procedure so that models for the propositional formula lead to solutions for the E-ground (dis-)unification problem. This is instrumental to port trigger- and conflict-based instantiation to be fully applied in λfHOL.

Bit blasting is the main method for solving SMT problems in the theory of fixed size bit vectors. It converts bit-vector problems to equisatisfiable Boolean satisfiability problems that are then solved by SAT solvers. We present an empirical evaluation of state-of-the-art SAT solvers on problems produced by bit blasting with the Yices SMT solver. The results are quite different from common SAT solver evaluations such as the SAT races and SAT competitions, which argues for extending these evaluations to include benchmarks derived from SMT problems.

Various approximate model counting techniques have been proposed and are used in many applications such as probabilistic inference and quantitative information-flow security. The hashing-based technique is a well-known approach and can be more scalable than exact model counting techniques. However, its performance is highly dependent on the performance of a decision procedure (SAT or SMT solver) and adding numerous hashing constraints to a formula might cause a solver to perform poorly.

We propose a model counting technique which computes lower and upper bounds of the number of solutions to an SMT formula by analyzing the structure of the formula, which means this approach does not rely on a decision procedure. Our algorithm runs in polynomial time and gives firm lower and upper bounds unlike other approximate model counters that compute probabilistic bounds. We compare our algorithm with state-of-the- art model counters and our experiments show that our approach is faster than others and provides a trade-off between computational effort and the precision of results.

A novel way to use SMT (Satisfiability Modulo Theories) solvers to compute the tropical prevariety (resp. equilibrium) of a polynomial system is presented. The new method is benchmarked against a naive approach that uses purely polyhedral methods. It turns out that the SMT approach is faster than the polyhedral approach for models that would otherwise take more than one minute to compute, in many cases by a factor of 60 or more, and in the worst case is only slower by a factor of two. Furthermore, the new approach is an anytime algorithm, thus offering a way to compute parts of the solution when the polyhedral approach is infeasible.

Reasoning tools for geometric equalities based on elimination methods are already integrated in some dynamic geometry systems (DGS), in particular in GeoGebra. However, no reasoning tools in any popular DGS environments for elementary inequalities exist yet. This paper investigates if the generic real quantifier elimination (RQE) methods and their existing implementations are mature enough from the practical point of view to explore simple elementary Euclidean triangle inequalities and the best possible geometric constants occurring in the inequalities. It is known, that from theoretical point, real geometry inequality problems can be cast as RQE problems and can be solved by RQE algorithms. Unfortunately, the computational complexity of the RQE algorithms are rather high. The practical question is, if the RQE problem formulations for the investigated geometric inequality are tractable in a reasonable time limit. If this is so, an RQE based geometry inequality prover may be also an integral part of DGS. As a first experimental step, we also implemented a real reasoning tool for GeoGebra called realgeom which uses Wolfram’s Mathematica poly-algorithmic RQE tool as an external service for solving the semi-algebraic problem associated to the geometric inequality exploration problem. Finally, we show by an example that parametric real root counting algorithms may be sufficient to attack certain inequality exploration problems and they can be later substitutes/alternatives for the general RQE tool in our framework.

The purpose of this paper is to explore the question “to what extent could we produce formal, machine-verifiable, proofs in real algebraic geometry?” The question has been asked before but as yet the leading algorithms for answering such questions have not been formalised. We present the thesis that a new algorithm for ascertaining satisfiability of formulae over the reals via Cylindrical Algebraic Coverings might provide a trace and outputs that allow the results to be more susceptible to machine verification than those of competing algorithms.

The recent years have seen a wealth of research on string solvers, i.e., SMT solvers that can check satisfiability of quantifier-free formulas over a background theory of strings and regular expressions. String solvers can be applied in different verification algorithms, for instance in symbolic execution to check path feasibility, in software model checking to take care of implication checks; a prime application area is security analysis for languages like JavaScript and PHP, for instance to discover vulnerability to injection attacks. To process constraints from those domains, it is necessary for string solvers to handle a delicate combination of (theoretically and practically) challenging operations: concatenation in word equations, to model assignments in programs; regular expressions or context-free grammars, to model properties or attack patterns; string length, to express string manipulation in programs; transduction, to express sanitisation, escape operations, and replacement operations in strings; and others. This talk will give a general introduction to string solving, and then present a solver architecture based on the concept of pre-image computation that is simple, yet turns out to be complete for an expressive fragment of string constraints. The architecture has been implemented in our solver OSTRICH (and is the result of joint work with many people).

Smart contracts are positioned to revolutionize today's business processes by automating financial transactions, digital media distribution, medical record management, property ownership registration, and more. The vast majority of smart contracts are implemented using virtual machines such as EVM and WebAssembly which are very powerful. However, bugs in smart contracts lead to tremendous economic losses.

I will describe our ongoing effort to leverage existing SMT solvers for verifying smart contracts and uncovering subtle bugs. We are developing SaaS technology demo.certora.com for smart contract verification. This technology is intended to be used as part of the CI/CD of smart contract development.

Safety properties of smart contracts are described in a high level manner to enable reuse across different smart contracts. The EVM code is decompiled into an intermediate representation using static analysis and the SMT formula is generated and fed into SMT solvers. The formulas include nonlinear integer arithmetic with large constants, uninterpreted functions, quantifications.

I will also describe some of the high level properties checked and bugs found using the SMT solvers.

This is a joint work with Thomas Bernardi, Nurit Dor, Anastasia Fedotov, Shelly Grossman, Alexander Nutz, Lior Oppenheim, Or Pistiner, John A. Toman, and James R. Wilcox.

In this paper, we present a reinforcement-learning based fuzzing system, BanditFuzz, that zeroes in on the grammatical constructs of well-formed inputs that are the root cause of performance slowdown in SMT solvers. BanditFuzz takes the following as input: a grammar G describing well-formed inputs to a set of distinct solvers (say, a target solver T and a reference solver R) that implement the same specification, and a fuzzing objective (e.g., maximize the relative performance difference between T and R). BanditFuzz outputs a list of grammatical constructs that are ranked in descending order by how likely they are to maximize performance differences between solvers T and R. Using BanditFuzz, we constructed two benchmark suites (with 400 floating- point and 300 string instances) that expose performance issues in all considered solvers, namely, Z3, CVC4, Colibri, MathSAT, Z3seq, and Z3str3. We also performed a comparison of BanditFuzz against random, mutation, and evolutionary fuzzing methods and observed up to a 81% improvement based on PAR-2 scores used in SAT competitions.

In this paper, we present MachSMT, an algorithm selection tool for state-of-the-art Satisfiability Modulo Theories (SMT) solvers. MachSMT supports the entirety of the logics within the SMT-LIB initiative. MachSMT uses machine learning to learn empirical hardness models (a mapping from SMT-LIB instances to solvers) for state-of-the-art SMT solvers to compute a ranking of which solver is most likely to solve a particular instance the fastest. We analyzed the performance of MachSMT on 102 logics/tracks of SMT-COMP 2019 and observe that it improves on competition winners in 49 logics (with up to 240% in perfor- mance for certain logics). MachSMT is clearly not a replacement for any particular SMT solver, but rather a tool that enables users to leverage the collective strength of the diverse set of algorithms implemented as part of these sophisticated solvers. Our MachSMT artifact is available at https://github.com/j29scott/MachSMT.

Satisfiability solvers can be embedded in applications to perform specific formal reasoning tasks. CBMC, for example, is a bounded model checker for C and C++ that embeds SMT and SAT solvers to check internally generated formulae. Such solvers will be solely used to evaluate the class of formulae generated by the embedding application and therefore may benefit from domain-specific parameter tuning. We propose the use of Bayesian optimisation for this purpose, which offers a principled approach to black-box optimisation within limited resources. We demonstrate its use for optimisation of the solver embedded in CBMC specifically for a collection of test harnesses in active industrial use, for which we have achieved a significant improvement over the default parameters.

This extended abstract describes work in progress on Smt-Switch, an open-source, solver-agnostic API for SMT solving. Smt-Switch provides an abstract interface, which can be implemented by different SMT solvers. Smt-Switch provides simple, uniform, and high-performance access to SMT solving for applications in areas such as automated reasoning, planning, and formal verification. The interface allows the user to create, traverse, and manipulate terms, as well as to dynamically dispatch queries to different underlying SMT solvers.