Submit two items to the submission website (see link in the navigation bar at the top of the page):
The designers of the hyperkernel move functions that hard to verify in a push-button approach to user space and don't verify those functions. What is the benefit in verifying the remaining kernel code? That is, what important guarantee does the hyperkernel provide, even though much "kernel" code is in user space?
Questions or comments regarding 6.826? Contact us on Piazza or send e-mail to the 6.826 staff at 6826-staff@lists.csail.mit.edu.