It's really nice work. I have to take issue with something in the paper [1]: “First, hardware-enforced isolation such as the use of SGX or EPT is fundamentally

It's really nice work. I have to take issue with something in the paper [1]: “First, hardware-enforced isolation such as the use of SGX or EPT is fundamentally stronger than software-enforced isolation (containers/software LibOS), as shown by the current trend of running containers within VMs for security” I don’t think that’s true. High-assurance security used to demand products use as many hardware defenses as possible. That was good for a while. Then, the hardware started having serious problems we’d have to work around. They seemed to be screwing them all up at some point with MMU and virtualization working better than average (most tested). Muen went with decision to use just one mechanism to avoid multiple, failure modes with software written in SPARK Ada for verification of safety. It did better with Meltdown/Spectre than many. More problems coming in on HW side, including attacks focused on SGX. I think their assumption is thoroughly refuted at this point for modern, complex hardware. I’d depend on the hardware as little as I can using as simple hardware as I can get away with. Then, build the software as strong as possible around the most battle-tested mechanisms to reduce number of changes needed. seL4 on ARM and Muen on x86 are examples. If one has a massive budget, then build extensions to hardware that make securing software easier. Then, do the same thing again building highly-assured kernels on those heavily-verified, hardware extensions. [1] https://www.ssrg.ece.vt.edu/papers/vee2019.pdf https://www.ssrg.ece.vt.edu/papers/vee2019.pdf