template: post
title: “Fuzzers vs. SMT Solvers - What’s the Difference?”
slug: how-to-setup-solidity-linters
draft: true
date: 2021-07-26T10:30:47.348Z
description: “Wondering what the differences between Fuzzers and SMT solvers are? I’ll cover it here.”
category: Solidity
tags:

Solidity

fuzzers

SMT

smart contract security

security

smart contract

When examining ways of testing smart contracts for security audits, there are two tools that I will explore today. One is fuzz testers. The other are SMT solvers. Both are used in smart contract security auditing tools, such as symbolic analyzers Oyente and Mythril, however they have different uses.

Fuzzers

“A fuzz tester (or fuzzer) is a tool that iteratively and randomly generates inputs with which it tests a target program” (Klees, Ruef, Cooper, Wei, and Hicks 2018). There are white-box fuzzers, black-box fuzzers and gray-box fuzzers. White-box fuzzers…

Black-box fuzzers…

Gray-box fuzzers…

In smart contract engineering, “Harvey” is an example of a gray-box fuzzer (Wustholz & Christakis 2020).

“Harvey” does XYZ…

SMT Solvers

Satisfiability modulo theories (SMT) solvers solve for logical contraints. “SMT solvers are capable of automatically determining whether logical formulas such as the one shown earlier are satisfiable, that is whether there exists an assignment to the variables that simultaneously satisfy all of the contraints. If so, the solver produces a model assigning each of the variables to a concrete value. Otherwise, the solver returns a proof that the formula is unsatisfiable, that is, it is impossible to assign all variables in a way that satisfies all constraints.” SMT solvers form the backbone of many symbolic analyzers, such as Z3 (Quantstamp 2019).

Differences between Gray-Box Fuzzers and SMT Solvers