> but I'm not aware of a general way of proving no information leakage. As I understand it, the current consensus is to use a tagged architecture, then show th

> but I'm not aware of a general way of proving no information leakage. As I understand it, the current consensus is to use a tagged architecture, then show that there are no observable differences when the tags involve secret data and the value of the tagged data changes. There are a few rubs here. One is that this is pretty hard to do. The other is that no one wants to pay the overhead of using a tagged architecture. Yet another is that deciding what "observable difference" means is challenging (too little, and you probably miss attacks, too much, and you will probably discover information leaks). Further, this kind of rigorous system hasn't been rigorously empirically evaluated by a third party (as far as I know, perhaps in part because it's so hard to create these systems). "Empirically evaluated?" you scoff, "there's a proof, what's the point of testing?" Well... For a glimpse of what this looks like, consider the SAFE architecture: http://www.crash-safe.org/assets/verified-ifc-long-draft-2013-11-10.pdf http://www.crash-safe.org/assets/verified-ifc-long-draft-201... and lowRISC: http://www.lowrisc.org/downloads/lowRISC-memo-2014-001.pdf http://www.lowrisc.org/downloads/lowRISC-memo-2014-001.pdf