-
Notifications
You must be signed in to change notification settings - Fork 11
Tools use cases (Work in progress)
- Forge
- Mythril
- Slither
- Picode's Code4rena 4nalyz3r
- Halmos
- Pyrometer
- Heimdall
- Certora Prover
- Chisel
- Anvil
- Cast
Here we would like to get the source code, compile it, analyze the bytecode to get the solidity code, etc
Disassembler and decompiler
Bytecode analysis, reverse engineering of smart contracts
Heimdall is used to disassemble and decompile Ethereum bytecode back into readable Solidity-like code, enabling analysis and review of compiled contracts where the source is not available.
heimdall <bytecode>This is what I consider the "I have no idea what it's inside the code, I just don't care. This phase is generally after compiling and basic setup
Symbolic execution tool
In-depth security reviews, complex vulnerability detection
Mythril leverages symbolic execution to simulate all possible execution outcomes in the Ethereum bytecode to find security vulnerabilities. It is useful for detecting sophisticated smart contract exploits that may not be immediately evident.
myth analyze --solc-json <input.json>Static analysis tool
Quick code reviews, continuous integration, common vulnerability identification
Slither scans Solidity code for security vulnerabilities, bad practices, and code optimization. Its integration with continuous integration systems makes it an essential tool for automated and preventive code review processes.
slither <contract.sol>Static analysis tool
Quick code reviews, continuous integration, common vulnerability identification
4nalyz3r is a static analyzer that would help finding basic vulnerabilities and optimizations.
analyze4 srcValid range analyzer
Prevention of numerical bugs, range analysis
Pyrometer focuses on the analysis of numerical ranges within smart contract code to prevent overflows and underflows, which can lead to critical security issues.
pyrometer check <contract.sol>Formal verification tool
Mathematically rigorous smart contract verification, advanced security assurance
Halmos provides formal verification for smart contracts, which involves mathematically proving the correctness of contract logic against a formal specification. It has an amazing integration within Foundry projects and would provide an extra verification to the system after unit tests and fuzzing tests.
halmosFormal verification tool
Contract verification against formal specifications, high-assurance code
Certora Prover uses formal methods to verify smart contracts against user-provided specifications. It aims to prove that contracts meet their specified requirements, preventing a wide range of bugs and vulnerabilities.
certoraRun <contract.sol>:<contract>