Contract verification made easier

Summary: Trail of Bits released manticore-verifier, a tool that lets smart contract authors write security properties as Solidity methods and have them checked automatically by symbolic execution, using the same property format as the Echidna fuzzer. In its example run against a simple token contract, the tool found that transferring an extremely large token amount overflowed an internal integer and let the sender create tokens out of thin air.
Why it matters: The failure it demonstrates is an integer overflow reachable through a single transfer call, the kind of bug that mints tokens from nothing in a live contract. Writing the property once and running it through both symbolic execution and fuzzing lowers the cost of catching that before deployment.

Read the original at Trail of Bits Blog ↗