It seems like a good first goal would be to dramatically reduce the size of the code base you need to trust (especially complex code with high privilege), and f

It seems like a good first goal would be to dramatically reduce the size of the code base you need to trust (especially complex code with high privilege), and focus on verifying the correctness of that code base. Then, have fine-grained encapsulation mechanisms for things that do need some level of privilege, and especially avoid conflating "can administer the system" and "can access all user data" levels of privilege. As an example, although one that practically seems to have turned out harder to do than the authors expected, take a look at HiStar: http://www.scs.stanford.edu/histar/ http://www.scs.stanford.edu/histar/