4 ms·

I’m confused. Wasn’t the error actually in an unverified subsystem and isomorphic to an error caught by the model checker in a verified subsystem? Isn’t this mo

I’m confused. Wasn’t the error actually in an unverified subsystem and isomorphic to an error caught by the model checker in a verified subsystem? Isn’t this more of a cautionary tale for someone not relying on formal verification?

lisper 2y ago
> Wasn’t the error actually in an unverified subsystem and isomorphic to an error caught by the model checker in a verified subsystem? No, it was quite a bit more subtle than that. The problem was that there was no mechanism to enforce the use of the formally verified API, and an application programmer put in a direct call to a system function that bypassed that API. Source: I was the technical lead on the RAX executive.
- extrabajs 2y ago
  It sounds more like a cautionary tale against bypassing APIs. What part of this is related to formal verification?
- Quekid5 2y ago
  This is why friends don't let friends use unsafePerformIO ... or whatever the equivalent was here :) I'm still a bit confused about the point though. I feel like an adequate rejoinder would be to enforce formal methods at all the levels? I'm obviously not talking specifics (because I don't know them! ... and you do), but this seems like a failure of process or lack of enforcement of formal methods "all the way down" as it were. I dunno, color me confused...
  - wucke13 2y ago
    Which almost reads as a cautionary tale about mechanisms like Dust's `unsafe`. Not necessarily the specifics of the Rust, but the overall idea of having a safe (by whatever means) sunset of operations and and additional unsafe operations, which eases code analysis tremendously. You can't got without unsafe in most embedded systems. But it's good to very explicitly mark in the code wherever the unknown depths of UB lurk if not the most attention is exercised.
    - renox 2y ago
      While this is true, let's not forget that if there's a problem in the unsafe section, the issue can manifest itself much later in the safe code.. I'm not a Rust programmer but I remember reading about such kind of issue (an alignment error if memory serves). So sometimes you can build a 'self contained' unsafe part made safe with the right API but not always, which is already a significant improvement over other languages which are unsafe all the time..

lisper 2y ago

> Wasn’t the error actually in an unverified subsystem and isomorphic to an error caught by the model checker in a verified subsystem? No, it was quite a bit more subtle than that. The problem was that there was no mechanism to enforce the use of the formally verified API, and an application programmer put in a direct call to a system function that bypassed that API. Source: I was the technical lead on the RAX executive.

extrabajs 2y ago
It sounds more like a cautionary tale against bypassing APIs. What part of this is related to formal verification?
Quekid5 2y ago
This is why friends don't let friends use unsafePerformIO ... or whatever the equivalent was here :) I'm still a bit confused about the point though. I feel like an adequate rejoinder would be to enforce formal methods at all the levels? I'm obviously not talking specifics (because I don't know them! ... and you do), but this seems like a failure of process or lack of enforcement of formal methods "all the way down" as it were. I dunno, color me confused...
- wucke13 2y ago
  Which almost reads as a cautionary tale about mechanisms like Dust's `unsafe`. Not necessarily the specifics of the Rust, but the overall idea of having a safe (by whatever means) sunset of operations and and additional unsafe operations, which eases code analysis tremendously. You can't got without unsafe in most embedded systems. But it's good to very explicitly mark in the code wherever the unknown depths of UB lurk if not the most attention is exercised.
  - renox 2y ago
    While this is true, let's not forget that if there's a problem in the unsafe section, the issue can manifest itself much later in the safe code.. I'm not a Rust programmer but I remember reading about such kind of issue (an alignment error if memory serves). So sometimes you can build a 'self contained' unsafe part made safe with the right API but not always, which is already a significant improvement over other languages which are unsafe all the time..