Easily Solving Hard SMT Queries

A wide range of practical problems can easily be solved by SMT solvers such as z3, cvc5, and STP. The idea is to write out the problem as a system of equations and let the solver automatically find a solution (or prove that no solution exists). Amazon Web Services is currently solving a billion SMT queries per day.

I pioneered the use of these solvers for the differential cryptanalysis of hash functions such as MD5 and SHA-1 in my Master’s thesis in 2008 and for Addition-Rotation-XOR (ARX) ciphers in 2013. This approach has since become one of the standard techniques in symmetric-key cryptanalysis and design, as explained in the first chapter of any good book on the subject.

In this blog post, I’ll look into hard SMT queries that appear in program verification, and explain how to solve them instantly. More specifically, I’ll look into the SPARK Lemma Library which contains a set of manual proofs using Coq for hard SMT queries.

In this post, I’m limiting myself to only the queries involving integer arithmetic. Also, I’ve simplified the queries (which were generated by GNATprove using Why3) to avoid getting lost in the details. For any questions or comments, free to send me an email:

Adding a Preprocessing Pass

Let’s start with Lemma_Mult_Then_Mod_Is_Zero. The goal is to prove that a × b mod b = 0. We assume b ≠ 0. To ensure that a × b doesn’t overflow, we also assume that a ≤ (2³²-1)/b, where 2³²-1 (which is #xFFFFFFFF in hexadecimal) is the largest value for an unsigned 32-bit integer.

A small technicality: by putting not before the statement to prove, an unsat (unsatisfiable) answer proves that there is no counterexample and therefore it is proven that the statement holds for all a and b.

Feel free to copy-paste this query into the online cvc5 solver:

(set-logic QF_BV)
(set-option :solve-bv-as-int sum)
(set-option :output post-asserts)
(declare-const a (_ BitVec 32))
(declare-const b (_ BitVec 32))
(assert (not (= b #x00000000)))
(assert (bvule a (bvudiv #xFFFFFFFF b)))
(assert (not (= (bvurem (bvmul a b) b) #x00000000)))
(check-sat)

Without the two lines in bold, the solver times out. Alex Ozdemir of the cvc5 team suggested that I use the solve-bv-as-int preprocessing pass to solve this type of query instantly. The post-asserts output option can be used to see the result of the preprocessing pass. (Without going into the details, I’d like to point out that this preprocessing pass is always complete and sound, meaning it doesn’t add or remove any solutions.)

Note that there’s no need to use cvc5 here, the output of the preprocessing pass can be solved by z3 as well. The preprocessing pass introduces integers (as its name implies), which are not supported by STP. If anyone knows how to solve this SMT query with STP, thanks for letting me know!

Using Built-In Functions

Let’s continue with Lemma_Mult_Then_Div_Is_Ident. Its goal is to prove that (a × b) / b = a:

(set-logic UFNIA)

(define-fun abs1 ((x Int)) Int (ite (<= 0 x) x (- x)))
(declare-fun div1 (Int Int) Int)
(declare-fun mod1 (Int Int) Int)

;; Div_mod
  (assert
  (forall ((x Int) (y Int))
  (=> (not (= y 0)) (= x (+ (* y (div1 x y)) (mod1 x y))))))

;; Div_bound
  (assert
  (forall ((x Int) (y Int))
  (=> (and (<= 0 x) (< 0 y)) (and (<= 0 (div1 x y)) (<= (div1 x y) x)))))

;; Mod_bound
  (assert
  (forall ((x Int) (y Int))
  (=> (not (= y 0))
  (and (< (- (abs1 y)) (mod1 x y)) (< (mod1 x y) (abs1 y))))))

;; Rounds_toward_zero
  (assert
  (forall ((x Int) (y Int))
  (=> (not (= y 0)) (<= (abs1 (* (div1 x y) y)) (abs1 x)))))

(declare-const a Int)
(declare-const b Int)

(define-fun in_range ((x Int)) Bool (and (<= (- 9223372036854775808) x)
                                    (<= x 9223372036854775807)))
(define-fun in_range1 ((x Int)) Bool (and (<= 1 x)
                                     (<= x 9223372036854775807)))

(assert (not (=> (in_range a)
             (=> (in_range1 b)
             (= (div1 (* a b) b) a)))))
(check-sat)

I’ve removed a lot of the asserts for readability. However, I’ve kept the (unnecessary) Rounds_toward_zero just to thwart cvc5 from outputting unsat immediately. Indeed, a well-known strategy for proof finding is to remove assertions (i.e., remove bounds). This results in an over-approximation of the query (which means unsat answers can be trusted, but sat answers can’t).

But removing Rounds_toward_zero isn’t sufficient for z3 to solve this. Instead, I would argue that the Why3 driver formulates this query in a strange way. Why would the SMT solver know about integers, addition, and multiplication, but not about div, mod, and abs? These functions are also part of the SMT-LIB Int theory!

So instead, let’s just replace the last div1 (shown in bold) by div. This approach allows us to solve this query (and several others) instantly with cvc5 or z3.

Using Mathematical Induction

With the previous two approaches, only one (integer arithmetic) lemma in the SPARK Lemma Library can’t be solved instantly by cvc5 or z3.

The lemma is Lemma_Exp_Is_Monotonic, and is defined as follows: for natural numbers n, a, and b, we have a ≤ b implies aⁿ ≤ bⁿ.

To solve this one instantly, here’s what I came up with (using the z3 API in Python):

from z3 import *

def inductionNat(f):
    n = FreshInt()
    return And(f(IntVal(0)), ForAll([n], Implies(And(n > 0, f(n)),  f(n+1))))

s = Solver()
a, b, x, n, m, p, q = Ints('a b x n m p q')
power = Function('power', IntSort(), IntSort(), IntSort())
mul = Function('mul', IntSort(), IntSort(), IntSort())

# ;; Power_0
#   (assert (forall ((x Int)) (= (power x 0) 1)))
s.add(ForAll([x], power(x,0) == 1))

# ;; Power_s_alt
#   (assert
#   (forall ((x Int) (n Int))
#   (=> (< 0 n) (= (power x n) (* x (power x (- n 1)))))))
s.add(ForAll([x,n], Implies(0<n, power(x,n) == mul(x,power(x,n-1)))))

# ;; Power_non_neg
#   (assert
#   (forall ((x Int) (y Int)) (=> (and (<= 0 x) (<= 0 y)) (<= 0 (power x y)))))
s.add(ForAll([x,n], 0 <= power(x,n)))

# Theorem mul_le_mono_nonneg :
#    forall n m p q, 0 <= n -> n <= m -> 0 <= p -> p <= q -> n * p <= m * q.
s.add(ForAll([n,m,p,q], Implies(0<=n, Implies(n<=m, Implies(0<=p, Implies(p<=q, mul(n,p)<=mul(m,q)))))))

s.add(a >= 0);
s.add(b >= 0);

claim = inductionNat(lambda n : Implies(a <= b, power(a,n) <= power(b,n)))
#claim = ForAll([n], Implies(n >= 0,  Implies(a <= b, power(a,n) <= power(b,n))))
s.add(Not(claim))

print(s.to_smt2())
print(s.check())

The original query (generated by Why3) has been simplified a bit, and modified in three ways:

First, I replaced the multiplication * by the uninterpreted function mul. (Why3 already provided the power uninterpreted function and several lemmas related to it.)
Second, I didn’t need to define mul, but I needed to add one lemma about multiplication: mul_le_mono_nonneg.
Third, the inductionNat function by Philip Zucker overcomes the limitation of cvc5 and z3 to figure out the mathematical induction automatically. (To see this, note that removing the # in the bold line results in a timeout.)

That’s all for this blog post! If you know any other short SMT queries (not involving floating-point arithmetic) that are difficult to solve, thanks for letting me know:

Easily Solving Hard SMT Queries