Open gsalzer opened 4 months ago
Hi @gsalzer, this is because, for all important overflows, solc versions post 0.8.0 adds an assert to check for violations. Hence, 0.8.0 does not detect any overflow issues. I get no issues for versions post 0.8.0 irrespective of using --unconstrained-storage
. Can you check it if that's the case?
@norhh Re 0.8.x: Yes, I know about the overflow and underflow checks, so the table | + | * | |
---|---|---|---|
int256 | no issue | no issue | |
int248 | no issue | no issue | |
uint256 | no issue | no issue | |
uint248 | no issue | no issue |
is the one to be expected.
However, for solc 0.8.25 and runtime code, i.e., the command
./myth a --bin-runtime --unconstrained-storage -c `solc --bin-runtime c.sol | tail -1`
I get indeed | + | * | |
---|---|---|---|
int256 | Int.Ar.Bugs | Int.Arith.Bugs | |
int248 | Int.Ar.Bugs | Int.Arith.Bugs | |
uint256 | no issue | no issue | |
uint248 | no issue | no issue |
So it seems that Mythril handles int
and uint
types differently: For the first, it detects an overflow without taking into account the surrounding check, whereas it either does not detect the overflow for uint
or it does, but notices the surrounding overflow check as well.
If you get different results: I'm using Z3 version 4.12.5 - 64 bit
and Mythril commit a4f51d0af
. The runtime codes (solc --bin-runtime --no-cbor-metadata
):
int248, add: 60806040526004361061001d575f3560e01c806392d0d15314610021575b5f80fd5b61002961002b565b005b60055f8054906101000a9004601e0b61004491906100d6565b5f806101000a8154817effffffffffffffffffffffffffffffffffffffffffffffffffffffffffffff0219169083601e0b7effffffffffffffffffffffffffffffffffffffffffffffffffffffffffffff160217905550565b5f81601e0b9050919050565b7f4e487b71000000000000000000000000000000000000000000000000000000005f52601160045260245ffd5b5f6100e08261009d565b91506100eb8361009d565b925082820190507fff8000000000000000000000000000000000000000000000000000000000000081127e7fffffffffffffffffffffffffffffffffffffffffffffffffffffffffffff82131715610146576101456100a9565b5b9291505056
int248, mul: 60806040526004361061001d575f3560e01c806392d0d15314610021575b5f80fd5b61002961002b565b005b60055f8054906101000a9004601e0b61004491906100d6565b5f806101000a8154817effffffffffffffffffffffffffffffffffffffffffffffffffffffffffffff0219169083601e0b7effffffffffffffffffffffffffffffffffffffffffffffffffffffffffffff160217905550565b5f81601e0b9050919050565b7f4e487b71000000000000000000000000000000000000000000000000000000005f52601160045260245ffd5b5f6100e08261009d565b91506100eb8361009d565b92508282026100f98161009d565b915082820584148315176101105761010f6100a9565b5b509291505056
int256, add: 608060405260043610601b575f3560e01c806392d0d15314601f575b5f80fd5b60256027565b005b60055f54603391906070565b5f81905550565b5f819050919050565b7f4e487b71000000000000000000000000000000000000000000000000000000005f52601160045260245ffd5b5f607882603a565b9150608183603a565b92508282019050828112155f8312168382125f84121516171560a45760a36043565b5b9291505056
int256, mul: 608060405260043610601b575f3560e01c806392d0d15314601f575b5f80fd5b60256027565b005b60055f54603391906070565b5f81905550565b5f819050919050565b7f4e487b71000000000000000000000000000000000000000000000000000000005f52601160045260245ffd5b5f607882603a565b9150608183603a565b9250828202608d81603a565b91507f800000000000000000000000000000000000000000000000000000000000000084145f8412161560c15760c06043565b5b828205841483151760d35760d26043565b5b509291505056
@norhh Re 0.4.26: It does not matter that the compiler is outdated, as the point is to analyze Mythril's capability to analyze bytecode. The unsystematic results may point to a weakness of Mythril's static analysis, either the method or its implementation. Even if we assume that Z3 behaves differently for addition and multiplication, uint and int, 256 and 248 (it most certainly does), the irregular matrix is surprising.
Description
Consider the following Solidity source
c.sol
:These are 16 source files (2 compilers, 4 types, 2 operations).
solc 0.4.26
Running the commands
The command
yields
no issues
for all variants (probably to be expected), whereassolc 0.8.25
For this compiler version, the two tables from above look like
Expected behavior
I'd expected Mythril to detect overflows more consistently, maybe just for (u)int256 and not for (u)int248 (if it is not able to infer the smaller type size), or just for addition and not multiplication, but not this patchwork.
Environment
Mythril:
0.24.8
Python:3.10.12
Solc:0.4.26+commit.4563c3fc.Linux.g++
/0.8.25+commit.b61c2a91.Linux.g++
OS: Ubuntu Linux 22.04