Securify v2.0 outperforms state-of-the-art vulnerability scanners for smart contracts by bringing:
Importantly, Securify v2.0 remains free and open-source. You can download Securify v2.0 for free on GitHub.
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.
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.
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.” …
We are happy to release SOLTIX, a scalable framework for automated testing of Solidity compilers.
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.
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:
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). …