Logo
ScienceStack
Table of Contents
Fetching ...
Sign In

Overapproximation of Non-Linear Integer Arithmetic for Smart Contract Verification

Petra Hozzová, Jaroslav Bendík, Alexander Nutz, Yoav Rodeh

TL;DR

This case study focuses on the two overapproximation techniques used by the industry verification tool Certora Prover: over approximation of non-linear integer arithmetic using linear integer arithmetic and using non- linear real arithmetic.

Abstract

The need to solve non-linear arithmetic constraints presents a major obstacle to the automatic verification of smart contracts. In this case study we focus on the two overapproximation techniques used by the industry verification tool Certora Prover: overapproximation of non-linear integer arithmetic using linear integer arithmetic and using non-linear real arithmetic. We compare the performance of contemporary SMT solvers on verification conditions produced by the Certora Prover using these two approximations against the natural non-linear integer arithmetic encoding. Our evaluation shows that the use of the overapproximation methods leads to solving a significant number of new problems.

Overapproximation of Non-Linear Integer Arithmetic for Smart Contract Verification

TL;DR

This case study focuses on the two overapproximation techniques used by the industry verification tool Certora Prover: over approximation of non-linear integer arithmetic using linear integer arithmetic and using non- linear real arithmetic.

Abstract

The need to solve non-linear arithmetic constraints presents a major obstacle to the automatic verification of smart contracts. In this case study we focus on the two overapproximation techniques used by the industry verification tool Certora Prover: overapproximation of non-linear integer arithmetic using linear integer arithmetic and using non-linear real arithmetic. We compare the performance of contemporary SMT solvers on verification conditions produced by the Certora Prover using these two approximations against the natural non-linear integer arithmetic encoding. Our evaluation shows that the use of the overapproximation methods leads to solving a significant number of new problems.
Paper Structure (19 sections, 7 equations, 2 figures)

This paper contains 19 sections, 7 equations, 2 figures.

Table of Contents

  1. Introduction
  2. Contributions.
  3. Outline.
  4. Preliminaries and Example
  5. Overapproximation Methods
  6. Linear Integer Arithmetic Overapproximation
  7. Non-Linear Real Arithmetic Overapproximation
  8. Experimental Evaluation
  9. Experimental setup.
  10. Experimental results.
  11. Measuring the Overapproximation Tightness.
  12. Applications in Other Domains.
  13. Related Work
  14. Conclusions
  15. Acknowledgements.
  16. ...and 4 more sections

Figures (2)

  • Figure 1: Numbers of solved problems in the respective benchmark sets. Columns "LIA" and "NRA" refer to the benchmark overapproximations. In the parentheses is the number of problems solved in the respective overapproximated benchmark set, but not in the original NIA benchmark set. The "virtual best solver" row corresponds to the best result for each benchmark -- i.e., the numbers in this row are the counts of benchmarks solved by any solver.
  • Figure 2: Comparison of the runtimes on original and overapproximated benchmark sets. We compare runtimes for the virtual best solver -- for each problem we consider the best runtime achieved by any of the four solvers.

Theorems & Definitions (2)

  • Example 1
  • Example 2