Stupid question: how do correctness proofs handle potentially buggy syscalls which break your assumptions?
No. You have to either assume external stuff behaves in a certain way, or go and actually verify that external stuff.
Which is why proven-correct mutex or semaphore implementation in Rust stdlib actually deadlocks when called recursively: Microsoft's implementation of the relevant OS primitive does not support it.
I was going to ask more questions, but I don't know the first thing about software verification. :speechless: I'm going to go educate myself.
@Zach Reizner solution: use seL4, prove your program correct in Isabelle, and build on their existing Isabelle proofs for seL4 :stuck_out_tongue_wink:
If that was a joke, it went right over my head :sunglasses:
It's a joke. They did 100,000 LoC of proofs for a 1,000 LoC program in C.
it's also the recommended way you develop applications for seL4, heh
...only to get what safe Rust already guarantees, assuming the stdlib and compiler are bug-free
yup, yeah I'm personally in the "write the best Rust I can and hope that's good enough" department for now
I'm really curious about applying SMACK to Rust now that it's been ported but didn't get a chance to really dig into it yet. I guess I'll repost this link in this topic too: http://soarlab.org/publications/atva2018-bhr.pdf - this is an article from the guys who adapted it for Rust and got several programs verified. Seems like it would have caught the latest stdlib CVE too.