Hi all,
I am experimenting with some hack that allows me to misuse
GCC's optimizer in combination with certain sanitizers to
prove specific safety properties statically.
For example, the shift sanitizers can find the bug in
uint8_t start = -1;
uint64_t result = start << 24;
(a real bug in a crypto library a long time ago), and
the signed-integer-overflow sanitizer finds the missing
error case in
static int divide(int a, int b)
{
if (b == 0)
error("divide by zero");
return a / b;
}
and much more.
A limitation of sanitizers is that they only find problems
exercised in the tests or by fuzzing, they do not ensure
that there are no remaining edge cases in the program.
But there is a neat and simple trick on how to ensure
(for small code snippets) that there is no such issue left.
1. Use certain UBSan sanitizers in trapping mode
2. Use optimization -O2
3. Add the following declaration:
[[gnu::warning("UNSAFE")]] void __builtin_trap();
This method then reliably pinpoints the remaining
problems. See for yourself:
https://godbolt.org/z/E9jqM53xr
https://godbolt.org/z/3ov3GPM74
What happens is that the sanitizer annotates the program
with __builtin_trap() where there is a potential problem,
while the optimizer then removes all traps it can show
to be unreachable.
The remaining ones are either real issues or false positives
(cases where the optimizer can not see that the trap is
unreachable). Those issue can then be fixed, annotated,
or one can add explicit run-time checks or assertions.
It does not work with all UB sanitizers (e.g. object-size
only opportunistically adds bound checking where a bound
is known) and sometimes there are also missing edge cases.
But for many this works already very well and I find it
useful.
Similar ideas are also explored (or already used) by others,
e.g. there is a related proposal for a "compile_assert" for
manually added assertions
https://www.open-std.org/jtc1/sc22/wg14/www/docs/n3950.pdf
or work by Anthropic that where they use Asan and then
prove that the generated RISC-V code does not trap (but
this then is conditional on the specifics of the generated
code)
https://www.anthropic.com/research/formal-verification
Considering that this is already - by accident - working in
a way that turns out to be useful, I think it would be cool
if this could become a proper GCC feature.
The nice thing is that this can be build on functionality we
already have, and works together with the optimizer and not
against it. The better the optimizer becomes, the more useful
is this feature.
The main issues I see is that there is currently no user friendly
interface to this. A user friendly version for this should allow
the user to selectively turn this on for some part of the code
(because turning it on for a large program produces too
many false positives) and also give the user some control over
which properties are checked, while also limiting the features
to specific sanitizers where it can work reliably. For example,
I could then turn this on for a snipped of crypto code, where
I want to make sure that there is no possibility for signed
integer overflow.
I could imagine a new pragma that turns this on and off
similar to the diagnostic pragmas we currently already have
(and perhaps using the same mechanism), possibly gated by a
global command-line flag that ensures that it does not collide
with any incompatible use of sanitizers or other features.
I would like to work on such a feature, but I want to
hear first what others think about this?
Martin
