Image for post
Image for post

We are happy to announce Securify v2.0, the new release of the popular security scanner for Ethereum smart contracts.

Securify v2.0 outperforms state-of-the-art vulnerability scanners for smart contracts by bringing:

  • High precision, thanks to a brand new intermediate representation (IR) for Solidity and fully declarative context-sensitive static analysis;
  • Improved scalability, leveraging a fully declarative static analysis powered by the efficient Souffle Datalog engine;
  • High vulnerability coverage, covering 37 distinct security properties adopted from the Smart Contract Weakness Classification Registry and classified by their severity.

Importantly, Securify v2.0 remains free and open-source. You can download Securify v2.0 for free on GitHub.

What does Securify v2.0 support?

  • Ethereum smart contracts written in Solidity 0.5.* and 0.6.*
  • 37 vulnerabilities classified by their severity (the full list of supported vulnerabilities is at the bottom of this…

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?

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.”


Image for post
Image for post

We are happy to release SOLTIX, a scalable framework for automated testing of Solidity compilers.

What is SOLTIX?

SOLTIX is a framework for automated testing of Solidity compilers. It started as the master thesis project of Nils Weller, supervised by researchers from the ICE center, and then evolved into a larger project that is now officially funded by the Ethereum Foundation.

How does it work?

SOLTIX tests the Solidity compiler and, in turn, the Ethereum Virtual Machine (EVM) in a fully automated way. There are two ways to test the compiler:

1. Testing via synthesis of random Solidity contracts

Image for post
Image for post
Fig 1: Testing via synthesis of random contracts. SOLTIX injects checks and emits an Error event to indicate that runtime values deviate from the expected behavior.

In this mode, to test the compiler SOLTIX automatically generates random Solidity contracts. It then interprets the generated contracts to anticipate the expected values that will appear at runtime and injects statements that would throw an error if the execution is incorrect. In the example of Fig. 1, SOLTIX checks whether the value assigned to variable x equals 5, and emits an error if this is not the case (to indicate an error in the compiler). …

About

Petar Tsankov

Senior researcher at ETH Zurich, Co-founder and Chief Scientist of ChainSecurity

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