3 ms·
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 inclu
by samth 9y ago
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).
- nickpsecurity 9y agoI think the one you're talking about got the TCB down to a few hundred lines of C. Done in Twelf.
- samth 9y agoNo, I'm talking about the one I linked to, which is done in Coq.
- nickpsecurity 9y agoOh 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 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.