News for hackers. Stuff that matters.

A comment on Writing correct lock-free and distributed stateful systems in Rust, with TLA+. Parent comment

Re:Writing correct lock-free and distributed stateful system... by samth on Friday May 19, 2017 @11:20AM (#14376524)
Right, the concept of the TCB (trusted computing base) is the important thing. Good discussions of remaining TCB in verified code are in the seL4 work, or in this paper: https://www.cs.princeton.edu/~appel/papers/verif-sha-2.pdf
[ Parent | on HN ]
Re:Writing correct lock-free and distributed stateful system... by nickpsecurity on Friday May 19, 2017 @12:32PM (#14377218)
See my link to Myreen's page and follow all those people's publications. Much of the TCB functions in papers like that has been eliminated in other work. It just needs to be cross-checked, integrated, and applied.
[ Parent | on HN ]
Re:Writing correct lock-free and distributed stateful system... by samth on Friday May 19, 2017 @01:58PM (#14377963)
Right, that's one of the nice things about Appel's paper: he shows how to integrate a few different pieces to significantly reduce the TCB (ie, it doesn't include anything about C the language at all).
[ Parent | on HN ]
Re:Writing correct lock-free and distributed stateful system... by nickpsecurity on Friday May 19, 2017 @01:59PM (#14377976)
I think the one you're talking about got the TCB down to a few hundred lines of C. Done in Twelf.
[ Parent | on HN ]
Re:Writing correct lock-free and distributed stateful system... by samth on Friday May 19, 2017 @05:34PM (#14379521)
No, I'm talking about the one I linked to, which is done in Coq.
[ Parent | on HN ]
Re:Writing correct lock-free and distributed stateful system... by nickpsecurity on Friday May 19, 2017 @09:15PM (#14380486)
Oh my bad. I just saw work such as seL4 then assumed it was a seL4 reference. I actually didn't have this one by Appel. Thanks for the paper! :)

Here's the one I was referencing with the tiny TCB:

https://www.cs.princeton.edu/~appel/papers/flit.pdf

OK. So, it was a few Kloc. Still smaller than Coq. They could probably get it even smaller with recent work given translation validation knocks compilers out of TCB. So, in between 803-2668loc.

[ Parent | on HN ]