Add Support for Integer overflow and underflow detection

[Akshat-Mishra101]

Add Support for Integer overflow and underflow detection

[0xalpharush]

We have never implemented it because it requires precise value range analysis which is slow and even then still prone to false positives. I don't think a tool like slither is the best way to identify overflows compared to something like a sanitizer in debug versions of solc paired with a fuzzer

[Akshat-Mishra101]

I wonder if there might be a middle ground that leverages Slither's capabilities without compromising its performance and accuracy.

For instance, Instead of a full range analysis, could we implement a more basic detector that flags only clear-cut cases of potential overflows and underflows? This detector could serve as an initial check, with more complex scenarios left for dynamic analysis tools as you suggested.

[0xalpharush]

You're welcome to give it a shot! It may be possible to flag exclusively overflows that will definitely occur like if (x > y) { unchecked { y - x }}; i.e. the detector would only identify true positives and allow false negatives.

This functionality could also be built on top of slither as an extension and not as a detector. Then, it could use something like an SMT solver and find counterexamples that demonstrate an overflow can occur.

Fwiw we are planning to remove (or not run by default) noisy detectors after benchmarking in the near future.

[Akshat-Mishra101]

Okay, I'd like to proceed with its development. Just wanted make sure, if this was the right process before i attempt to make any sort of contribution. I'd like to build an exclusive overflow detector to only flag clear-cut cases. :)