Matthew Green’s blog post on the KRACK vulnerability, entitled “Falling through the KRACKs”, makes two points which have come up on the System Safety mailing list frequently.
One is that the IEEE standards business model makes it difficult for researchers to access standards, namely they want you to pay lots of money for them. We have had this discussion many times with regards to the cost of IEC 61508.
Most of the people who have access to IEC 61508 are engineering-company employees whose job does not include (and whose company lawyers may not permit) analysing the standard for flaws and publishing them. Almost none of those with access are researchers at public institutions. The late John Knight had something to say about this in his keynote Safety Standards: A New Approach at the SCSC Safety-critical Systems Symposium 2014, available (*) under open access from the Publications page of the Safety Critical Systems Club WWW site to registered users (registration is free). John observed he couldn’t teach IEC 61508 in his classes because the thing costs over a thousand dollars for one copy and site licences cost five-figure sums which libraries at public institutions do not pay. I can gloss on that from local experience.(**)
Takeaway: the business model of standards is broken. Green points out that this flaw will cost industry lots of money. If access to the WPA2 standard had been easier for curious researchers (there are always PhD students looking for a topic), it might not have taken so many years for this flaw to have been found. (Peter Neumann notes in his Risks piece on KRACK that Steve Bellovin considers the flaw obvious.)
The second point concerns the protocol having been “proven correct” twelve years ago, by He, Sundararajan, Datta, Derek and Mitchell in 2005 (go to John Mitchell’s publications page, search for He, and you’ll see “A Modular Correctness Proof of TLS and IEEE 802.11i, ACM Transactions on Information and System Security” . The conference version is freely available there).
How come a “proven correct” protocol is flawed? The reason is clear to those of us with experience. The standard apparently “defines” the protocol in pseudocode fragments, and there is no specification of the intended state machine (so says Green).(***) So (a) anyone formally analysing the protocol has to interpret the pseudocode, leading to possible variance in interpretation; and (b) where there is incompleteness, formal analysts have to guess what is meant – in other words, assumptions need to be made, and these assumptions may not always hold in all implementations.
Green suggests that the most useful approach to formal analysis is to analyse the source code of the implementation. And he suggests machine proofs, because (he suggests) we are close to the limits of what humans can hand-prove. In other words, he is suggesting the model of protocol software development which has been promoted by companies such as AdaCore and Altran UK (formerly Praxis) for decades now. I can only agree.
Footnotes.
(*) 2017-10-24. Tim Kelly has confirmed that open access is SCSC policy for self-published papers. The WWW site is being so configured and I imagine this might take a little time.
(**) The German electrotechnical standards organisation DKE has a number of repositories around the country in public-institutional libraries where copies of all standards may be accessed for free. One is at the University of Applied Sciences Bielefeld, whose engineering campus is ten minutes walk from the Uni, and next door to the Uni’s CITEC research institute. It nominally has 17 copies of DIN EN 61508 (the German translation of IEC 61508). Not a single one is available to my group members who have tried to access one. 15 of them are just not there, and the other two are on what appears to be semi-permanent loan somewhere. The theory is that university researchers and others have access. The practice is that they don’t.
(***) This substantiates a point close to my engineering heart, and which I have voiced in accord with John. There is no peer review of standards, in the sense of putting a proposed final draft out for independent review. All worthwhile journals do this. The EU subjects each of its research consortia to (paid, multi-day) annual peer review, with reviewers determining whether to accept or reject deliverables (rejected deliverables must be modified until they are accepted). Yet electrotechnical standards organisations are putting out engineering standards with clear weaknesses that one imagines would be picked up easily in qualified independent expert review.