Hacker News Reader

Comment by lifthrasiir | Hacker News Reader

We don't have a very good mainstream [1] solution for critical and performance-hungry applications. I do think that they are limited in number (many applications are not that performance-hungry) and Rust is already good enough, but those applications need the proof for correctness so that more dangerous code---say, what would need `unsafe` in Rust---can be safely added. This particular bug could have been reasoned once you know where to look at, after all.

[1] In my definition, this translates to "as popular and user-friendly as sanitizers".

View on HN

> those applications need the proof for correctness so that more dangerous code---say, what would need `unsafe` in Rust---can be safely added

There are actually already tools built for this very purpose in Rust (see Kani [1] for instance).

Formal verification has a serious scaling problem, so forming programs in such a way that there are a few performance-critical areas that use unsafe routines seems like the best route. I feel like Rust leans into this paradigm with `unsafe` blocks.

[1] - https://github.com/model-checking/kani

Yeah, I'm aware of Kani, but it is not optimal for many reasons, including but not limited: hard to install in some cases, loop unrolling is mandatory and does not scale in general (this is a main issue with bounded model checkers, not just Kani), and hard to give hints for efficient verification and/or harness generation. And Kani makes use of CMBC, which is a model checker for C/C++, so Rust is not even special in this regard.

It should be possible with Ada/SPARK. It's focused on low level systems programming and compilable programs are free from run-time errors. In addition, the correctness of the program or key properties can be proven at compile-time.

> "as popular and user-friendly as sanitizers" solution for critical and performance-hungry applications.

Google just did enable Memory Tagging Extension (ARM's hardware accelerated sanitizers) on the Pixels last year. May be sanitizing ISAs offer hope?

MTE is good to have, but it only reduces the probability of successful attacks (by a factor of 16). If the process is allowed to segfault multiple times attackers have a good chance to work around MTE.

That's a general limitation with tagged pointers, I belive? Have you come across demonstrations of such exploits?

Do you have a source for that? AFAIK Pixel 7 uses an ARM v8.2 CPU, which doesn't support MTE. The upcoming Pixel 8 might support it, but Google hasn't announced anything yet.

I'm going by the bugreports I see for a FOSS app I develop: https://github.com/celzero/rethink-app/issues/962

See: https://source.android.com/docs/security/test/memory-safety/...

Reply on news.ycombinator.com