3 ms·

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 application

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".

bennettnate5 3y ago
> 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 https://github.com/model-checking/kani
- lifthrasiir 3y ago
  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.
irundebian 3y ago
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.
ignoramous 3y ago
> "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?
- lifthrasiir 3y ago
  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.
  - ignoramous 3y ago
    That's a general limitation with tagged pointers, I belive? Have you come across demonstrations of such exploits?
- akyuu 3y ago
  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.
  - ignoramous 3y ago
    I'm going by the bugreports I see for a FOSS app I develop: https://github.com/celzero/rethink-app/issues/962 https://github.com/celzero/rethink-app/issues/962 See: https://source.android.com/docs/security/test/memory-safety/arm-mte https://source.android.com/docs/security/test/memory-safety/...

bennettnate5 3y ago

> 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 https://github.com/model-checking/kani

lifthrasiir 3y ago
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.

irundebian 3y ago

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.

ignoramous 3y ago

> "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?

lifthrasiir 3y ago
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.
- ignoramous 3y ago
  That's a general limitation with tagged pointers, I belive? Have you come across demonstrations of such exploits?
akyuu 3y ago
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.
- ignoramous 3y ago
  I'm going by the bugreports I see for a FOSS app I develop: https://github.com/celzero/rethink-app/issues/962 https://github.com/celzero/rethink-app/issues/962 See: https://source.android.com/docs/security/test/memory-safety/arm-mte https://source.android.com/docs/security/test/memory-safety/...