Liudvikas Bukys

Security researchers successfully forge a CA certificate, allowing them to produce new certificates that will be trusted by every browser:

MD5 considered harmful today
Creating a rogue CA certificate
Alexander Sotirov, Marc Stevens,
Jacob Appelbaum, Arjen Lenstra, David Molnar, Dag Arne Osvik, Benne de Weger

We have identified a vulnerability in the Internet Public Key Infrastructure (PKI) used to issue digital certificates for secure websites. As a proof of concept we executed a practical attack scenario and successfully created a rogue Certification Authority (CA) certificate trusted by all common web browsers. This certificate allows us to impersonate any website on the Internet, including banking and e-commerce sites secured using the HTTPS protocol.

Our attack takes advantage of a weakness in the MD5 cryptographic hash function that allows the construction of different messages with the same MD5 hash. This is known as an MD5 “collision”. Previous work on MD5 collisions between 2004 and 2007 showed that the use of this hash function in digital signatures can lead to theoretical attack scenarios. Our current work proves that at least one attack scenario can be exploited in practice, thus exposing the security infrastructure of the web to realistic threats.

Now that it’s been demonstrated once, it won’t be long before someone malevolent does it too. One hopes that, by then, software desupporting MD5-based signatures will have been widely distributed, and certificates containing them will have been retired.

Update: Of course, the day of doom can be postponed by getting every MD5-cert-issuing CA to immediately update their software to: (a) stop issuing MD5-based hashes, or, at least, (b) make their certificate serial numbers less predictable. The latter is a fairly small change. Is it too much to hope for?

Alan Shostack points out that
Alan Drexler is excited about the interesting AMS survey article
“Formal Proof” (Hales)
because of the prospects for program verification.

I think the article is better at inspiring hope about computer verification of proofs than about proof system verification of computers.

For balance one should read the still-persuasive May 1979 paper
“Social processes and proofs of theorems and programs” (De Millo, Lipton, Perlis).
The abstract:

It is argued that formal verifications of programs, no matter how obtained, will not play the same key role in the development of computer science and software engineering as proofs do in mathematics. Furthermore the absence of continuity, the inevitability of change, and the complexity of specification of significantly many real programs make the formal verification process difficult to justify and manage. It is felt that ease of formal verification should not dominate program language design.

(Note that that there are lots of copies cached around the web if you don’t have an ACM Portal subscription.)