Exploring Solidity’s Model Checker

Exploring Solidity’s Model Checker
May 13, 2020 13 mins

Exploring Solidity’s Model Checker

Exploring Solidity’s Model Checker

This blog post aims to be an exploration of how Solidity’s model checker works, how it can be utilized to find certain types of bugs, and its current limitations.

Model checking is a method of formally verifying whether a model of a system meets a specification. Modern model checkers can determine whether certain security properties hold true for a given program, and can automate the discovery of memory corruption bugs, unsafe arithmetic, assertion failures, and more. When a property is not found to hold, a model checker produces a counterexample that acts as a proof of its contradiction.

While working with our clients to test the security of high assurance software, such as smart contracts that transact valuable digital assets, we often find ourselves seeking a high level of confidence in a program’s correctness. A model checker is one type of tool with the potential of delivering this level of confidence when used effectively. Furthermore, the security properties we formulate can be later used by our clients to perform their own formal verification even after an engagement has ended. Many of these companies would not otherwise use formal methods due to their reputation of having steep learning curves and being highly academic.

This is why we are excited to see the development of a model checker within the Solidity compiler itself. Solidity is the predominant programming language for the Ethereum Virtual Machine (EVM), and is what many widely used smart contracts today are written in. While there are already several formal verification tools that support Solidity and/or the EVM, our hope is that having a model checker built directly into Solidity will make formal methods more accessible to developers. In addition, specifications are written inline using the Solidity language itself. This means that while there is some extra work involved in writing a specification, it does not come with the usual overhead of having to install a new tool and learn a new language.

At the time of writing this, Solidity’s model checker is still very much a work in progress, and we cannot yet recommend its sole use as a formal verification tool. However, a quick look at the Solidity GitHub repository shows promising and active development (http://github.com/ethereum/solidity/tree/develop/libsolidity/formal). In addition, one of its authors has demonstrated that it can find real bugs (https://medium.com/@leonardoalt/soliditys-smtchecker-can-automatically-find-real-bugs-beb566c24dea). This blog post aims to be an exploration of how Solidity’s model checker works, how it can be utilized to find certain types of bugs, and its current limitations.

Solidity Model Checking 101

As stated, model checking is a method for formally verifying whether a model of a system meets a specification. In order to do this, Solidity’s model checker takes source code and encodes the parts it wants to reason about as SMT2, which is a language for SMT (satisfiability modulo theories) solvers. An SMT solver’s job is to take a system of constraints and determine whether a model exists. For example, a system containing the single constraint X > 3 has a model X = 7. However, a system containing the constraints X > 5 and X * 2 < 10 has no model. A popular SMT solver supported by Solidity is Microsoft’s Z3, which offers a good balance between performance and feature support.

The following graphic illustrates a simplified, high-level version of Solidity’s model checker process:

A sound model checker can do this type of encoding task without losing necessary information that could lead to false negatives (or if this is unavoidable, it emits warnings), while a complete model checker can do this encoding task without making generalizations that could lead to false positives. Solidity’s model checker is currently known to be sound but incomplete, while emitting warnings about unsupported language features (e.g., inline assembly). This means that the tool shouldn’t miss any bugs without warning you that it cannot reason about something, though it may also produce false positives which will need to be sorted through.

Bounded Model Checking

As it turns out, Solidity currently has two model checker engines that specialize in different uses of a backend SMT solver. The original one, a bounded model checker (BMC), is a relatively simple algorithm that analyzes Solidity functions in isolation. When encoding a Solidity source unit into SMT2, the checker navigates the unit’s abstract syntax tree (AST) and compiles a list of symbolic variables and constraints for each contract and function. Solidity’s built-in require function is used to declare assumptions made within the specification, while the built-in assert function is used to declare its verification targets (which may or may not have a possible model). Other AST nodes are used to determine the unit’s implementation.

The following example demonstrates that proving assertions that are local to a single basic function are straightforward. Note the use of the experimental SMTChecker pragma to enable the model checker.

pragma solidity >=0.5.0;
pragma experimental SMTChecker;

contract C {
  function b(uint256 x) pure public {
    require(x < 250 && x >= 10);

    uint256 y = x * 2;
    uint256 z = y - 15;

    assert(z > 5);
  }
}


Warning: Assertion violation happens here
  --> example1.sol:11:5:
   |
11 |     assert(z > 5);
   |     ^^^^^^^^^^^^^
Note:   for:
  x = 10
  y = 20
  z = 5

Note: Callstack:
Note:

Solidity’s BMC also contains several built-in checks for language-specific issues like integer underflows, integer overflows, division by zero, and insufficient funds on transfer. These types of built-in checks are exciting to see because they are provided “for free” and require virtually no effort to use.

The following example demonstrates this by having the BMC detect a more subtle and realistic bug, which can be exploited by an attacker to grant themselves unlimited tokens (hint: Consider the result of amount – fee(amount) when amount is zero):

pragma solidity >=0.5.0;
pragma experimental SMTChecker;

contract TransferWithFees {
  address operator;
  mapping (address => uint256) public balances;

  constructor() public {
    operator = msg.sender;
  }

  function transfer(address to, uint256 amount) public {
    require(balances[msg.sender] >= amount, "Insufficient funds");
    balances[msg.sender] -= amount;
    balances[to] = safeAdd(balances[to], amount - fee(amount));
    balances[operator] = safeAdd(balances[operator], fee(amount));
  }

  function fee(uint256 amount) internal pure returns(uint256) {
    if(amount >= 1 ether) {
      return 1 ether / 10000;
    } if(amount >= 1 ether / 2) {
      return 1 ether / 5000;
    } else {
      return 1 ether / 1000;
    }
  }

  function safeAdd(uint256 a, uint256 b) internal pure returns(uint256) {
    uint256 c = a + b;
    require(c >= a, "Overflow on add");
    return c;
  }
}


Warning: Underflow (resulting value less than 0) happens here
  --> example2.sol:15:42:
   |
15 |     balances[to] = safeAdd(balances[to], amount - fee(amount));
   |                                          ^^^^^^^^^^^^^^^^^^^^
Note:   for:
   = 0x038d7eA4C68000
   = (- 1000000000000000)
  amount = 0
  balances[msg.sender] = 0xFFFFffffFFFFffffFFFFffffFFFFffffFFFFffffFFFFffffFFFFffffFFFFf8fb
  balances[to] = 0
  msg.sender = 8366
  operator = 8367
  to = 8365

Note: Callstack:
Note:

Unfortunately, this type of model checker is not without its limitations. As implied by its name, a bounded model checker can only analyze a finite number of program steps. This approach isn’t usually an issue for functions without loops. Consider that for if statements and Boolean operators, the model checker only needs to evaluate one extra path of execution. It asks the backend SMT solver to try finding a model for one version where the conditional returns true and another version where it returns false. However, with loops the model checker must also account for any number of loop iterations and the extra paths associated with them, which may become huge. This problem exists for virtually all Turing-complete languages and we call it state blowup.

To mitigate state blowup, Solidity’s model checker currently only considers one iteration of a loop. This approach alone would lead to unsoundness, so variables that were “touched” in the body of a loop have their knowledge of side effects erased and a warning is emitted. This leads to some obvious false positives such as the following:

pragma solidity >=0.5.0;
pragma experimental SMTChecker;

contract C {
  function count() public pure returns(uint256) {
    uint256 y = 0;

    for(uint256 i = 0; i < 5; i++) {
      y += y; // Effectively a NOP since y is always 0, but y is touched so the model checker erases knowledge.
    }
    return y;
  }
}


Warning: Overflow (resulting value larger than 2**256 - 1) happens here
 --> example3.sol:9:7:
  |
9 |       y += y; // Effectively a NOP since y is always 0, but y is touched so the model checker erases knowledge.
  |       ^^^^^^
Note:   for:
   = 0
   = 2**256
  i = 0
  y = 0x80 * 2**248

Note: Callstack:
Note:
Note that some information is erased after the execution of loops.
You can re-introduce information using require().

Just as the warning explains, lost information can always be reintroduced using assumptions via require. While this can be helpful in some situations, it is often infeasible to work around this limitation without avoiding loops all together. How do other BMCs handle this issue?

Traditional BMCs take some integer k that acts as the upper bound of how many steps of executions to consider. When k is set to the minimal number of steps required to reach all program states (referred to as a program’s reachability diameter), soundness holds. The issue is that if k is set too high, the state blowup can quickly become intractable for complex programs. This is especially true when one considers contract interaction to be its own type of loop: While Solidity’s BMC only considers one function in isolation, an attacker is free to make zero or more calls to any of a contract’s public functions. A bug may not be found until a certain number of function calls are made in some particular order.

The inherit limitations of the bounded model checker have led to the recent introduction of a second type of model checker engine within Solidity that uses something called Constrained Horn Clauses.

Constrained Horn Clauses

When a SMT solver wants to efficiently reason about loops, it must have a way to efficiently reason about reachability. This becomes more apparent when we think of loops as recursive functions and ask if one program state may ever reach another. One way for an SMT solver to tackle this problem is by using Constrained Horn Clauses (CHCs) and Property Directed Reachability (PDR). CHCs are first-order logic formulas that are capable of encoding meaningful information about whether one program state is reachable from another. PDR is a relatively new type of incremental model checking algorithm that breaks the problem down into smaller subproblems called cubes, which can make it more tractable to analyze loops. Z3, as used by Solidity, incorporates both CHCs and PDR to more efficiently solve this otherwise intractable type of problem.

Just like the BMC, the CHC engine encodes a Solidity source unit into SMT2 by navigating the unit’s AST and compiling a list of symbolic variables and constraints. However, this time it navigates the unit and considers all possible paths of execution each contract can take. The CHC engine does this by attempting to synthesize the correct Horn clauses that accurately model these paths as logical relationships with constraints (which may or may not be recursive) between blocks of code. Z3 can then be asked to solve queries about these constrained logical relationships.

Consider the following button pressing puzzle as an example. Note that the CHC engine is able to quickly reason about the implications of calling each public function and evaluate if a model exists for not solving the puzzle. An assertion failure in is_not_solved would imply that the puzzle is solvable:

pragma solidity >=0.5.0;
pragma experimental SMTChecker;

contract C {
  bool a;
  bool b;
  bool c;
  bool d;
  bool e;
  bool f;

  function pressA() public {
    if(e) { a = true; } else { reset(); }
  }

  function pressB() public {
    if(c) { b = true; } else { reset(); }
  }

  function pressC() public {
    if(a) { c = true; } else { reset(); }
  }

  function pressD() public {
    d = true;
  }

  function pressE() public {
    if(d) { e = true; } else { reset(); }
  }

  function pressF() public {
    if(b) { f = true; } else { reset(); }
  }

  function is_not_solved() view public {
    assert(!f);
  }

  function reset() internal {
    a = false;
    b = false;
    c = false;
    d = false;
    e = false;
    f = false;
  }
}


Warning: Assertion violation happens here
  --> example4.sol:37:5:
   |
37 |     assert(!f);
   |     ^^^^^^^^^^
Note:   for:
  f = true

Note: Callstack:
Note:

While Solidity’s model checker doesn’t display the chain of independent function calls that led to a counterexample, it does guarantee that such a chain exists (as implied by f being set to true). It would be nice to see this type of information returned in future versions of the model checker.

Unfortunately, at the time of writing this it was too difficult to produce a more realistic example. This was largely due to an incompleteness of more complex types such as mappings when the CHC engine was used (e.g., see https://github.com/ethereum/solidity/issues/8688). A bug was also discovered that impacted the CHC engine’s ability to properly handle contract inheritance (https://github.com/ethereum/solidity/issues/8623). While the solver remains powerful, getting Solidity’s model checker closer to completeness is a challenging endeavor that will likely take some time.

Conclusion

Although Solidity’s model checker is very much a work in progress, we think that it is a tool with great potential. It is especially exciting to see built-in checks for language-specific issues like integer underflows, integer overflows, division by zero, and insufficient funds on transfer. This makes this tool already valuable, although incompleteness can lead to more false positives to sort through. We’d love to see this list extended to include other types of common bugs such as unsafe reentrancy, unsafe timestamp dependence, and denial of service. It is also exciting to see Solidity’s model checker make use of relatively new advances in model checking technology such as PDR. Although this feature is still in a very early phase of development, it could one day be used to detect more complex bugs.

We look forward to seeing this tool be developed further.

Author:
  • Eric Rafaloff

About Cyber Solutions:

Cyber security services are offered by Stroz Friedberg Inc., its subsidiaries and affiliates. Stroz Friedberg is part of Aon’s Cyber Solutions which offers holistic cyber risk management, unsurpassed investigative skills, and proprietary technologies to help clients uncover and quantify cyber risks, protect critical assets, and recover from cyber incidents.

General Disclaimer

This material has been prepared for informational purposes only and should not be relied on for any other purpose. You should consult with your own professional advisors or IT specialists before implementing any recommendation, following any of the steps or guidance provided herein. Although we endeavor to provide accurate and timely information and use sources that we consider reliable, there can be no guarantee that such information is accurate as of the date it is received or that it will continue to be accurate in the future.

Terms of Use

The contents herein may not be reproduced, reused, reprinted or redistributed without the expressed written consent of Aon, unless otherwise authorized by Aon. To use information contained herein, please write to our team.

Aon's Better Being Podcast

Our Better Being podcast series, hosted by Aon Chief Wellbeing Officer Rachel Fellowes, explores wellbeing strategies and resilience. This season we cover human sustainability, kindness in the workplace, how to measure wellbeing, managing grief and more.

Aon Insights Series Asia

Expert Views on Today's Risk Capital and Human Capital Issues

Aon Insights Series Pacific

Expert Views on Today's Risk Capital and Human Capital Issues

Aon Insights Series UK

Expert Views on Today's Risk Capital and Human Capital Issues

Construction and Infrastructure

The construction industry is under pressure from interconnected risks and notable macroeconomic developments. Learn how your organization can benefit from construction insurance and risk management.

Cyber Labs

Stay in the loop on today's most pressing cyber security matters.

Cyber Resilience

Our Cyber Resilience collection gives you access to Aon’s latest insights on the evolving landscape of cyber threats and risk mitigation measures. Reach out to our experts to discuss how to make the right decisions to strengthen your organization’s cyber resilience.

Employee Wellbeing

Our Employee Wellbeing collection gives you access to the latest insights from Aon's human capital team. You can also reach out to the team at any time for assistance with your employee wellbeing needs.

Environmental, Social and Governance Insights

Explore Aon's latest environmental social and governance (ESG) insights.

Q4 2023 Global Insurance Market Insights

Our Global Insurance Market Insights highlight insurance market trends across pricing, capacity, underwriting, limits, deductibles and coverages.

Regional Results

How do the top risks on business leaders’ minds differ by region and how can these risks be mitigated? Explore the regional results to learn more.

Human Capital Analytics

Our Human Capital Analytics collection gives you access to the latest insights from Aon's human capital team. Contact us to learn how Aon’s analytics capabilities helps organizations make better workforce decisions.

Insights for HR

Explore our hand-picked insights for human resources professionals.

Workforce

Our Workforce Collection provides access to the latest insights from Aon’s Human Capital team on topics ranging from health and benefits, retirement and talent practices. You can reach out to our team at any time to learn how we can help address emerging workforce challenges.

Mergers and Acquisitions

Our Mergers and Acquisitions (M&A) collection gives you access to the latest insights from Aon's thought leaders to help dealmakers make better decisions. Explore our latest insights and reach out to the team at any time for assistance with transaction challenges and opportunities.

Navigating Volatility

How do businesses navigate their way through new forms of volatility and make decisions that protect and grow their organizations?

Parametric Insurance

Our Parametric Insurance Collection provides ways your organization can benefit from this simple, straightforward and fast-paying risk transfer solution. Reach out to learn how we can help you make better decisions to manage your catastrophe exposures and near-term volatility.

Pay Transparency and Equity

Our Pay Transparency and Equity collection gives you access to the latest insights from Aon's human capital team on topics ranging from pay equity to diversity, equity and inclusion. Contact us to learn how we can help your organization address these issues.

Property Risk Management

Forecasters are predicting an extremely active 2024 Atlantic hurricane season. Take measures to build resilience to mitigate risk for hurricane-prone properties.

Technology

Our Technology Collection provides access to the latest insights from Aon's thought leaders on navigating the evolving risks and opportunities of technology. Reach out to the team to learn how we can help you use technology to make better decisions for the future.

Top 10 Global Risks

Trade, technology, weather and workforce stability are the central forces in today’s risk landscape.

Trade

Our Trade Collection gives you access to the latest insights from Aon's thought leaders on navigating the evolving risks and opportunities for international business. Reach out to our team to understand how to make better decisions around macro trends and why they matter to businesses.

Weather

With a changing climate, organizations in all sectors will need to protect their people and physical assets, reduce their carbon footprint, and invest in new solutions to thrive. Our Weather Collection provides you with critical insights to be prepared.

Workforce Resilience

Our Workforce Resilience collection gives you access to the latest insights from Aon's Human Capital team. You can reach out to the team at any time for questions about how we can assess gaps and help build a more resilience workforce.

More Like This

View All
View All
Subscribe CTA Banner