mythril/security_checks.md

Mythril Detection Capabilities

Detection modules, ideas collection and wish list. Contributions are welcome!

Issue	Description	Mythril Detection Module(s)	References
Unprotected functions	Critical functions such as sends with non-zero value or suicide() calls are callable by anyone, or msg.sender is compared against an address in storage that can be written to. E.g. Parity wallet bugs.	unchecked_suicide, ether_send
Missing check on CALL return value		unchecked_retval	Handle errors in external calls
Re-entrancy	Contract state should never be relied on if untrusted contracts are called. State changes after external calls should be avoided.	external calls to untrusted contracts	Call external functions last Avoid state changes after external calls
Multiple sends in a single transaction	External calls can fail accidentally or deliberately. Avoid combining multiple send() calls in a single transaction.		Favor pull over push for external calls
External call to untrusted contract		external call to untrusted contract
Delegatecall or callcode to untrusted contract		delegatecall_forward
Integer overflow/underflow		integer_underflow	Validate arithmetic
Timestamp dependence		Dependence on predictable variables	Miner time manipulation
Payable transaction does not revert in case of failure
Use of tx.origin		tx_origin	Solidity documentation, Avoid using tx.origin
Type confusion
Predictable RNG		Dependence on predictable variables
Transaction order dependence			Front Running
Information exposure
Complex fallback function (uses more than 2,300 gas)	A too complex fallback function will cause send() and transfer() from other contracts to fail. To implement this we first need to fully implement gas simulation.
Use require() instead of assert()	Use assert() only to check against states which should be completely unreachable.	Exceptions	Solidity docs
Use of depreciated functions	Use revert() instead of throw(), selfdestruct() instead of suicide(), keccak256() instead of sha3()
Detect tautologies	Detect comparisons that always evaluate to 'true', see also #54
Call depth attack	Depreciated		EIP 150 Hard Fork