VerX: Full functional verification for Ethereum contracts, now at your fingertips

Petar Tsankov
Apr 24, 2019 · 6 min read
Image for post
Image for post
VerX: the first automated verifier for certifying custom functional requirements of Ethereum smart contracts.

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?

Support for custom functional requirements

Full formal guarantees

Fully automated

How does VerX differ from other security tools for Ethereum?

Image for post
Image for post
Fig 1: Benefits and limitations of existing techniques for analyzing Ethereum contracts

We consider the most common techniques used by popular tools:

Symbolic execution

Static analysis

Interactive theorem provers

How is the custom business logic of a smart contract specified?

We exemplify the specification of common function requirements in Fig. 1 and elaborate on two examples:

Image for post
Image for post
Fig 2: Common types of requirements

Example 1: Access control

Example 2: Business processes

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?

Image for post
Image for post

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:

Image for post
Image for post
Fig 4: Verification results reported by VerX

Impact

  1. First, it is capable to certify what the contract does, as opposed to merely looking for bugs in the contract.
  2. 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.
  3. 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?

If you have any feedback, please write us as contact@chainsecurity.com

ChainSecurity

From the world of secure smart contracts

Medium is an open platform where 170 million readers come to find insightful and dynamic thinking. Here, expert and undiscovered voices alike dive into the heart of any topic and bring new ideas to the surface. Learn more

Follow the writers, publications, and topics that matter to you, and you’ll see them on your homepage and in your inbox. Explore

If you have a story to tell, knowledge to share, or a perspective to offer — welcome home. It’s easy and free to post your thinking on any topic. Write on Medium

Get the Medium app

A button that says 'Download on the App Store', and if clicked it will lead you to the iOS App store
A button that says 'Get it on, Google Play', and if clicked it will lead you to the Google Play store