3 ms·

> we're seeing more and more clients take memory safety seriously Running your test suite with asan, msan, tsan isn't sufficient? From my experience you need t

> we're seeing more and more clients take memory safety seriously Running your test suite with asan, msan, tsan isn't sufficient? From my experience you need to start doing really nasty things (which shouldn't pass code review) before the sanitizers won't find your issues.

woodruffw 4y ago
There are plenty of things that ASan won’t catch, like misuse between contiguous allocations. But that’s sort of tangential: the goal is to write software that’s correct to begin with, not poke holes in it with the testsuite after the fact. With Rust, I can pick third-party dependencies that I can be (vanishingly) confident don’t have memory safety issues; when I start a greenfield C++ project, any dependencies I bring in are now potential sources of memory unsafety in my code.
- LtWorf 4y ago
  Do you vet all of your dependencies' code for unsoundness when using unsafe?
  - woodruffw 4y ago
    One of the guarantees that Unsafe Rust makes is that well-formed unsafe code cannot trigger unsoundness in safe code. In other words: I very rarely write unsafe code myself. When I bring in others’ unsafe code, I use cargo-geiger and siderophile (which I help maintain) to quantify it.
    - LtWorf 4y ago
      It's not a guaranteed guarantee as far as I can understand. Or such bugreports would make no sense: https://github.com/denoland/deno/issues/15020 https://github.com/denoland/deno/issues/15020
      - woodruffw 4y ago
        The bug report says exactly what I said: if you don't write well-formed Unsafe Rust, then Rust will not make any guarantees about invariant preservation in Safe Rust. This is exactly the same as in C++, except stronger: in C++, any piece of well-formed code can violate safe invariants. In Rust, only unsafe code can violate safe invariants, and can only do so if it isn't itself well-formed.
      - rng_civ 4y ago
        According to the RustBelt paper [0]: > so long as the only unsafe code in a well-typed λRust program is confined to libraries that satisfy their verification conditions, the program is safe to execute. I think the main caveat is that IIRC, the RustBelt unsafe rules do not cover ALL uses of unsafe in the wild, they analyze only a subset of Rust as whole, and of course, unsafe usage actually has to obey the rules. But I'm hardly an expert here. That bug report basically says they broke the unsafe rules and thus the guarantee no longer holds (and there is UB). [0] https://dl.acm.org/doi/abs/10.1145/3158154 https://dl.acm.org/doi/abs/10.1145/3158154
ssokolow 4y ago
I'm reminded of this quote, written in support of more and stronger use of systems for formal verification, like powerful type systems: > Program testing can be a very effective way to show the presence of bugs, but it is hopelessly inadequate for showing their absence. -- Edsger W. Dijkstra, "The Humble Programmer" (1972)
- snovv_crash 4y ago
  Oh for sure, use better types to express the problem in ways that the compiler can catch mistakes. But... you do need to show at some point that your code actually does what you claim it does, even if just for a single use case; might as well piggyback sanitizers since you're running tests anyways. Re: Dijkstra, I'm not trying to prove that the code has no memory errors, I'm trying to make sure none get triggered in production ie. the difference between computer science and software engineering. If there was a simple and easy way to do behaviour proofs I'd be happy to use that, but coq et al. are a real pain.

woodruffw 4y ago

There are plenty of things that ASan won’t catch, like misuse between contiguous allocations. But that’s sort of tangential: the goal is to write software that’s correct to begin with, not poke holes in it with the testsuite after the fact. With Rust, I can pick third-party dependencies that I can be (vanishingly) confident don’t have memory safety issues; when I start a greenfield C++ project, any dependencies I bring in are now potential sources of memory unsafety in my code.

LtWorf 4y ago
Do you vet all of your dependencies' code for unsoundness when using unsafe?
- woodruffw 4y ago
  One of the guarantees that Unsafe Rust makes is that well-formed unsafe code cannot trigger unsoundness in safe code. In other words: I very rarely write unsafe code myself. When I bring in others’ unsafe code, I use cargo-geiger and siderophile (which I help maintain) to quantify it.
  - LtWorf 4y ago
    It's not a guaranteed guarantee as far as I can understand. Or such bugreports would make no sense: https://github.com/denoland/deno/issues/15020 https://github.com/denoland/deno/issues/15020
    - woodruffw 4y ago
      The bug report says exactly what I said: if you don't write well-formed Unsafe Rust, then Rust will not make any guarantees about invariant preservation in Safe Rust. This is exactly the same as in C++, except stronger: in C++, any piece of well-formed code can violate safe invariants. In Rust, only unsafe code can violate safe invariants, and can only do so if it isn't itself well-formed.
    - rng_civ 4y ago
      According to the RustBelt paper [0]: > so long as the only unsafe code in a well-typed λRust program is confined to libraries that satisfy their verification conditions, the program is safe to execute. I think the main caveat is that IIRC, the RustBelt unsafe rules do not cover ALL uses of unsafe in the wild, they analyze only a subset of Rust as whole, and of course, unsafe usage actually has to obey the rules. But I'm hardly an expert here. That bug report basically says they broke the unsafe rules and thus the guarantee no longer holds (and there is UB). [0] https://dl.acm.org/doi/abs/10.1145/3158154 https://dl.acm.org/doi/abs/10.1145/3158154

ssokolow 4y ago

I'm reminded of this quote, written in support of more and stronger use of systems for formal verification, like powerful type systems: > Program testing can be a very effective way to show the presence of bugs, but it is hopelessly inadequate for showing their absence. -- Edsger W. Dijkstra, "The Humble Programmer" (1972)

snovv_crash 4y ago
Oh for sure, use better types to express the problem in ways that the compiler can catch mistakes. But... you do need to show at some point that your code actually does what you claim it does, even if just for a single use case; might as well piggyback sanitizers since you're running tests anyways. Re: Dijkstra, I'm not trying to prove that the code has no memory errors, I'm trying to make sure none get triggered in production ie. the difference between computer science and software engineering. If there was a simple and easy way to do behaviour proofs I'd be happy to use that, but coq et al. are a real pain.