3 ms·
No, I'm talking about the one I linked to, which is done in Coq.
by samth 9y ago
No, 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.