4 ms·
The new version of securify, which will soon be available at https://securify.ch https://securify.ch, catches 7 our of the 9 mentioned issues automatically and
by hritzdorf 8y ago
The new version of securify, which will soon be available at https://securify.ch https://securify.ch, catches 7 our of the 9 mentioned issues automatically and is free.
I am one of the tool's authors. We went on to found ChainSecurity (https://chainsecurity.com https://chainsecurity.com) in order to deepen our research and understanding of smart contract security. Feel free to ask any questions about securify or ChainSecurity.
- seanwilson 8y agoDo you have any views on Solidity as a contract language and how suitable it is for being formally verified? Does it make any properties you want to check difficult or impossible to verify? My experience with formal verification is that the further a language is away from being a pure functional language with easy to check termination, the more difficult you make life for yourself. You really want a smart contract language that was specifically created to be easy to formally verify rather than trying to tack on formal verification later.
- ptsankov1 8y agoNote that tools like Securify work directly on the EVM, and are therefore agnostic to the high-level language the contract is written in. The EVM itself is not as amenable to formal analysis (no types, explicit function calls, etc.).
- snissn 8y agoA bit confusing how to parse the audit. For example the output of this contract: https://etherscan.io/address/0xb6ed7644c69416d67b522e20bc294a9a9b405b31#code https://etherscan.io/address/0xb6ed7644c69416d67b522e20bc294... it's a bit opaque what lines of code you are warning of
- hritzdorf 8y agoThank you for the feedback. We will add some extra information. In this particular examples there seem to be no warnings. However, as I said the new version is coming soon.