This isn't germane to the main topic but this paper they cite about using a compiler pass to verify OS security ("Protecting Applications from Hostile Operating Systems") is pretty darn interesting: http://sva.cs.illinois.edu/pubs/VirtualGhost-ASPLOS-2014.pdf