"What I understand there verified is however not that the adversary can't add malicious code but that there are formal verification steps that no bugs are intro

"What I understand there verified is however not that the adversary can't add malicious code but that there are formal verification steps that no bugs are introduced as the non-subverted implementation is introduced." What they did is a high-level view (formal spec) of exactly what it does, one of what it means to be secure, and proof the design matches that. It's harder to subvert. It can also prove the system can't be attacked if they model those properties. For instance, they do show some protection against leaks from one process to another with the non-interference property of their partitioning mechanism. I just posted a lot more stuff like that in hardware and software here if you're interested: https://news.ycombinator.com/item?id=17530829 https://news.ycombinator.com/item?id=17530829 " the way I see it, the accidental errors that introduce security issues are much more probable in compilers and the modern linkers (especially as they do more of a job that formerly only compilers did) than in assemblers." I agree. I bring it up every time someone erroneously focuses on the Karger/Thompson attack on compilers. The more common error is the compiler messing the code up. An easier subversion would be to put a bug into a compiler that did that which looked like a normal bug. It's why certifying compilers are necessary. Note that TALC is part of a bigger picture at FLINT team where they do certifying compilers for stuff like ML, safe versions of C, intermediate/assembly languages that are typed for extra layer of defense, I/O, interrupts, and many other things. Here's their work: http://flint.cs.yale.edu/flint/publications/ http://flint.cs.yale.edu/flint/publications/ http://flint.cs.yale.edu/flint/software.html http://flint.cs.yale.edu/flint/software.html Yeah, assemblers should be pretty easy if they're just doing straight-forward stuff preserving the data and structure. Those like Hyde's High-Level Assembly (HLA) might be trickier with high-level functionality. However, even those might be divided between a first-pass acting as a compiler for high-level stuff and a simpler assembler.