I wonder how true the assertion "This performance is partly achieved by sacrificing memory safety" is today. I suspect a sufficiently advanced compiler can remove bounds checks where they are provably unnecessary, and a sufficiently advanced CPU can run the remaining checks in parallel with the array accesses. But it'd be interesting if there's been any research on that.
(A sufficiently advanced programming language can avoid the entire issue by writing loops as map, fold, etc. but we're talking about C here.)
> I suspect a sufficiently advanced compiler can remove bounds checks where they are provably unnecessary,
That’s true by definition, isn’t it?
> and a sufficiently advanced CPU can run the remaining checks in parallel with the array accesses.
But it still would slow down the program, as the CPU would have to commit resources to that bound checking that it then cannot use for doing other things.
There are a few things that cannot be done as fast in rust, but those are rare to need in the real world. Most of the things rust cannot do are around sharing memory between threads with locks - Humans have a very hard time getting code that does this to work correctly and usually have race conditions because they analysed the problem wrong.
> The findings highlight significant variations
in the theoretical detection capabilities of these techniques
and reveal that, in practice, the implementations of most
available sanitizers fall short of their conceptual potential.
Furthermore, the evaluation demonstrates the complexities
and diversity of memory bugs in C/C++, as well as the
challenges associated with detecting them. For instance, our
results show that SoftBound+CETS, a conceptually complete sanitizer, misses nearly a quarter of spatial memory
bugs in its original implementation, while ASan, likely the
most widely used memory sanitizer, cannot detect 50% of
use-after-* bugs and any non-linear overflows and under-
flows. Ultimately, our evaluation concludes that no sanitizer
currently provides complete temporal or spatial memory
safety
Rust supports all the same sanitizers as c/C++ last I checked (at least UBSAN, TSAN, MSAN and ASAN which are the only ones I’ve ever seen used in practice on c/c++).
Weird that Infer [1] was not included in the evaluation. It supports C/C++ and its underlying reasoning framework (Separation Logic [2]) is exactly geared towards checking memory safety.
Sanitizers are runtime tools, not static analysis tools.
Static analyzers are also virtually never sound as sound tools produce an outrageous number of false positives, especially when languages that so easily permit nonlocal mutation.
Wait hold up the same authors did MESH: https://arxiv.org/pdf/2108.08683
So why isn't MESH part of the evaluation? And why isn't it mentioned even once in the paper?
I wonder if their test cases are available.
Fil-C is specifically engineered to catch everything so it would be interesting to check it against their tests
I wonder how true the assertion "This performance is partly achieved by sacrificing memory safety" is today. I suspect a sufficiently advanced compiler can remove bounds checks where they are provably unnecessary, and a sufficiently advanced CPU can run the remaining checks in parallel with the array accesses. But it'd be interesting if there's been any research on that.
(A sufficiently advanced programming language can avoid the entire issue by writing loops as map, fold, etc. but we're talking about C here.)
> I suspect a sufficiently advanced compiler can remove bounds checks where they are provably unnecessary,
That’s true by definition, isn’t it?
> and a sufficiently advanced CPU can run the remaining checks in parallel with the array accesses.
But it still would slow down the program, as the CPU would have to commit resources to that bound checking that it then cannot use for doing other things.
There are a few things that cannot be done as fast in rust, but those are rare to need in the real world. Most of the things rust cannot do are around sharing memory between threads with locks - Humans have a very hard time getting code that does this to work correctly and usually have race conditions because they analysed the problem wrong.
Download possible without paywall from https://publica.fraunhofer.de/entities/publication/9d7783f8-...
Unfortunately that gives a 500 error when attempting to download the PDF (maybe the server is overloaded now?)
Conclusion is scathing:
> The findings highlight significant variations in the theoretical detection capabilities of these techniques and reveal that, in practice, the implementations of most available sanitizers fall short of their conceptual potential. Furthermore, the evaluation demonstrates the complexities and diversity of memory bugs in C/C++, as well as the challenges associated with detecting them. For instance, our results show that SoftBound+CETS, a conceptually complete sanitizer, misses nearly a quarter of spatial memory bugs in its original implementation, while ASan, likely the most widely used memory sanitizer, cannot detect 50% of use-after-* bugs and any non-linear overflows and under- flows. Ultimately, our evaluation concludes that no sanitizer currently provides complete temporal or spatial memory safety
If SoftBound+CETS has the best results, why does Fraunhofer not sponsor the creation of a Debian package?
It is unmaintained:
https://github.com/Fraunhofer-AISEC/softboundcets
Seems like it should have "C/C++" in the title. Or maybe that's understood?
Sanitizers aren't just for C/C++. Rust, go, D all have at least asan support.
Rust supports all the same sanitizers as c/C++ last I checked (at least UBSAN, TSAN, MSAN and ASAN which are the only ones I’ve ever seen used in practice on c/c++).
Weird that Infer [1] was not included in the evaluation. It supports C/C++ and its underlying reasoning framework (Separation Logic [2]) is exactly geared towards checking memory safety.
[1] https://fbinfer.com/
[2] https://en.wikipedia.org/wiki/Separation_logic
Sanitizers are runtime tools, not static analysis tools.
Static analyzers are also virtually never sound as sound tools produce an outrageous number of false positives, especially when languages that so easily permit nonlocal mutation.
Looks interesting, but unfortunately the research paper is behind a paywall
Here is the author's version: https://publica-rest.fraunhofer.de/server/api/core/bitstream...
really sorry about that gaffe ! i had access, and the content was too interesting to not share.
as @osivertsson has kindly pointed out, may you please access that, and share your insights here ? thanks !