I completely agree! There's lots of crappy but crucial components of networked systems ("the cloud") that we rely upon not to be bugged, that could do with a healthy dose of verification. While the examples you picked are excellent candidates, what's even more fascinating is that even if we only had a few extremely dumb systems verified correct - such as a trusted box that did nothing but provide a verified incrementing counter - that itself is surprisingly useful. The Ironclad paper does discuss this in Section 3.3, but it's worth looking at the description of the TrInc paper as well: http://research.microsoft.com/apps/pubs/default.aspx?id=7836...

Next up should be a Kerberos server, which is a central security controller for high security networks. A major vulnerability in Microsoft's Kerberos server was announced three days ago:

(https://www.us-cert.gov/ncas/current-activity/2014/11/18/Mic...)

"The Microsoft Windows Kerberos KDC fails to properly check for valid signatures in the Privilege Attribute Certificate (PAC) included with the Kerberos ticket request. A domain user may forge the information contained in the PAC to request higher user privileges than should be allowed. Since the KDC does not verify the signature correctly, it will award the user the requested privileges, effectively making the user a domain administrator and allowing complete compromise of the entire domain."

Yes, there's an exploit. Applying the patch isn't enough, either.

"The only way a domain compromise can be remediated with a high level of certainty is a complete rebuild of the domain. An attacker with administrative privilege on a domain controller can make a nearly unbounded number of changes to the system that can allow the attacker to persist their access long after the update has been installed."