VerX: Full functional verification for Ethereum contracts, now at your fingertips
ChainSecurity, an ETH Zurich spin-off, is happy to announce VerX, the first automated verifier for certifying custom functional requirements of Ethereum smart contracts. A demo of VerX is available at https://verx.ch.
What is VerX?
VerX marks the beginning of a new, second generation automated security tools for contracts, which go beyond detection of known, generic security vulnerabilities and are capable to certify the functional correctness of smart contracts. Moreover, VerX provides full formal guarantees while being automated. We elaborate on these important points below.
Support for custom functional requirements
Existing first-generation security tools for Ethereum (including our own Securify) are limited to checking known security vulnerabilities (such as integer overflows). While useful, this is clearly not enough, because auditors and developers must not only guarantee that their contracts are free of known vulnerabilities, but also that they are functionally correct. VerX bridges this gap and allows auditors and developers to precisely specify the functional requirements they would like to verify, such as “No investor can claim a refund if the total amount of investments collected during the crowdsale has reached the target goal.”
Full formal guarantees
VerX uses a novel sound abstraction technique to prove that the smart contracts conform to the provided requirements. That is, once the contract is deployed, the verified requirements are guaranteed to hold for the lifetime of the smart contract. This is in sharp contrast to existing tools based on symbolic execution and fuzzing, which are useful to discover bugs but unable to provide full formal guarantees, as we explain in more detail in our comparison below.
Fully automated
Finally, the analysis pipeline behind VerX is fully automated. This makes VerX a one-click verification solution that does not require elaborate experience and formal methods, thereby bringing formal verification at the fingertips of security auditors and developers.
How does VerX differ from other security tools for Ethereum?
In the past few years, a number of different security tools have been developed with the goal to help developers write more secure smart contracts. While different on the surface, these tools are based on well-known program analysis techniques whose benefits and limitations are well understood (summarized in Fig. 1).
We consider the most common techniques used by popular tools:
Symbolic execution
Existing tools based on symbolic execution focus on checking generic vulnerabilities using off-the-shelf, automated constraint solvers. Nonetheless, symbolic execution can check expressive, contract-specific properties, and we anticipate that current tools would provide an interface for custom properties in the future. These tools are, unfortunately, fundamentally limited to reasoning about a bounded number of transactions (usually 2–3 transactions) and will inevitably miss deeper violations (which require more transactions to manifest). In contrast, VerX certifies the absence of violations for any number of transactions.
Static analysis
Static analysis tools, such as our own Securify, are capable to provide guarantees and are also fully automated. These tools are, however, limited to checking a predefined list of generic security vulnerabilities, such as unrestricted access to storage. VerX bridges this gap by supporting custom functional requirements, formalized in an intuitive and expressive specification language.
Interactive theorem provers
Finally, theorem provers such as Isabelle/HOL and Coq can be used to verify the functional correctness of contracts. Unfortunately, these tools require a non-trivial manual effort and expertise, making the audit process expensive and time-consuming (the verification of simple properties can take several months). Not surprisingly, only a handful of contracts have been formally verified with these tools. In contrast, the verification pipeline of VerX is fully automated and does not require expertise in formal verification, which is essential in bringing strong formal guarantees to all projects.
How is the custom business logic of a smart contract specified?
VerX has a designated specification language that allows auditors and developers to express the intended behavior of contracts. Common functional requirements include access control, correct enforcement of business processes, contextual constraints, and many others. To ease adoption, VerX’s specification language is based on Solidity, extending it with support for additional keywords, which are used to refer to past blockchain states, aggregates over mappings, and other idioms often encountered in requirements.
We exemplify the specification of common function requirements in Fig. 1 and elaborate on two examples:
Example 1: Access control
The first requirement in Fig. 1 stipulates that only the owner can change the state of an escrow contract. Concretely, it constraints which users are allowed to modify a critical part of the contract’s storage (namely, the variable state). This requirement is formalized with the following implication: if the value of the state variable is changed in-between two transactions (captured by the condition Escrow.state != prev(Escrow.state)), then the transaction was sent by the escrow’s owner (captured by msg.sender == Escrow.owner).
Example 2: Business processes
Smart contracts often implement non-trivial business processes and auditors must ensure that the state transitions of these processes are correctly enforced.The second requirement in Fig. 1 illustrates such a requirement. It formalizes that once the crowdsale contract transitions to state REFUND, then it will never transition to state FINALIZED in the future, and vice versa.
Finally, we note that VerX’s specification language is based on a solid formal foundation (linear temporal logic) and can express many other useful idioms. For more technical details, please read the VerX documentation.
How does VerX work?
VerX takes as input the code of smart contracts (written in Solidity), deployment script (which defines how the contracts will be initialized), and a formal requirement to be verified:
Given these inputs, VerX either verifies that the requirement is satisfied or not. In the latter case, VerX outputs a sequence of transactions that may result in violating the property. We illustrate an example verification report produced by VerX in Fig. 4:
Impact
VerX has been already used to verify 100+ Ethereum contracts. In this process, we have observed at least three major benefits in adopting VerX as part of the audit process.
- First, it is capable to certify what the contract does, as opposed to merely looking for bugs in the contract.
- Second, it allows formalization and re-use of common specifications (for example, that specify correctness requirements for tokens and crowdsales). Once the common requirements have been formalized, they can be re-used across different projects with similar contracts.
- Finally, it enables cheap re-certification, which is useful in case of code updates that address, for example, encountered correctness issues during the verification process.
Where can I find more information?
To find out more about VerX, you can:
- Watch our talk about VerX, presented at ETHCC in March 2019
- Try our VerX demo by verifying custom properties on popular smart contracts.
- Read our VerX documentation
If you have any feedback, please write us as contact@chainsecurity.com
