The latest update for Ethereum comes from ChainSecurity who recently announced its first fully automated verification for certifying custom functional requirements of Ethereum smart contracts. The newly released verification security is termed VerX by a company of Swiss security experts from ETH Zurich.
VerX is a second-generation automated security tool which is purposefully designed in a way that works at certifying the functional requirements of Ethereum smart contracts. This recently announced tool for verification proves the functional correctness of these smart contracts by detecting the generic security threats and vulnerabilities that it may pose. Interestingly, the VerX promises clear formal guarantee despite being completely automated.
This new security tool differs majorly from the previous versions, where the tool could only detect the known threats and vulnerabilities of the contracts. However, this isn’t enough for the developers and auditors. As a result, the second-generation security tool, VerX, tests the Ethereum smart contracts for the generic vulnerabilities while automatically surveying the contracts for being functionally correct.
Happy to release VerX (https://t.co/x0Dxqq4Bkj), the first system for full functional verification of Ethereum contracts, bringing formal verification at the fingertips of auditors and developers 🎉
More info at this article: https://t.co/mjgRvMtPBp@ethereum @chain_security— Petar Tsankov (@ptsankov) April 25, 2019
Advertisement
Apart from giving full formal guarantees for the Ethereum contracts, VerX is fully automated as it is developed for security processing. Moreover, this new development makes sure that the security auditors and creators attain the one-click verification solution, without the need for complex and formal methods and achieve fully formal verification for their contracts.
VerX is prepared after considering the advantages and limitations of the previously existing techniques used for verification, and as a result, the new development in security tools make sure to understand the past confines and adjust it. One of the limitations with a previous security tool was that it could only process up to 2 or 3 transactions whereas the VerX challenges this technique by providing the opportunity of checking the violations in a contract for any number of transactions. Another existing security tool was designed in a way that could only check the smart contracts for a predefined set of generic vulnerabilities. However, the VerX is therefore designed taking this limitation into account by supporting custom functional requirements and check beyond the predefined list of security gaps and threats.
How Does VerX Work?
So now that you have a general idea about the tool, you might be wondering about the mechanisms behind it and how it works. VerX starts with an input of precise information from the smart contracts including the Solidarity-written code, deployment script that explains how the contracts are to be initialized and a formal requirement which needs to be verified for that smart contract.
Once this information if rightly entered, VerX will then conclude if the requirements of the smart contract match correctly with the expectation of requirement as entered in the input. Then VerX brings out a sequence of transactions which could potentially result in properly violation according to the developed security tool mechanism. It brings out a result window where it lists the dangerous or threatening vulnerabilities as well as the verified and generically safe requirements of the checked Ethereum smart contract.
Advertisement
The newest development of Ethereum world has already been used for various smart contracts. And it has rightfully managed to certify the objective of the contract, allowing the formalization of common specifications and re-using them with different but similar contracts and it has proven to be effective as it allows cheaper re-certifications for updating addresses if the developers come across verification correctness during the process.
