Zesty Market recently completed an audit with Certora. Certora is a smart contract auditing company which offers a one-of-a-kind formal verification tool using Satisfiability Modulo Theories (SMT).
If you’re intimidated by Formal Verification and Satisfiability Modulo Theories (SMT). Don’t be intimidated because this post will break it down in a digestible way. If you’re already an expert in this feel free to read through and correct things.
A Gentle Introduction to Formal Verification and SMT
Motivations
If you’re not a computer science expert or a math nerd, these terms would be very foreign to you and very much meaningless. I’ll first convince you why they’re very much needed and why there’s so much work in the domain.
If you ever used a computer you would have encountered bugs. Bugs are really unexpected behaviors in a computer program. Most of the time computer bugs are more of an annoyance that can be usually fixed by restarting the computer. However, sometimes bugs can be a result of some unknown function in a shoddily created program.
Usually, bugs are tolerated, hence ‘move fast, and break things’ is an accepted principle because bug fixes can be easily pushed. Unfortunately, not all systems can be easily fixed with bug fixes. Airplane hardware, electronics, and smart contracts are pretty much set in stone once they have been launched or manufactured (there are proxy patterns for smart contracts, but we’ll leave that for another discussion). How can you try your best to ensure that the programs work as intended? Software engineers have to literally expect the unexpected, this seems to be a fairly impossible task. What can we do about it?
Nobody expects the Spanish Inquistion
Expecting the Unexpected
The first approach is peer review. You essentially get a bunch of experts to look at your code and give you the *thumbs up*. This is the main approach taken by most projects and auditing firms. However, the time constraints and limits on human cognition can make it hard to find all possible issues. This can sometimes lead to epic hacks that make engineers sleep deprived and users sad because they lost their money :(
The second approach is to rigorously test a system with unit tests and integration tests. This is an important step. Proper unit tests and integration tests can at least guarantee that the system would function correctly in a sanitized environment. Sadly, it can be hard and very time consuming to thoroughly test an entire system. Unknown edge cases can be very tricky to spot.
The third approach is to have some kind of automated system to catch bugs before they emerge. Some techniques in this field includes fuzzing and formal verification techniques. Formal verification include interactive proofs with programs Coq, and SMT proofs with programs like Z3. The general idea behind these techniques is to find some kind of unifying principle or theorem behind the correct functioning of a system and then checking if the theorem holds. This is more rigorous, but again the theorems and specifications are still human made so it’s possible to miss things out. However, that being said, it is likely the stronger guarantee among the previous two approaches.
The practical approach is a combination of peer review, unit test, and computer verification. Really, the more the merrier, systems get safer the more they are verified and tested.
Understanding Formal Verification and Satisfiability Modulo Theories
For this discussion, we’ll focus more on a specific approach which is Formal Verification with Satisfiable Modulo Theories (SMT). This is the approach taken by Zesty Market. Peer review was done by specifying theorems or invariants and reasoning about in rigorous mathematical way. In addition, unit tests were used. That being said, there may still be gaps that we might have missed. As such, we’re in the process of setting up a bug bounty program with Immunefi.
In this writing, we’ll introduce the topic in a practical way and would avoid too much theoretical treatment. Details may be glossed over, should they be of interest do refer to the wide selection of textbooks and papers in the field.
Before we dive into SMT, we need to understand what exactly is Formal Verification about. Formal Verification is the process of figuring out whether a system you made satisfies the specification that it was designed for. Usually for most programming work, the specifications are drawn/written in the form of some Unified Modeling Language (UML) diagram.
While this is intelligible to humans, it’s not necessarily intelligible for a computer. We need to figure out to turn human readable business logic into some form of mathematical model so that the business logic is also machine readable.
Brute-Force Approach with Model Checking
To gain an intuition behind more elaborate formal verification techniques, we’ll start with understanding model checking.
If the model is simple enough, you can exhaustively list down all the states and test all the state transitions. This process is known as model checking. Such simple models are known as finite models, and finite state machines are a kind of finite model. An example of a finite state machine is a coin operated turnstile.
With such a model available, we can pose the question: Does the machine only goes into the unlocked state when you push a coin?
This is the motivation behind the model checking approach: Does model, M, satisfy a property, P.
In this example, it’s is pretty trivial to humans to know this property is true by observing the diagram alone. However, to make this intelligible to a computer for it to check, we need to define this mathematically. We can then describe this model as follows:
- States: Locked, Unlocked
- Initial State: Locked
- Paths, or transition relations:
Locked to Unlocked
Unlocked to Locked - Labeling function, this is the set of atomic proposition, AP, atomic propositions are boolean expressions over variables, such that States → 2^AP:
Locked to Unlocked with Coin, (Locked, {Coin})
Unlocked to Locked with Push (Unlocked, {Push})
This is known as as a Kripke structure, defined in the model checking textbook, as well as in this paper. if you’re familiar with Finite State Machines, you would realize that the Kripke structure is a variant of a Moore machine (if this is unintelligible, carry on, it’s just an FYI).
To check for the validity of the properties, we can then enumerate various execution paths computationally using a computation tree, and check if the property, “Does the machine only goes into the unlocked state when you push a coin?”, is violated. A number of techniques are possible, Computational Tree Logic, and Automata language acceptance approaches are usually used. We’ll avoid discussing further details about this here.
Vardi and Worper’s Automata-theoretic techniques for modal logics of programs is a useful resource in understanding the Automata theory approach.
Most programmers would have knowingly or unknowingly essentially do a form of manual model checking through unit testing. So for simple enough systems, a dedicated program might not be required to verify a system. While simplistic, this has been a very effective technique for embedded systems.
This is all and well for simple models. Unfortunately, life isn’t simple. Many systems of interest in our world can be really complex. State explosion can happen regularly and simplifications might not always be feasible. Life is hard, oof.
Life is hard, oof. (Jseam, 2021)
We need a better approach to approach more complex systems with more expressivity.
Deductive Verification with SMT
Smart contracts are complex systems where the execution environment, libraries, and contract code are relevant to the functioning of the contract itself. While the smart contract may be a simple state machine, external library calls and bugs within the Solidity compiler itself can make it really difficult to ascertain the correct functioning of the code. External contract calls introduce even more vectors that can be really hard to account for. This can easily lead to the state explosion that model checking cannot easily handle.
In order to deal with state explosion we need a more expressive way of figuring things out and checking the logic of things. One possible way is through designing mathematical proofs and checking those proofs with the computer. This way we have a very expressive way of describing and testing the function. The approach to doing so is pretty ingenious. We have two ingredients:
- Mathematical proofs can be expressed with first-order logic (or predicate logic)
We’ll gloss over details about first-order logic. It is an extension of propositional logic which deals with true or false things. An propositional logic statement would be something like, “this is an article”. First-order logic includes predicates and quantifiers allow for more expressivity. This is the basis for mathematical proofs. For example, “all natural numbers have a successor”. This can be expressed as (∀x)(x != 0 ⊃ (∃y)(Sy = x)), where S is the successor function and 0 is not a natural number. This is an example of an axiom as it is irreducible and a mathematical fact we have to accept for subsequent proofs to make sense.
2. Computers can check whether a boolean expression is satisfiable by solving the SAT problem
The SAT (Satisfiability) problem is a problem of figuring out whether a Boolean formula evaluates to true. For example, given this Boolean formula find the set of assignment that evaluates to true.
(¬x ∨ y) ∧(¬y ∨ z) ∧(¬z ∨ y) = ??
If we put x = False, y = True, z = True, the Boolean formula evaluates to True, so it is satisfiable.
While the SAT problem is a NP-complete problem (easy to check, but hard to find a solution for), there are scalable approaches to solve it, one notable algorithm is the DPLL Algorithm which relies on backtracking to solve the equation. Variants of the DPLL Algorithm is the basis for SAT solvers which are part of SMT solvers.
As the problem is in NP, it’s not always feasible to solve if there are too many variables. We also cannot check undecidable problems, like the halting problem. However, in most practical cases this is not a concern.
While not perfect, this approach is generally more scalable than brute force search with model checking approaches.
Combining the 2 ingredients
The idea behind a SMT solver is to be able to express our verification specifications in an expressive first-order logic form, which can be then converted by a computer program into a SAT problem. This would allow us to have a computer check if the specifications match how a program actually functions. One notable SMT solver is the Z3 solver (see the paper for details). Note the Certora solver is proprietary but we can presume that it works similarly to the Z3 solver except that it’s optimized for EVM bytecode and an EVM execution environment.
The Z3 solver is a practical implementation that combines the 2 ingredients mentioned above. First, it processes code into the Simplifier which simplifies human written code using algebraic reductions. Once that’s done the Compiler parses code into an abstract syntax tree and converts it into a set of clauses and congruence-closure nodes. With this form it can be fed into the Congruence closure core which interacts with the SAT solver, Theory Solver, and E-matching engine. This allows the solver to then evaluate specifications regarding properties of a given system, to see if any property is violated or if no property is violated and the system functions correctly.
With that we’ll move onto a practical example with the contracts used by Zesty Market.
Tutorial on Specification Writing with Zesty Market Contracts
To write the specification for Zesty Market, we’ll first understand the business logic behind the Zesty Market V1 and Zesty Space NFT contract.
Business Logic of Zesty Market V1
Zesty Market is a decentralized peer-to-peer market for the rental of digital spaces. Digital spaces at the moment include websites, games, streams. Such spaces can be used for advertising, building portals, sharing art, and for sharing memes.
Users can mint a Zesty Space NFT, tokenizing a space into an NFT. After which, a user can deposit that NFT in to the Zesty Market V1 contract to rent time slots on the Space NFT. The pricing of the time slots are decided using a Dutch Auction, where prices start high and end low (prices terminate at 0, since an expired time slot would be valueless). The final price is the price of the first bidder paid.
A buyer would create a campaign with some desired metadata and bid on the auction, locking the bid.
Should a seller reject the bid. in the case the seller dislikes the campaign, the buyer would be refunded (excluding a small tax to disincentivize repeated malicious bidding to DDoS the timeslot, this tax will be given to the Zesty DAO for redistribution back to the community). The auction will still proceed with the original price decay schedule until another buyer buys the time slot.
Should a seller accept the bid, an agreement contract is made between the buyer and seller (this is a struct entry not a new contract deployment, sorry for confusing terminology). As there may be a delay between the time the buyer bids and seller approves, the contract would refund the buyer the time difference based on the Dutch Auction price decay. This refund is needed suppose if the seller approves at the last minute and withdraws funds without completing the contract. After the contract concludes, the seller will be able to withdraw funds from the Zesty Market contract. The Zesty Space NFT now has an on-chain record of income that had passed through it which can be used for future valuation.
The code for the Zesty Market Contracts can be found in our repo. More rules on specification writing can be found in the /specs folder in the repo.
Specification Writing with Certora
Do take note to follow the steps, you will need to request a demo key from Certora.
The contract we’ll be focusing on for this tutorial would be the ZestyMarket_ERC20_V1_1.sol contract. This is they key smart contract used by Zesty Market at the current moment. We’ll outline the thought process and key steps when designing the specification, v1.spec
For this tutorial, we will want to focus on a simple rule. We will check whether the Dutch auction price decay property will always hold. We’ll call this rule sellerAuctionPriceMonotonicallyDecreasingInTime . A monotonic function is always non-increasing and non-decreasing, this means there can be plateaus. We expect the price decay to be a linear function with a negative gradient, hence it is non-increasing.
Harnesses
Before writing specifications for the contract we need to have an easy way of referencing contract state. For that, we’ll create a harness for the market contract. To do so, create a harness contract that inherits the market contract and expose state variables as so. V1Harness.sol. Essentially, what the harness contract does is to expose getter functions to return a single value. This helps with testing.
pragma solidity ^0.7.6;
import "../../contracts/market/ZestyMarket_ERC20_V1_1.sol";
contract V1Harness is ZestyMarket_ERC20_V1_1 {
constructor(
address txTokenAddress_,
address zestyNFTAddress_,
address owner_
)
ZestyMarket_ERC20_V1_1(txTokenAddress_, zestyNFTAddress_, owner_)
{
}
function getAuctionPricePending(uint256 id) external view returns (uint256) {
uint256 ret;
(, , , , , , , ret, , , ) = ZestyMarket_ERC20_V1_1(this).getSellerAuction(id);
return ret;
}
...
}In the case of the Zesty Market contract, we included an additional script to modify the contract code for easier testing. This is found under specs/scripts/applyHarness.sh. It’s a simple perl script that comments out events, creates a mapping for the price function for tests that don’t need the full compute, and renames the original getSellerAuctionPrice to getSellerAuctionPriceOriginal. We’ll be focusing on the getSellerAuctionPriceOriginal for the rest of the tutorial.
Before developing specifications with Certora’s specs, do download the extension on Visual Studio Code for syntax highlighting. We’ll discuss key parts of the specification file.
Imports
At the top of the specification file you can import other smart contracts on top of the current contract you’re writing specifications for as such.
using DummyERC20A as token
using ZestyNFT as nftMethod Declarations
You can then specify method declarations, the primary use case for Zesty Market specifications is to make those selected methods envfree as those methods are non-payable and does not need to access the EVM execution environment. The EVM execution environment contains things like block.timestamp , msg.sender . We do not need to access these variables for some functions.
methods {
getDepositor(uint256) returns (address) envfree
getOperator(address) returns (address) envfree
getTxTokenAddress() returns (address) envfree...
}
Ghosts and Hooks
You can specify ghosts and hooks to access contract state. Ghosts are uninterpreted functions, but when you combine them with hooks you are able to access contract state that is not explicitly callable from the contract, these could be private values. For example, _txToken is a private value in our contract, we have made this private as a safeguard in case a future dev inherits the market contract and accidentally overwrites the _txToken value causing token balances to be recorded wrongly.
ghost txToken() returns address;hook Sload address v _txToken STORAGE {
require txToken() == v;
}hook Sstore _txToken address v STORAGE {
havoc txToken assuming txToken@new() == v;
}
Rules and Invariants
We can now look at implementing rules. Rule writing and writing unit test cases are largely similar except you can be more expressive with properties with rules.
In the case of sellerAuctionPriceMonotonicallyDecreasingInTime we actually don’t need the methods and ghosts section as mentioned above. For this rule we want to ensure that some before price is always greater than some after price after some elapsed time. Note that this is being solved symbolically and not through exhaustive enumeration with model checking mentioned above. As such we can write the following rule.
rule sellerAuctionPriceMonotonicallyDecreasingInTime(uint auctionId) {
env e1; // any evm environment
env e2; // any evm environment // ensure that e1 time <= e2 time
require e1.block.timestamp <= e2.block.timestamp; // get price of seller auction for respective env
uint before = getSellerAuctionPriceOriginal(e1, auctionId);
uint after = getSellerAuctionPriceOriginal(e2, auctionId); // price before must be equal or greater than after
// for monotonicity to be true assert before >= after;
}
If you have seen the v1.spec file, you’d see invariant along side with rule . The invariant keyword is a shorthand for an invariant as a rule.
Checking Specifications
Once we have all the necessary steps completed, we can begin to run the solver. The Certora solver works on the EVM bytecode level, so we’ll need to have the appropriate solc version in your computer to compile solidity to EVM bytecode. solc-select is a useful tool for selecting between solc versions on your computer. Follow the necessary instructions and switch to the appropriate solidity version. In our case, we are using solidity version0.7.6 .
Once installed, it is as easy as running.
$ solc-select install 0.7.6
$ solc-select use 0.7.6With that you can run v1Rule.sh. The reason we want to test rules individually is because the entire specification suite can take a very long time to run. As a reference. the whole ZestyMarket_ERC20_V1 specification suite can take between 1 hour to 2 hours to run. In the root of the repository run ./specs/scripts/v1Rule.sh sellerAuctionPriceMonotonicallyDecreasingInTime
// in ./specs/v1Rule.sh
certoraRun specs/harness/V1Harness.sol contracts/market/ZestyNFT.sol specs/harness/DummyERC20A.sol specs/harness/DummyERC721Receiver.sol \--link V1Harness:_txToken=DummyERC20A \--link V1Harness:_zestyNFT=ZestyNFT \--verify V1Harness:specs/market/v1.spec \--optimistic_loop --loop_iter 2 \--rule $1 \--cache zesty \--msg "Market V1 $1 $2"
The solver will then tell you whether the rule holds or not. If it doesn’t there’s a bug somewhere in the code. You can try a sample under the demo provided by Certora. The result would look something like this if there’s a bug. There are other rules and invariants specified in the specification file which would be too much to cover in the medium post. Feel free to checkout the specifications and the Zesty Market contract and see if there are any issues.
More documentation regarding Certora specification writing can be found here.
Conclusion
The formal verification specifications were really useful and helped to uncover critical issues in the original code. See the formal verification report for more insight on the issues.
Given the precautions taken, the specifications themselves may not be perfect and there could be oversights despite the effort taken. See thread on Sushi’s MISO vulnerability. As such, Zesty will be looking towards additional audits and bounties in future to harden the system.
I hope this article helped shared light about applying formal methods and formal verification in a practical way to smart contracts. Formal Verification is still an active field of research and a rather interesting one.
If you want to talk to me, JSeam, about smart contract development, general computer science topics, and random things, feel free to hop onto Zesty Market’s Discord and ping me.
