There's actually been a lot of work in that going back five years or so. Here's a commercialized one: http://www.ccs.neu.edu/home/pete/acl206/slides/hardin.pdf

There's actually been a lot of work in that going back five years or so. Here's a commercialized one: http://www.ccs.neu.edu/home/pete/acl206/slides/hardin.pdf http://www.ccs.neu.edu/home/pete/acl206/slides/hardin.pdf Formal verification of specs, microcode, and security policy they hold in ACL2. Part of that is embedding a separation kernel a la MILS or SKPP model. It also has triplicated registers for fault-tolerance. Then, they integrate high-level languages like SPARK and microCryptol with that using certified compilers or equivalence checking. Here's some examples from CompSci work: https://eprint.iacr.org/2016/846.pdf https://eprint.iacr.org/2016/846.pdf http://users.ece.utexas.edu/~tiwari/pubs/tiwari-dissertation.pdf http://users.ece.utexas.edu/~tiwari/pubs/tiwari-dissertation... http://cs.ucsb.edu/~sherwood/glift/ http://cs.ucsb.edu/~sherwood/glift/ http://ieeexplore.ieee.org/document/7927266/ http://ieeexplore.ieee.org/document/7927266/ http://www.eecs.ucf.edu/~jinyier/papers/VTS12.pdf http://www.eecs.ucf.edu/~jinyier/papers/VTS12.pdf http://www.cse.psu.edu/~dbz5017/pub/asplos17.pdf http://www.cse.psu.edu/~dbz5017/pub/asplos17.pdf Just also found a super-old one that tries to do it with capability-based mechanisms. https://dl.acm.org/citation.cfm?id=803030 https://dl.acm.org/citation.cfm?id=803030 Most hardware work in information-flow analysis and control is currently focused on making hardware that controls bad software. I don't think most of them consider a CPU failure. If anything, they might be more vulnerable from a practical strategy of trying to reuse existing cores by making info-flow components that operate side-by-side with them. Here's an example from that area, though, since they could be modified to address recent concerns. http://www.crash-safe.org/assets/verified-ifc-popl2014.pdf http://www.crash-safe.org/assets/verified-ifc-popl2014.pdf http://csl.stanford.edu/~christos/publications/2010.hari_kannan.phd_thesis.slides.pdf http://csl.stanford.edu/~christos/publications/2010.hari_kan...