3 ms·
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
by nickpsecurity 9y ago
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 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.