Hacker News new | ask | show | jobs
by sevenoftwelve 1205 days ago
Author here: No, symbolic verification does not protect from buffer overflows. Writing the implementation in Rust does

We are investigating ways how to do more formal verification for the implementation itself.

2 comments

> Writing the implementation in Rust does

sigh, not true.

https://tgrez.github.io/posts/2022-06-19-buffer-overflow-in-... https://shnatsel.medium.com/how-rusts-standard-library-was-v... "This is a buffer overflow bug in the standard library’s implementation of a double-ended queue." "Rust will panic if you attempt to write out of bounds."

Writing the implementation will increase memory safety but only if the implementation adheres strictly to safe Rust - which means even avoiding ANY packages that use unsafe features. The fact Rust can pull in any package that has an unsafe {} block means you're not promised to be safe.

The equivalent could be said about writing the implementation in JavaScript, Python, etc... (that they protect against buffer overflows)

Granted, writing things in Rust doesn't exclude the possibility of a buffer overflow entirely. It does help make it much less likely.
Yes, I mentioned it :)
So any claim such as your previous one is rather of no value.

>It does help make it much less likely.

Yeah... To the same extent as the infamous proof of formal correctness of an example program published in a book, until the program was tested negatively by a student some months later.

Panicking when writing out of bounds is not a bad thing though, this is the behavior you want, assuming you can't statically guarantee that indexes are always in bounds.

It is true though that the underlying unsafe rust in std, or crates or whatnot can have errors though and sometimes we just kind of pretend it's not there since we don't see it.

>The equivalent could be said about writing the implementation in JavaScript, Python, etc... (that they protect against buffer overflows)

This is why we should be encouraging people to write in memory safe languages in general and not just rust or whatever. The overwhelming majority of software does not need to be some super optimized native-code SIMD+AVX1024 beast and would run on something like .net or the JVM, and even Python with no issues. It makes me cringe every time I see some random utils written in C that would work fine in Python.

> No, symbolic verification does not protect from buffer overflows. Writing the implementation in Rust does

I don't believe writing the implementation in Rust does that: https://blog.rust-lang.org/2018/09/21/Security-advisory-for-...

One would think that this would be fixed in the last five years?
Certainly. What I don't believe is certain is that only one such vulnerability has ever existed and none exist in Rust today.

It's not pedantic to differentiate between mitigating a thing and preventing a thing.

You can add `#![forbid(unsafe_code)]` to your codebase to avoid any unsafe Rust, which should prevent buffer overflows. Obviously it may make writing a codebase somewhat harder.
Will that restriction also be applied transitively to all dependencies?
No. That kind of restriction cannot realistically be applied to any project above toy scale. The stdlib uses unsafe code to implement a large number of memory management primitives, because the language is (by design!) not complex enough to express every necessary feature in just safe code. Rust's intention is merely to limit the amount of unsafe code as much as possible.
For that, I believe you need to use cargo-geiger[0] and audit the results.

[0] - https://github.com/rust-secure-code/cargo-geiger

No, and in fact that would be impractical, because you can't do anything useful (e.g., any I/O whatsoever) without ultimately either calling into a non-Rust library or issuing system calls directly, both of which are unsafe.
The amount of reported and unfixed memory bugs in Rust went 10x more, not less in the last 5 years.
If you believe you can find a memory unsafety vulnerability in this project's Rust code based on the existence of those bugs, feel free to do so.