Stream: wg-secure-code

Topic: correctness proofs

Zach Reizner (Oct 19 2018 at 17:08, on Zulip):

Stupid question: how do correctness proofs handle potentially buggy syscalls which break your assumptions?

Shnatsel (Oct 19 2018 at 17:11, on Zulip):

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.

Zach Reizner (Oct 19 2018 at 17:18, on Zulip):

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.

Tony Arcieri (Oct 19 2018 at 17:20, on Zulip):

@Zach Reizner solution: use seL4, prove your program correct in Isabelle, and build on their existing Isabelle proofs for seL4 :stuck_out_tongue_wink:

Zach Reizner (Oct 19 2018 at 17:20, on Zulip):

If that was a joke, it went right over my head :sunglasses:

Shnatsel (Oct 19 2018 at 17:21, on Zulip):

It's a joke. They did 100,000 LoC of proofs for a 1,000 LoC program in C.

Tony Arcieri (Oct 19 2018 at 17:21, on Zulip):

it's also the recommended way you develop applications for seL4, heh

Shnatsel (Oct 19 2018 at 17:21, on Zulip):

...only to get what safe Rust already guarantees, assuming the stdlib and compiler are bug-free

Tony Arcieri (Oct 19 2018 at 17:22, on Zulip):

yup, yeah I'm personally in the "write the best Rust I can and hope that's good enough" department for now

Shnatsel (Oct 19 2018 at 17:24, on Zulip):

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

Last update: Apr 04 2020 at 03:40UTC