Gambit: A Solidity Mutation Testing Tool for Formal Verification

When developers write tests, they often think about common logical errors they may have introduced or edge cases they may not have handled. But what about errors they did not think they may have introduced, such as programming or complex logical errors? How does one write tests to anticipate unanticipated bugs? Mutation testing is a practical solution to this problem. It is a well-studied technique for improving / assessing test suites and has seen significant adoption in large software companies [1]. Typically applied in the context of testing, the key idea is to synthesize faulty versions of a program and check if the existing test suite is able to catch these faulty programs. If not, then the developer expands the test suite with new tests designed to catch the previously uncaught problems. Mutation analysis is the process of measuring the quality of an existing test suite in terms of its ability to kill “mutants” (faulty programs).

In this blog, we discuss our efforts to apply mutation testing in the context of automated verification. We have developed an open source mutation generator for the Solidity language and integrated it with the Certora Prover, a tool for formally verifying smart contracts. The Certora Prover is accompanied by a declarative, domain specific language called CVL that allows users to write formal specifications for their programs as “rules”. The Prover then automatically verifies that the program satisfies the specification in all possible cases or it produces a counterexample showing a violation. This procedure can identify critical security bugs before the code is deployed by checking the executable bytecode (you can read more about Certora’s core technology in our white paper). But how does the user know whether the specification was “good enough”? After all, one of the hardest challenges in formal verification is writing the specification itself.

Leave a Comment