15 ms·

Falling through the KRACKs

462 points by kjhughes 9y ago

goalieca 9y ago
> As the KRACK paper points out, there is no formal description of the 802.11i handshake state machine. This, to me, is one of the biggest problems facing our industry. In first year undergraduate in engineering we learn how to design a state machine. We learn to design one before we learned OOP and circuits and assembly. Yet, how many APIs or Protocols have you come across or has your organization developed where there isn't a state machine described somewhere. It may seem difficult and tedious, but this is how you engineer something rather than merely 'develop' it. We programmers sometimes spend far too much time juggling stuff in our heads and communicating with coworkers in a wonderful game of workplace telephone. If the state machine has become too complex, then we have lost all hope to fully manage it and must accept the risks. Some things just shouldn't be risked!
- eradicatethots 9y ago
  It is tedious. It’s inefficient. Quality software usually is less important than working software.
  - maldeh 9y ago
    Unless I'm misinterpreting the meaning of "usually" or "important", I find this comment a little bewildering in the context of the article.
    - katastic 9y ago
      In the working world, what matters is you ship. The most beautiful code and best "game ever designed" means nothing if it doesn't ship. Additionally, in my years of working as a contractor, I can tell you that nearly 1 in 1,000 companies (+ or - 1) care about security. Management simply does not value it, and everyone already thinks your product "should have been done yesterday." The entire world runs on insecure products. From banks, to healthcare, to universities. I can list every one of those who has put admin credentials in a publicly, internet accessible text file. (But they'll do silly things like insanely unmemorizable passwords like 23ix2n5 that get written down as postit notes and as files on desktops, and disable RDP copy-and-paste but leave RDP hard drive support.) We're going to continue seeing these blunders day after day until people start going to jail for losing data.
      - digi_owl 9y ago
        Or stop treating programming like some grand joust...
        TeMPOraL 9y ago
        We won't. Worse is better, remember? Especially when a typical company wants to be the first to quickly sell some shit product and then, maybe, they'll patch it for a while as they go along. Competitive pressures (and management fads, IMO - software market ain't that efficient yet) turned "good solution today > perfect solution next week" into "steaming pile of garbage today > good solution tomorrow". I guess this is fine for throwaway acquihire SaaS stuff, but it's becoming a serious problem for stuff that's meant to be widely used.
    - emmelaich 9y ago
      Consider it descriptive rather than prescriptive.
  - InclinedPlane 9y ago
    Can you think of any particular circumstances where quality would be of paramount importance? I'll wait.
    - jdhendrickson 9y ago
      Pacemaker firmware comes to mind.
      - colejohnson66 9y ago
        You’d think: https://arstechnica.com/information-technology/2017/08/465k-patients-need-a-firmware-update-to-prevent-serious-pacemaker-hacks/ https://arstechnica.com/information-technology/2017/08/465k-...
  - criddell 9y ago
    I've been working in the same code base one way or another for more than 20 years now. Quality is underrated.
- userbinator 9y ago
  This, to me, is one of the biggest problems facing our industry. In first year undergraduate in engineering we learn how to design a state machine. We learn to design one before we learned OOP and circuits and assembly. I think one of the causes is that a lot of CS is taught top-down and not bottom-up, so things like flowcharts, state diagrams, and other similar visual aids are completely skipped in preference to more abstract thinking. I wonder if at least some of this aversion is directly related to the "gotophobia" that started with Dijkstra's famous paper. It may seem difficult and tedious, but this is how you engineer something rather than merely 'develop' it. As someone who learned the "old school" way of planning out your code --- yes, even drawing flowcharts and state diagrams --- before writing a single line of it, I can assuredly say that it should be a natural and completely pleasant process; what's "difficult and tedious" is trying to debug and coerce something you (or someone else) wrote without planning into working correctly. Over the years coworkers have been puzzled at why I spend "so much time" flowcharting and just thinking before writing even a single line of code --- only to try adopting the same method once they realise how much time it saves in total, since all the cases have already been accounted for and the only thing left to do is test out any of the few remaining and often trivial bugs introduced during the design->code process.
  - digi_owl 9y ago
    It also takes all the "fun" out of programming, as so many seems to approach it like some grand display of mental prowess. Never mind the whole "agile" thing...
    - reitanqild 9y ago
      You can look at this both ways actually: For some people (like me) thinking through problems with pen and paper is a tool. For others I guess it is annoying: look at him, now he's doing this wannabe software architect stuff again. Same might go the other way: here he goes again, trying to prove his programming super skills by jumping into it without even the smalles amount of planning.
      - Swizec 9y ago
- foobarian 9y ago
  I find it interesting how in a large codebase or project there is a temptation to mutate an object here, decorate some intermediate object there, and before you know it you have an ugly state machine hiding in your code. As you know the number of possible states grows very fast and when people don't know this is happening things soon get out of control. Having things immutable by default helps somewhat, but it's still easy to add various decorators.
- technion 9y ago
  I guess a related question would be, is anyone aware of a common protocol that does have a formally defined state machine to review?
  - scott_karana 9y ago
    TCP's might not be formally defined (unsure), but it's pretty well understood to the point of having de facto ones, at least.
    - userbinator 9y ago
      There are state diagrams in the TCP RFC --- in ASCII art, so the authors clearly really wanted to have one.
      - scott_karana 9y ago
        Nice! Good to know. That must be the origin of all the useful but unofficial SVG ones I'd seen :)
  - lsh123 9y ago
    SSL
    - tom_mellior 9y ago
      Here is really cool work on state machines in TLS: https://www.smacktls.com/smack.pdf https://www.smacktls.com/smack.pdf Beurdouche et al., "A Messy State of the Union: Taming the Composite State Machines of TLS" From the abstract: "mplementations of the Transport Layer Security (TLS) protocol must handle a variety of protocol versions and extensions, authentication modes and key exchange methods, where each combination may prescribe a different message sequence between the client and the server. We address the problem of designing a robust composite state machine that can correctly multiplex between these different protocol modes. We systematically test popular open-source TLS implementations for state machine bugs and discover several critical security vulnerabilities that have lain hidden in these libraries for years ..." Based on this work you might say that there are formal state machines for TLS, but they aren't in the standard.
- bdcravens 9y ago
  > It may seem difficult and tedious, but this is how you engineer something rather than merely 'develop' it. Don't agile approaches encourage this, focusing on features and things that can cleanly be assigned story points at the expense of a bigger picture, with velocity being the focus?
  - maskedSlacker 9y ago
    It seems to me that agile approaches are a response to the phenomena of the spec often being wrong. If the spec is wrong and going to need substantial revision, iteration is better than planning. If the spec is not wrong, careful planning is probably better than high velocity iteration. I think cryptography is a good example of this--would you develop a cryptographic API on which people's lives might depend iteratively through a release early and fail often method? I hope not.
    - taneq 9y ago
      Exactly, and this is why Agile (while grand for things like "The customer wants a web site. They don't know what they want or how they want it to look, but we need to start on Tuesday.") isn't the be-all and end-all that it's advertised to be by people who only work on websites for tech-illiterate customers. In a lot of software development, especially large scale enterprise software (where you're trying to map a complex set of existing business practices and workflows into software) and embedded software (where you have to write something that provides fixed, well-understood functionality running on hardware with a months- or years-long iteration time) you do have a complete and correct spec (or at least the means to generate one). In these cases a less ad-hoc approach than Agile can be beneficial.
    - arohner 9y ago
      I upvoted this, but agile and "release early and fail often" aren't necessarily the same thing. For example, they could have iterated quickly during the draft phase, come up with a proposed implementation, have the security researchers review it, and iterate.
- NamTaf 9y ago
  Compare front-end [1] design philosophies (such as used in waterfall development) vs iterative design philosophies (such as in agile development). As a non-software, 'real world' engineer (mechanical, heavy industry design) looking in from the periphy of computing as a hobby/amateur interest, it appears to me like software engineering as a discipline has sort of forgotten about why and when FEED is appropriate and, critically, how to implement it when it is. Let's reflect: iterative design is popular in software engineering because software usually suits it. Changes are easily iterable, you can often roll changes back, there's relatively low cost to cloning changes across millions of instances, code's design lifetime is relatively short, etc. In contrast, 'real world' engineering (civil, heavy mechanical) favours FEED because the cost of change rapidly and prohibitively rises with time, so nailing down the scope and structure early is critical, there's long procurement times for changes, the design lifetime of the finished product is measured in decades, etc. The rub is that there's a small niche of software design, such as protocol design like this, or certain firmware scenarios, which far more closely resembles the latter even though it's usually done by a community used to and trained in the former. Although it's for different reasons, all the things that make FEED appropriate for 'real world' engineering also apply to these sorts of software tasks, but software engineering as a whole doesn't appear to[2] focus on teaching and supporting the necessary tools and techniques for performing that process well. Flip that on its head, and it's why software companies quickly begin to run rings around companies traditionally focused on hardware once software starts to play a bigger part and the limitations stopping iterative design from working begin to disappear. Software engineering largely biases towards iteration (understandably) and when it works it allows for good advantages. But in embracing those advantages, software engineering as a discipline has begun to lose an understanding of FEED and the careful methodology it delivers. [1]: https://en.wikipedia.org/wiki/Front-end_engineering https://en.wikipedia.org/wiki/Front-end_engineering & https://en.wikipedia.org/wiki/Front-end_loading https://en.wikipedia.org/wiki/Front-end_loading [2] I admit I've not done a CS/SE degree, but I've gone through a couple of subjects run online and I talk to friends who did do it and that's the feel I get. Besides, just look at HN's generally trending articles. edit: With all I wrote, I don't mean to undermine the extremely good work that the devs designing these protocols, etc. almost always perform. It's far beyond my ability. I am speaking more in a general sense about how Soft. Eng. seems to have thrown out the baby with the bathwater in declaring agile philosophies as 'the best way'. My feel is that the pendulum seems to have swung too far past 'best' towards becoming 'only'.
- pfortuny 9y ago
  Either engineering and its tools (eg state machines) or just craftmanship. Totally right.
- pron 9y ago
  > there is no formal description of the 802.11i handshake state machine. Here is what the paper actually says: The 802.11i amendment does not contain a formal state machine describing how the supplicant must implement the 4-way handshake. ... Fortunately, 802.11r ... does provide a detailed state machine of the supplicant. The problem, as I understand it, was that when the protocol was formally verified, the properties checked were only the escape of the private key and identity related issues. The property of the nonce never being reset was simply not considered. The missing piece, then, wasn't a precise description of how the system works, but rather a precise list of what it's supposed to guarantee. Without a clear and concise description of the requirements, it's hard to verify that the system satisfies them. Alternatively, it's possible that the list of guarantees was complete, in which case reviewers should have noticed that no nonce reset isn't one of them, yet it's required for the security of certain communication protocols used over the channel.
oconnore 9y ago
> In the end we all know that the answer is for humans to stop doing this work. We need machine-assisted verification of protocols, preferably tied to the actual source code that implements them. This would ensure that the protocol actually does what it says, and that implementers don’t further screw it up, thus invalidating the security proof. And yet, there are still regular posts here about whether static type systems have any merit at all... never mind advanced things like linear/dependent types, theorem provers, TLA+, etc. Just use Go!
- munin 9y ago
  We did formally verify the 802.11i protocol, though: https://link.springer.com/article/10.1007%2Fs12204-009-0122-3?LI=true https://link.springer.com/article/10.1007%2Fs12204-009-0122-...
  - scott_karana 9y ago
    And the implementations ignored all the fundamental "nonces should never be used" part of the formal handshake protocol, and thus would have failed the aforementioned testing.
  - tom_mellior 9y ago
    Question about this, because the featured article strangely doesn't actually say what the problem is: Did this verification result simply forget/not consider nonce reuse? The article seems to imply there's nothing wrong with the proof or the statement of the properties to be proved, it's about integration with another component. But if "don't reuse nonces" is a standard security property to verify, then I would think that that is a hole in the verification. Could someone shed more light on this?
    - kruczek 9y ago
      It is covered in Q&A at https://www.krackattacks.com/#faq https://www.krackattacks.com/#faq - basically the proof didn't cover this particular scenario: > The 4-way handshake was mathematically proven as secure. How is your attack possible? > The brief answer is that the formal proof does not assure a key is installed once. Instead, it only assures the negotiated key remains secret, and that handshake messages cannot be forged.
userbinator 9y ago
More importantly, even after the fact, they’re hard for ordinary security researchers to access. Go ahead and google for the IETF TLS or IPSec specifications — you’ll find detailed protocol documentation at the top of your Google results. Now go try to Google for the 802.11i standards. I wish you luck. The first result for "802.11i" is the Wiki page for IEEE 802.11i-2004, which mentions that it's incorporated into 802.11-2007, and if you search for "802.11-2007", the first result at the top (after the amusing calculation that 802.11 - 2007 = -1 204.89) is the PDF of the full standard. ...and I'm not even a security researcher. But I agree with the rest of the criticism of the IEEE and the 802.11 standard in particular, once you've acquired it. One of my pasttimes is seeking out and reading standards for protocols, file formats, and other things; and so I've seen quite a few. As an overall impression: IETF's are very readable, most of the ITU ones are pretty good if somewhat terse, ANSIs and IEEEs vary widely between "a little bit of effort" and "I feel like my brain is melting if I read more than a paragraph an hour", and 3GPPs along with BlueTooth are very much in the "take a 10 minute break to digest after every sentence or two" category. 802.11 is also like that. The acronym density in that document is one of the highest I've ever seen. Maybe KRACK will at least make them consider editing their standards and formatting them to be somewhat less of a chore to understand; things like https://files.catbox.moe/xym9dq.PNG https://files.catbox.moe/xym9dq.PNG should really be put into tables.
- thezilch 9y ago
  And then he wrote... The IEEE has been making a few small steps to ease this problem, but they’re hyper-timid incrementalist bullshit. There’s an IEEE program called GET that allows researchers to access certain standards (including 802.11) for free, but only after they’ve been public for six months — coincidentally, about the same time it takes for vendors to bake them irrevocably into their hardware and software. In other words, it's getting better, but vendors are burning silicon by the time researchers have the time to even crack open whitepapers -- too late.
  - colejohnson66 9y ago
    Why is there a delay at all? If they’re a security researcher, it would make sense to allow them access as soon as possible.
cyberferret 9y ago
Just to clarify a question I had when reading about KRACK - If you are using a VPN over WiFi, you still have some degree of safety, right? Any way that the KRACK vulnerability can be elevated to sniff and decrypt VPN packets in transit?
- wskinner 9y ago
  Yes. It appears that since KRACK can allow the attacker to hijack a TCP handshake that they could potentially downgrade an HTTPS connection where HSTS is not used, but that shouldn’t affect your VPN connection.
  - iancarroll 9y ago
    To be clear, if a client makes an HTTPS request, you cannot downgrade it to HTTP, even if you're in control of the TCP socket. You can only hijack connections that are initially made over HTTP.
    - wskinner 9y ago
      In fact, you can, using sslstrip. It was demonstrated in the video, as well as in this article: https://arstechnica.com/information-technology/2017/10/severe-flaw-in-wpa2-protocol-leaves-wi-fi-traffic-open-to-eavesdropping/ https://arstechnica.com/information-technology/2017/10/sever.... I think this will only work against android/linux clients, since in that case the attacker actually knows the key, and can perform a proper MITM.
      - iancarroll 9y ago
        You cannot. sslstrip exists to attempt to work around the fact you can't directly downgrade HTTPS to HTTP. In that video, because HSTS isn't used on match.com (unfortunate), the browser doesn't attempt to make an HTTPS connection at first. Obviously, if you have control of that TCP connection, you can do whatever you want. The browser is oblivious to HTTPS existing. Also, be careful not to confuse the layers here. The encryption algorithms in WPA2 are completely unrelated to TLS/HTTPS. TLS is... somewhere in the OSI model, but it's well above WPA2/packet handling, and TLS can/does work with a compromised network.
a3_nm 9y ago
One thing I don't understand about this attack is whether it allows the attacker to connect to the Wifi network (in the style of airmon-ng for WEP), or whether the attacker can only decrypt packets of legitimate users. Has anyone figured this out?
- M4v3R 9y ago
  This attack doesn't expose Wi-Fi network key, so I assume it doesn't let you join the network, just sniff the traffic of the targeted user (and also, in some cases, forge/inject packets).
- grive 9y ago
  This attack is a MitM. The attacker is able to act as the access point and receive the victim's traffic, unencrypted. He is also able to modify this traffic and serve compromised pages. The attacker needs to have a stronger signal than the legitimate access point. So he has to stand pretty close to the victim, physically.
  - blauditore 9y ago
    But still, this is only problematic if you "trust" an access point. If you treat any wifi network like a public hotspot (i.e. potentially rogue), there's not much of a difference, right? In practice, as long as you only trust data received through TLS, you should be fine.
    - rocqua 9y ago
      Do you not 'trust' your home wifi router?
      - Retr0spectrum 9y ago
        Personally I don't, because my ISP owns it.
      - blauditore 9y ago
        Well, I don't trust whole the network (internet) in general, as I don't know where and how things are routed, and by whom. The only situation where trust in the router would be relevant to me is for communication within a local network, so I'm controlling every device involved. And there, this attack might actually be harmful, as far as I understand.
dmitriid 9y ago
Re-read this article every time when you come across yet another blog post or article extolling the virtues of formall proofs, verifications, and, while we’re at it, static typing. None of these work when taken in isolation and given to actual people to work with.
- TeMPOraL 9y ago
  On mobile and imgur refuses to work on my Fx, so won't post a screenshot. So just imagine how funny yours and oconnore's [0] comments look next to each other... So, which way is it? [0] - https://news.ycombinator.com/item?id=15488391 https://news.ycombinator.com/item?id=15488391
  - ktta 9y ago
    If you look around, the problem touted here was that formal verification was done, but independently for two different parts of the standard, in isolation. The layman answer that is formal verification should've been done on those systems after integration. I'm not sure how much that would've helped though, since the proofs for each of those was complex enough. And then actual code written tends to sway far away from what protocol implementers (also crypto folks) think it should look like. So I'd say more formal verification, but also make it easier and accessible for normal developers without a Math PhD. And verification of actual code would be ideal. Something I've come across recently is formal verification of cryptographic implementations not on paper (i.e. mathematically) but in plain C using tools and languages developed recently. For example, a three part series on how SAW and Crytol were used to formally verify s2n (AWS's TLS lib): https://galois.com/blog/2016/09/verifying-s2n-hmac-with-saw/ https://galois.com/blog/2016/09/verifying-s2n-hmac-with-saw/ https://galois.com/blog/2016/09/specifying-hmac-in-cryptol/ https://galois.com/blog/2016/09/specifying-hmac-in-cryptol/ https://galois.com/blog/2016/09/proving-program-equivalence-with-saw/ https://galois.com/blog/2016/09/proving-program-equivalence-... PS(A) for the adventurous: I've also come across a github repo that lists related stuff https://github.com/enzet/symbolic-execution https://github.com/enzet/symbolic-execution
  - dmitriid 9y ago
    The protocol was formally verified. And yet...
vikiomega9 9y ago
I don't understand how the attacker can block step 3 of the handshake from the client. Can someone ELI5? What I was able to understand so far is that the use of a particular nonce is being forced on the client and given that invariant keystream one can decrypt known messages. I'm still fuzzy on how the attacker can force this step. EDIT: Further question, isn't timestamp synchronization taken into account here when invalidating a nonce? What happens when I disconnect from wifi to a mobile network and back to the wifi?
- rocqua 9y ago
  The attacker gets a Man in the Middle position on layer 2 (data link). So every step in the handshake goes through the attacker. The attacker couldn't just MitM the protocol on layer 3 as it cannot authenticate with the WiFi router. Of course, the attacker already could just pretend to be the wifi router and then forward and inspect all traffic to the internet. What is scary here is that it breaks into a Local network as opposed to the internet.
- cesarb 9y ago
  From what I understood, there are two ways to block step 3. The most obvious way is to jam it, that is, send noise at the same time so the radio fails to receive it. The other way (and the one which makes attacks easier) is to pretend to be the AP but in another channel. Suppose the real AP is on channel 1. The attacker is nearer the victim than the AP, and is on channel 6. The attacker repeats on channel 6 everything the AP sends on channel 1, and repeats on channel 1 everything the victim sends on channel 6. The victim sees the same AP on both channels, channel 1 and channel 6 (the attacker modifies the part of the AP beacon/responses which says "I'm on channel X"), which is a perfectly legitimate and normal thing, and chooses channel 6 because it has a stronger signal. Since now the attacker is in the middle, it can modify anything. Change the AP beacon to say "I'm on channel 6", drop any packet it wants, duplicate any packet it wants, and so on. > What happens when I disconnect from wifi to a mobile network and back to the wifi? The wifi negotiation starts from scratch, with a new step 1.
  - vikiomega9 9y ago
Perceptes 9y ago
Question for the HN mods: I submitted this same article earlier: https://news.ycombinator.com/item?id=15483452 https://news.ycombinator.com/item?id=15483452 Why was this one able to be submitted instead of just redirecting to my submission?
- Jedi72 9y ago
  The quality of this title is terrible as well, the title should say 'Vulnerability in WiFi handshake discovered, its name is KRACK'
- tonyztan 9y ago
  I have the same question. I tried to submit this same article last evening and got redirected to Perceptes' submission. I'm curious as to what happened?
deleted 9y ago
[deleted]
deleted 9y ago
[deleted]
askvictor 9y ago
Can someone clarify if wpa2-enterprise with radius auth is affected? I have seen assertions both ways.
- GenericsMotors 9y ago
  It is affected. Note that this isn't an exploit that allows the attacker to discover the encryption key or connect to the AP by getting around an authentication scheme (such as radius). The attacker impersonates an existing AP and forces the client to reuse IVs / reset the encryption key to zero (in the case of wpa_supplicant), and is able to decrypt traffic that way.
  - PakG1 9y ago
    Yes, but stupid question. If Radius is being used, there's no way to successfully impersonate the AP and have the victim accidentally try to join it because the AP won't be able to authenticate the WPA2-Enterprise credentials? Then the attack fails? Or silly me, the fake AP could be configured to somehow accept the login attempt by the victim? But if so, then it'd be able to record the login credentials thus making the attack's impact even larger than I've seen discussed, because then not only is the attack successful in decrypting the victim's traffic, but the victim's Wi-Fi credentials are also stolen?
    - GenericsMotors 9y ago
      > If Radius is being used, there's no way to successfully impersonate the AP and have the victim accidentally try to join it because the AP won't be able to authenticate the WPA2-Enterprise credentials? From what I understand the credentials won't matter. Anyone else more knowledgeable please correct me if I'm wrong, but the attack goes something like this: 1. Capture trafic that includes the 4-way handshake 2. replay message #3 of the handshake 3. client's encryption key is set to zero (in the case of wpa_supplicant), and nonce/IV are reused going forward 4. you are now in control of the encryption key being used (again, only wpa_supplicant) so you can go ahead and MITM the victim's DNS queries, capture cookies, etc... The Details section of the researcher's site explains it pretty well: https://www.krackattacks.com/#details https://www.krackattacks.com/#details Lastly, the most urgent task for mitigating this is to patch client devices as quickly as possible. Android's fractured vendor-specific distributions and lack of long-term support for the low-mid level models is going to make this a difficult/impossible task...
qznc 9y ago
This seems so overhyped? Why do you care about encrypting the step from device to access point? If you have sensitive data, then you must encrypt end-to-end anyways, because there are a lot more steps between access point and destination. Thus, HTTPS or Signal or PGP or whatever is enough and WPA does not matter.
- mhandley 9y ago
  That might be true if we had secure DNS deployed. But we don't, so using this attack, DNS cache poisoning is pretty easy. And if you can subvert DNS, you can redirect HTTPS traffic to a typosquatted version of a website. Unless you check the URL bar every time you visit an HTTPS website that is in your bookmarks, you'll probably not notice, and there goes your password in the clear across a nice secure end-to-end encypted HTTPS connection to the bad guy.
  - NoGravitas 9y ago
    Modern browsers are very vociferous about not connecting to https sites with certificate errors. So while DNS cache poisoning with this attack is Very Bad, unless the attacker can insert a bad CA certificate in your browser, or has a valid but improperly-obtained certificate for the website in question, you're not going to fail to notice that something janky is going on.
  - PinguTS 9y ago
    And that is actually what the author of KRACK has presented. He re-directed as MTIM via DNS to a different site.
- PinguTS 9y ago
  There are many services in your local network, which are un-encrypted. Any basic protocol that is in the lower layers required to run the infrastructure like ARP, DHCP, DNS, and alike. Then there are also higher layer protocols, which are un-encrypted like SMB, AFP, NFS, and alike. Many IoT devices, like your Cisco Phone talks TFTP at startup. That is the reason why we have/had WEP, WPA, WPA2 to allow a local infrastructure to have the very same trust like physical cables.
z3t4 9y ago
I love the image with the kitchen drawers ... It passed the linter, it passed the type checks, it passed the unit tests ...
cesarb 9y ago
> There’s an IEEE program called GET that allows researchers to access certain standards (including 802.11) for free, but only after they’ve been public for six months Also, that program only allows access to the latest release of each standard. Which means that, when there's a new release of a standard, access to any version of it is closed for six months.
acqq 9y ago
Funny how 2013 discoveries are tried to be forgotten and not mentioned: https://www.theguardian.com/world/2013/sep/05/nsa-gchq-encryption-codes-security https://www.theguardian.com/world/2013/sep/05/nsa-gchq-encry... "$250m-a-year US program works covertly with tech companies to insert weaknesses into products" "The documents show that the agency has already achieved another of the goals laid out in the budget request: to influence the international standards upon which encryption systems rely." [emphasis mine] Now compare with the details from KRACK regarding Android and Linux: https://www.krackattacks.com/#details-android https://www.krackattacks.com/#details-android "Our attack is especially catastrophic against version 2.4 and above of wpa_supplicant, a Wi-Fi client commonly used on Linux. Here, the client will install an all-zero encryption key instead of reinstalling the real key. This vulnerability appears to be caused by a remark in the Wi-Fi standard that suggests to clear the encryption key from memory once it has been installed for the first time." [emphasis mine] Sometimes adding an innocent-appearing remark, and later acting on it would be all that's needed for a rich and mighty adversary. I don't claim it happened this time, but I worry when the possibility isn't being considered and properly investigated.
agentultra 9y ago
From TFA "And separately, to answer a question: how did this attack slip through, despite the fact that the 802.11i handshake was formally proven secure?" Implies that the formal verification failed. Yet from the paper on the attack: "Interestingly, our attacks do not violate the security properties proven in formal analysis of the 4-way and group key handshake." This is a good thing! One of the hard things for software developers to do is separate the theorem (spec) from the proof (implementation). I can see how the article author would posit such a question. The paper answers the question. What do we do about it? More theorems, modelling, and proofs. Research on synthesizing the implementation from its specification. Treat events like this as we treat auto-collisions and correct the processes, tools, and technology that enable attacks like this to occur in our systems... at least that's my 0.02. :)
danib31 9y ago
Definitely another big issue, inherent to cryptography (and maybe matematics in general), is the subtelty of creating the appropriate definitions. As the post says, they thought about the individual components, but failed (or maybe it is just too difficult) to define the security considering composability of schemes. This is a clear limitation of modern cryptography. Great post!
cryptonector 9y ago
This whole process is dumb and — in this specific case — probably just cost industry tens of millions of dollars. It should stop. Bingo. A pay-for-play standards development organization should charge to _participate_ in the standards-setting activity, and NOT charge the public for access to the standards. The ITU-T seems to have learned this, at least as to some things (e.g., the ASN.1 family of standards, such as x.680 and x.690). The IEEE should do the same. Better yet, they should look at the IETF model, which has been working for _decades_. In the IETF model there is no charge at all, except for attending physical meetings. Mailing list participation is free. RFC publication is free. The IETF is financed via meeting fees and donations. Vendors have an interest in the IETF staying afloat, so they see to it -- their interest is, of course, the IETF's overall low cost to them (by comparison to OASIS, IEEE, ANSI/ISO, or the ITU-T), and the amount of review their specifications get. Maybe 802.x dev should move to the IETF lock stock and barrel, you might say, but there is a problem: the IETF doesn't have a lot of expertise with physical layer protocol specifications. _Most_ IETF participants are at layer 2 and up. Of course, this can be fixed by... just moving all the 802.x work (and the people working on it) to the IETF. EDIT: Mind you, getting the work done at the IETF would not be a guarantee of no such bugs. It would address the procedural and public access problems TFA talks about. But that alone is a huge improvement over using the IEEE for highly consequential specifications that greatly affect the public.
- pc2g4d 9y ago
  I recently found the need to understand the 802.11 standards in detail and was shocked to discover how difficult it is to access IEEE standards. I even work for $BIGCORP, with institutional access to various IEEE publications, but 802.11 isn't part of our subscription. I'd venture a guess that much of 802.11's security is by way of obscurity.
cryptonector 9y ago
This will provide further impetus for not using CCM/GCM and similar AEAD cipher modes in any context other than octet stream protocols (e.g., TLS, but _not_ DTLS). There is ongoing work to produce AEAD cipher modes that do not fall apart when {key, nonce} pairs are reused (for different message plaintexts, naturally). Crypto is tricky... It's easy enough to construct AEAD cipher modes by generic composition that don't have this problem. For example, the Kerberos enctypes don't. The key is to construct AEAD cipher modes that are efficient (Kerberos' add a block's worth (16 bytes) of "confounder" to each message, bloating it, and also adds a block's worth of cipher operation, slowing it down) and don't require additional random numbers if at all possible (those confounders in Kerberos are random numbers prepended to the plaintext). Also, Kerberos' enctypes use HMAC for the integrity protection part, which is not a very fast MAC.

462 points by kjhughes 9y ago

> As the KRACK paper points out, there is no formal description of the 802.11i handshake state machine. This, to me, is one of the biggest problems facing our industry. In first year undergraduate in engineering we learn how to design a state machine. We learn to design one before we learned OOP and circuits and assembly. Yet, how many APIs or Protocols have you come across or has your organization developed where there isn't a state machine described somewhere. It may seem difficult and tedious, but this is how you engineer something rather than merely 'develop' it. We programmers sometimes spend far too much time juggling stuff in our heads and communicating with coworkers in a wonderful game of workplace telephone. If the state machine has become too complex, then we have lost all hope to fully manage it and must accept the risks. Some things just shouldn't be risked!

eradicatethots 9y ago
It is tedious. It’s inefficient. Quality software usually is less important than working software.
- maldeh 9y ago
  Unless I'm misinterpreting the meaning of "usually" or "important", I find this comment a little bewildering in the context of the article.
  - katastic 9y ago
    In the working world, what matters is you ship. The most beautiful code and best "game ever designed" means nothing if it doesn't ship. Additionally, in my years of working as a contractor, I can tell you that nearly 1 in 1,000 companies (+ or - 1) care about security. Management simply does not value it, and everyone already thinks your product "should have been done yesterday." The entire world runs on insecure products. From banks, to healthcare, to universities. I can list every one of those who has put admin credentials in a publicly, internet accessible text file. (But they'll do silly things like insanely unmemorizable passwords like 23ix2n5 that get written down as postit notes and as files on desktops, and disable RDP copy-and-paste but leave RDP hard drive support.) We're going to continue seeing these blunders day after day until people start going to jail for losing data.
    - digi_owl 9y ago
      Or stop treating programming like some grand joust...
      - TeMPOraL 9y ago
        We won't. Worse is better, remember? Especially when a typical company wants to be the first to quickly sell some shit product and then, maybe, they'll patch it for a while as they go along. Competitive pressures (and management fads, IMO - software market ain't that efficient yet) turned "good solution today > perfect solution next week" into "steaming pile of garbage today > good solution tomorrow". I guess this is fine for throwaway acquihire SaaS stuff, but it's becoming a serious problem for stuff that's meant to be widely used.
  - emmelaich 9y ago
    Consider it descriptive rather than prescriptive.
- InclinedPlane 9y ago
  Can you think of any particular circumstances where quality would be of paramount importance? I'll wait.
  - jdhendrickson 9y ago
    Pacemaker firmware comes to mind.
    - colejohnson66 9y ago
      You’d think: https://arstechnica.com/information-technology/2017/08/465k-patients-need-a-firmware-update-to-prevent-serious-pacemaker-hacks/ https://arstechnica.com/information-technology/2017/08/465k-...
- criddell 9y ago
  I've been working in the same code base one way or another for more than 20 years now. Quality is underrated.
userbinator 9y ago
This, to me, is one of the biggest problems facing our industry. In first year undergraduate in engineering we learn how to design a state machine. We learn to design one before we learned OOP and circuits and assembly. I think one of the causes is that a lot of CS is taught top-down and not bottom-up, so things like flowcharts, state diagrams, and other similar visual aids are completely skipped in preference to more abstract thinking. I wonder if at least some of this aversion is directly related to the "gotophobia" that started with Dijkstra's famous paper. It may seem difficult and tedious, but this is how you engineer something rather than merely 'develop' it. As someone who learned the "old school" way of planning out your code --- yes, even drawing flowcharts and state diagrams --- before writing a single line of it, I can assuredly say that it should be a natural and completely pleasant process; what's "difficult and tedious" is trying to debug and coerce something you (or someone else) wrote without planning into working correctly. Over the years coworkers have been puzzled at why I spend "so much time" flowcharting and just thinking before writing even a single line of code --- only to try adopting the same method once they realise how much time it saves in total, since all the cases have already been accounted for and the only thing left to do is test out any of the few remaining and often trivial bugs introduced during the design->code process.
- digi_owl 9y ago
  It also takes all the "fun" out of programming, as so many seems to approach it like some grand display of mental prowess. Never mind the whole "agile" thing...
  - reitanqild 9y ago
    You can look at this both ways actually: For some people (like me) thinking through problems with pen and paper is a tool. For others I guess it is annoying: look at him, now he's doing this wannabe software architect stuff again. Same might go the other way: here he goes again, trying to prove his programming super skills by jumping into it without even the smalles amount of planning.
    - Swizec 9y ago
foobarian 9y ago
I find it interesting how in a large codebase or project there is a temptation to mutate an object here, decorate some intermediate object there, and before you know it you have an ugly state machine hiding in your code. As you know the number of possible states grows very fast and when people don't know this is happening things soon get out of control. Having things immutable by default helps somewhat, but it's still easy to add various decorators.
technion 9y ago
I guess a related question would be, is anyone aware of a common protocol that does have a formally defined state machine to review?
- scott_karana 9y ago
  TCP's might not be formally defined (unsure), but it's pretty well understood to the point of having de facto ones, at least.
  - userbinator 9y ago
    There are state diagrams in the TCP RFC --- in ASCII art, so the authors clearly really wanted to have one.
    - scott_karana 9y ago
      Nice! Good to know. That must be the origin of all the useful but unofficial SVG ones I'd seen :)
- lsh123 9y ago
  SSL
  - tom_mellior 9y ago
    Here is really cool work on state machines in TLS: https://www.smacktls.com/smack.pdf https://www.smacktls.com/smack.pdf Beurdouche et al., "A Messy State of the Union: Taming the Composite State Machines of TLS" From the abstract: "mplementations of the Transport Layer Security (TLS) protocol must handle a variety of protocol versions and extensions, authentication modes and key exchange methods, where each combination may prescribe a different message sequence between the client and the server. We address the problem of designing a robust composite state machine that can correctly multiplex between these different protocol modes. We systematically test popular open-source TLS implementations for state machine bugs and discover several critical security vulnerabilities that have lain hidden in these libraries for years ..." Based on this work you might say that there are formal state machines for TLS, but they aren't in the standard.
bdcravens 9y ago
> It may seem difficult and tedious, but this is how you engineer something rather than merely 'develop' it. Don't agile approaches encourage this, focusing on features and things that can cleanly be assigned story points at the expense of a bigger picture, with velocity being the focus?
- maskedSlacker 9y ago
  It seems to me that agile approaches are a response to the phenomena of the spec often being wrong. If the spec is wrong and going to need substantial revision, iteration is better than planning. If the spec is not wrong, careful planning is probably better than high velocity iteration. I think cryptography is a good example of this--would you develop a cryptographic API on which people's lives might depend iteratively through a release early and fail often method? I hope not.
  - taneq 9y ago
    Exactly, and this is why Agile (while grand for things like "The customer wants a web site. They don't know what they want or how they want it to look, but we need to start on Tuesday.") isn't the be-all and end-all that it's advertised to be by people who only work on websites for tech-illiterate customers. In a lot of software development, especially large scale enterprise software (where you're trying to map a complex set of existing business practices and workflows into software) and embedded software (where you have to write something that provides fixed, well-understood functionality running on hardware with a months- or years-long iteration time) you do have a complete and correct spec (or at least the means to generate one). In these cases a less ad-hoc approach than Agile can be beneficial.
  - arohner 9y ago
    I upvoted this, but agile and "release early and fail often" aren't necessarily the same thing. For example, they could have iterated quickly during the draft phase, come up with a proposed implementation, have the security researchers review it, and iterate.
NamTaf 9y ago
Compare front-end [1] design philosophies (such as used in waterfall development) vs iterative design philosophies (such as in agile development). As a non-software, 'real world' engineer (mechanical, heavy industry design) looking in from the periphy of computing as a hobby/amateur interest, it appears to me like software engineering as a discipline has sort of forgotten about why and when FEED is appropriate and, critically, how to implement it when it is. Let's reflect: iterative design is popular in software engineering because software usually suits it. Changes are easily iterable, you can often roll changes back, there's relatively low cost to cloning changes across millions of instances, code's design lifetime is relatively short, etc. In contrast, 'real world' engineering (civil, heavy mechanical) favours FEED because the cost of change rapidly and prohibitively rises with time, so nailing down the scope and structure early is critical, there's long procurement times for changes, the design lifetime of the finished product is measured in decades, etc. The rub is that there's a small niche of software design, such as protocol design like this, or certain firmware scenarios, which far more closely resembles the latter even though it's usually done by a community used to and trained in the former. Although it's for different reasons, all the things that make FEED appropriate for 'real world' engineering also apply to these sorts of software tasks, but software engineering as a whole doesn't appear to[2] focus on teaching and supporting the necessary tools and techniques for performing that process well. Flip that on its head, and it's why software companies quickly begin to run rings around companies traditionally focused on hardware once software starts to play a bigger part and the limitations stopping iterative design from working begin to disappear. Software engineering largely biases towards iteration (understandably) and when it works it allows for good advantages. But in embracing those advantages, software engineering as a discipline has begun to lose an understanding of FEED and the careful methodology it delivers. [1]: https://en.wikipedia.org/wiki/Front-end_engineering https://en.wikipedia.org/wiki/Front-end_engineering & https://en.wikipedia.org/wiki/Front-end_loading https://en.wikipedia.org/wiki/Front-end_loading [2] I admit I've not done a CS/SE degree, but I've gone through a couple of subjects run online and I talk to friends who did do it and that's the feel I get. Besides, just look at HN's generally trending articles. edit: With all I wrote, I don't mean to undermine the extremely good work that the devs designing these protocols, etc. almost always perform. It's far beyond my ability. I am speaking more in a general sense about how Soft. Eng. seems to have thrown out the baby with the bathwater in declaring agile philosophies as 'the best way'. My feel is that the pendulum seems to have swung too far past 'best' towards becoming 'only'.
pfortuny 9y ago
Either engineering and its tools (eg state machines) or just craftmanship. Totally right.
pron 9y ago
> there is no formal description of the 802.11i handshake state machine. Here is what the paper actually says: The 802.11i amendment does not contain a formal state machine describing how the supplicant must implement the 4-way handshake. ... Fortunately, 802.11r ... does provide a detailed state machine of the supplicant. The problem, as I understand it, was that when the protocol was formally verified, the properties checked were only the escape of the private key and identity related issues. The property of the nonce never being reset was simply not considered. The missing piece, then, wasn't a precise description of how the system works, but rather a precise list of what it's supposed to guarantee. Without a clear and concise description of the requirements, it's hard to verify that the system satisfies them. Alternatively, it's possible that the list of guarantees was complete, in which case reviewers should have noticed that no nonce reset isn't one of them, yet it's required for the security of certain communication protocols used over the channel.

oconnore 9y ago

> In the end we all know that the answer is for humans to stop doing this work. We need machine-assisted verification of protocols, preferably tied to the actual source code that implements them. This would ensure that the protocol actually does what it says, and that implementers don’t further screw it up, thus invalidating the security proof. And yet, there are still regular posts here about whether static type systems have any merit at all... never mind advanced things like linear/dependent types, theorem provers, TLA+, etc. Just use Go!

munin 9y ago
We did formally verify the 802.11i protocol, though: https://link.springer.com/article/10.1007%2Fs12204-009-0122-3?LI=true https://link.springer.com/article/10.1007%2Fs12204-009-0122-...
- scott_karana 9y ago
  And the implementations ignored all the fundamental "nonces should never be used" part of the formal handshake protocol, and thus would have failed the aforementioned testing.
- tom_mellior 9y ago
  Question about this, because the featured article strangely doesn't actually say what the problem is: Did this verification result simply forget/not consider nonce reuse? The article seems to imply there's nothing wrong with the proof or the statement of the properties to be proved, it's about integration with another component. But if "don't reuse nonces" is a standard security property to verify, then I would think that that is a hole in the verification. Could someone shed more light on this?
  - kruczek 9y ago
    It is covered in Q&A at https://www.krackattacks.com/#faq https://www.krackattacks.com/#faq - basically the proof didn't cover this particular scenario: > The 4-way handshake was mathematically proven as secure. How is your attack possible? > The brief answer is that the formal proof does not assure a key is installed once. Instead, it only assures the negotiated key remains secret, and that handshake messages cannot be forged.

userbinator 9y ago

More importantly, even after the fact, they’re hard for ordinary security researchers to access. Go ahead and google for the IETF TLS or IPSec specifications — you’ll find detailed protocol documentation at the top of your Google results. Now go try to Google for the 802.11i standards. I wish you luck. The first result for "802.11i" is the Wiki page for IEEE 802.11i-2004, which mentions that it's incorporated into 802.11-2007, and if you search for "802.11-2007", the first result at the top (after the amusing calculation that 802.11 - 2007 = -1 204.89) is the PDF of the full standard. ...and I'm not even a security researcher. But I agree with the rest of the criticism of the IEEE and the 802.11 standard in particular, once you've acquired it. One of my pasttimes is seeking out and reading standards for protocols, file formats, and other things; and so I've seen quite a few. As an overall impression: IETF's are very readable, most of the ITU ones are pretty good if somewhat terse, ANSIs and IEEEs vary widely between "a little bit of effort" and "I feel like my brain is melting if I read more than a paragraph an hour", and 3GPPs along with BlueTooth are very much in the "take a 10 minute break to digest after every sentence or two" category. 802.11 is also like that. The acronym density in that document is one of the highest I've ever seen. Maybe KRACK will at least make them consider editing their standards and formatting them to be somewhat less of a chore to understand; things like https://files.catbox.moe/xym9dq.PNG https://files.catbox.moe/xym9dq.PNG should really be put into tables.

thezilch 9y ago
And then he wrote... The IEEE has been making a few small steps to ease this problem, but they’re hyper-timid incrementalist bullshit. There’s an IEEE program called GET that allows researchers to access certain standards (including 802.11) for free, but only after they’ve been public for six months — coincidentally, about the same time it takes for vendors to bake them irrevocably into their hardware and software. In other words, it's getting better, but vendors are burning silicon by the time researchers have the time to even crack open whitepapers -- too late.
- colejohnson66 9y ago
  Why is there a delay at all? If they’re a security researcher, it would make sense to allow them access as soon as possible.

cyberferret 9y ago

Just to clarify a question I had when reading about KRACK - If you are using a VPN over WiFi, you still have some degree of safety, right? Any way that the KRACK vulnerability can be elevated to sniff and decrypt VPN packets in transit?

wskinner 9y ago
Yes. It appears that since KRACK can allow the attacker to hijack a TCP handshake that they could potentially downgrade an HTTPS connection where HSTS is not used, but that shouldn’t affect your VPN connection.
- iancarroll 9y ago
  To be clear, if a client makes an HTTPS request, you cannot downgrade it to HTTP, even if you're in control of the TCP socket. You can only hijack connections that are initially made over HTTP.
  - wskinner 9y ago
    In fact, you can, using sslstrip. It was demonstrated in the video, as well as in this article: https://arstechnica.com/information-technology/2017/10/severe-flaw-in-wpa2-protocol-leaves-wi-fi-traffic-open-to-eavesdropping/ https://arstechnica.com/information-technology/2017/10/sever.... I think this will only work against android/linux clients, since in that case the attacker actually knows the key, and can perform a proper MITM.
    - iancarroll 9y ago
      You cannot. sslstrip exists to attempt to work around the fact you can't directly downgrade HTTPS to HTTP. In that video, because HSTS isn't used on match.com (unfortunate), the browser doesn't attempt to make an HTTPS connection at first. Obviously, if you have control of that TCP connection, you can do whatever you want. The browser is oblivious to HTTPS existing. Also, be careful not to confuse the layers here. The encryption algorithms in WPA2 are completely unrelated to TLS/HTTPS. TLS is... somewhere in the OSI model, but it's well above WPA2/packet handling, and TLS can/does work with a compromised network.

a3_nm 9y ago

One thing I don't understand about this attack is whether it allows the attacker to connect to the Wifi network (in the style of airmon-ng for WEP), or whether the attacker can only decrypt packets of legitimate users. Has anyone figured this out?

M4v3R 9y ago
This attack doesn't expose Wi-Fi network key, so I assume it doesn't let you join the network, just sniff the traffic of the targeted user (and also, in some cases, forge/inject packets).
grive 9y ago
This attack is a MitM. The attacker is able to act as the access point and receive the victim's traffic, unencrypted. He is also able to modify this traffic and serve compromised pages. The attacker needs to have a stronger signal than the legitimate access point. So he has to stand pretty close to the victim, physically.
- blauditore 9y ago
  But still, this is only problematic if you "trust" an access point. If you treat any wifi network like a public hotspot (i.e. potentially rogue), there's not much of a difference, right? In practice, as long as you only trust data received through TLS, you should be fine.
  - rocqua 9y ago
    Do you not 'trust' your home wifi router?
    - Retr0spectrum 9y ago
      Personally I don't, because my ISP owns it.
    - blauditore 9y ago
      Well, I don't trust whole the network (internet) in general, as I don't know where and how things are routed, and by whom. The only situation where trust in the router would be relevant to me is for communication within a local network, so I'm controlling every device involved. And there, this attack might actually be harmful, as far as I understand.

dmitriid 9y ago

Re-read this article every time when you come across yet another blog post or article extolling the virtues of formall proofs, verifications, and, while we’re at it, static typing. None of these work when taken in isolation and given to actual people to work with.

TeMPOraL 9y ago
On mobile and imgur refuses to work on my Fx, so won't post a screenshot. So just imagine how funny yours and oconnore's [0] comments look next to each other... So, which way is it? [0] - https://news.ycombinator.com/item?id=15488391 https://news.ycombinator.com/item?id=15488391
- ktta 9y ago
  If you look around, the problem touted here was that formal verification was done, but independently for two different parts of the standard, in isolation. The layman answer that is formal verification should've been done on those systems after integration. I'm not sure how much that would've helped though, since the proofs for each of those was complex enough. And then actual code written tends to sway far away from what protocol implementers (also crypto folks) think it should look like. So I'd say more formal verification, but also make it easier and accessible for normal developers without a Math PhD. And verification of actual code would be ideal. Something I've come across recently is formal verification of cryptographic implementations not on paper (i.e. mathematically) but in plain C using tools and languages developed recently. For example, a three part series on how SAW and Crytol were used to formally verify s2n (AWS's TLS lib): https://galois.com/blog/2016/09/verifying-s2n-hmac-with-saw/ https://galois.com/blog/2016/09/verifying-s2n-hmac-with-saw/ https://galois.com/blog/2016/09/specifying-hmac-in-cryptol/ https://galois.com/blog/2016/09/specifying-hmac-in-cryptol/ https://galois.com/blog/2016/09/proving-program-equivalence-with-saw/ https://galois.com/blog/2016/09/proving-program-equivalence-... PS(A) for the adventurous: I've also come across a github repo that lists related stuff https://github.com/enzet/symbolic-execution https://github.com/enzet/symbolic-execution
- dmitriid 9y ago
  The protocol was formally verified. And yet...

vikiomega9 9y ago

I don't understand how the attacker can block step 3 of the handshake from the client. Can someone ELI5? What I was able to understand so far is that the use of a particular nonce is being forced on the client and given that invariant keystream one can decrypt known messages. I'm still fuzzy on how the attacker can force this step. EDIT: Further question, isn't timestamp synchronization taken into account here when invalidating a nonce? What happens when I disconnect from wifi to a mobile network and back to the wifi?

rocqua 9y ago
The attacker gets a Man in the Middle position on layer 2 (data link). So every step in the handshake goes through the attacker. The attacker couldn't just MitM the protocol on layer 3 as it cannot authenticate with the WiFi router. Of course, the attacker already could just pretend to be the wifi router and then forward and inspect all traffic to the internet. What is scary here is that it breaks into a Local network as opposed to the internet.
cesarb 9y ago
From what I understood, there are two ways to block step 3. The most obvious way is to jam it, that is, send noise at the same time so the radio fails to receive it. The other way (and the one which makes attacks easier) is to pretend to be the AP but in another channel. Suppose the real AP is on channel 1. The attacker is nearer the victim than the AP, and is on channel 6. The attacker repeats on channel 6 everything the AP sends on channel 1, and repeats on channel 1 everything the victim sends on channel 6. The victim sees the same AP on both channels, channel 1 and channel 6 (the attacker modifies the part of the AP beacon/responses which says "I'm on channel X"), which is a perfectly legitimate and normal thing, and chooses channel 6 because it has a stronger signal. Since now the attacker is in the middle, it can modify anything. Change the AP beacon to say "I'm on channel 6", drop any packet it wants, duplicate any packet it wants, and so on. > What happens when I disconnect from wifi to a mobile network and back to the wifi? The wifi negotiation starts from scratch, with a new step 1.
- vikiomega9 9y ago

Perceptes 9y ago

Question for the HN mods: I submitted this same article earlier: https://news.ycombinator.com/item?id=15483452 https://news.ycombinator.com/item?id=15483452 Why was this one able to be submitted instead of just redirecting to my submission?

Jedi72 9y ago
The quality of this title is terrible as well, the title should say 'Vulnerability in WiFi handshake discovered, its name is KRACK'
tonyztan 9y ago
I have the same question. I tried to submit this same article last evening and got redirected to Perceptes' submission. I'm curious as to what happened?

deleted 9y ago

[deleted]

deleted 9y ago

[deleted]

askvictor 9y ago

Can someone clarify if wpa2-enterprise with radius auth is affected? I have seen assertions both ways.

GenericsMotors 9y ago
It is affected. Note that this isn't an exploit that allows the attacker to discover the encryption key or connect to the AP by getting around an authentication scheme (such as radius). The attacker impersonates an existing AP and forces the client to reuse IVs / reset the encryption key to zero (in the case of wpa_supplicant), and is able to decrypt traffic that way.
- PakG1 9y ago
  Yes, but stupid question. If Radius is being used, there's no way to successfully impersonate the AP and have the victim accidentally try to join it because the AP won't be able to authenticate the WPA2-Enterprise credentials? Then the attack fails? Or silly me, the fake AP could be configured to somehow accept the login attempt by the victim? But if so, then it'd be able to record the login credentials thus making the attack's impact even larger than I've seen discussed, because then not only is the attack successful in decrypting the victim's traffic, but the victim's Wi-Fi credentials are also stolen?
  - GenericsMotors 9y ago
    > If Radius is being used, there's no way to successfully impersonate the AP and have the victim accidentally try to join it because the AP won't be able to authenticate the WPA2-Enterprise credentials? From what I understand the credentials won't matter. Anyone else more knowledgeable please correct me if I'm wrong, but the attack goes something like this: 1. Capture trafic that includes the 4-way handshake 2. replay message #3 of the handshake 3. client's encryption key is set to zero (in the case of wpa_supplicant), and nonce/IV are reused going forward 4. you are now in control of the encryption key being used (again, only wpa_supplicant) so you can go ahead and MITM the victim's DNS queries, capture cookies, etc... The Details section of the researcher's site explains it pretty well: https://www.krackattacks.com/#details https://www.krackattacks.com/#details Lastly, the most urgent task for mitigating this is to patch client devices as quickly as possible. Android's fractured vendor-specific distributions and lack of long-term support for the low-mid level models is going to make this a difficult/impossible task...

qznc 9y ago

This seems so overhyped? Why do you care about encrypting the step from device to access point? If you have sensitive data, then you must encrypt end-to-end anyways, because there are a lot more steps between access point and destination. Thus, HTTPS or Signal or PGP or whatever is enough and WPA does not matter.

mhandley 9y ago
That might be true if we had secure DNS deployed. But we don't, so using this attack, DNS cache poisoning is pretty easy. And if you can subvert DNS, you can redirect HTTPS traffic to a typosquatted version of a website. Unless you check the URL bar every time you visit an HTTPS website that is in your bookmarks, you'll probably not notice, and there goes your password in the clear across a nice secure end-to-end encypted HTTPS connection to the bad guy.
- NoGravitas 9y ago
  Modern browsers are very vociferous about not connecting to https sites with certificate errors. So while DNS cache poisoning with this attack is Very Bad, unless the attacker can insert a bad CA certificate in your browser, or has a valid but improperly-obtained certificate for the website in question, you're not going to fail to notice that something janky is going on.
- PinguTS 9y ago
  And that is actually what the author of KRACK has presented. He re-directed as MTIM via DNS to a different site.
PinguTS 9y ago
There are many services in your local network, which are un-encrypted. Any basic protocol that is in the lower layers required to run the infrastructure like ARP, DHCP, DNS, and alike. Then there are also higher layer protocols, which are un-encrypted like SMB, AFP, NFS, and alike. Many IoT devices, like your Cisco Phone talks TFTP at startup. That is the reason why we have/had WEP, WPA, WPA2 to allow a local infrastructure to have the very same trust like physical cables.

z3t4 9y ago

I love the image with the kitchen drawers ... It passed the linter, it passed the type checks, it passed the unit tests ...

cesarb 9y ago

> There’s an IEEE program called GET that allows researchers to access certain standards (including 802.11) for free, but only after they’ve been public for six months Also, that program only allows access to the latest release of each standard. Which means that, when there's a new release of a standard, access to any version of it is closed for six months.

acqq 9y ago

Funny how 2013 discoveries are tried to be forgotten and not mentioned: https://www.theguardian.com/world/2013/sep/05/nsa-gchq-encryption-codes-security https://www.theguardian.com/world/2013/sep/05/nsa-gchq-encry... "$250m-a-year US program works covertly with tech companies to insert weaknesses into products" "The documents show that the agency has already achieved another of the goals laid out in the budget request: to influence the international standards upon which encryption systems rely." [emphasis mine] Now compare with the details from KRACK regarding Android and Linux: https://www.krackattacks.com/#details-android https://www.krackattacks.com/#details-android "Our attack is especially catastrophic against version 2.4 and above of wpa_supplicant, a Wi-Fi client commonly used on Linux. Here, the client will install an all-zero encryption key instead of reinstalling the real key. This vulnerability appears to be caused by a remark in the Wi-Fi standard that suggests to clear the encryption key from memory once it has been installed for the first time." [emphasis mine] Sometimes adding an innocent-appearing remark, and later acting on it would be all that's needed for a rich and mighty adversary. I don't claim it happened this time, but I worry when the possibility isn't being considered and properly investigated.

agentultra 9y ago

From TFA "And separately, to answer a question: how did this attack slip through, despite the fact that the 802.11i handshake was formally proven secure?" Implies that the formal verification failed. Yet from the paper on the attack: "Interestingly, our attacks do not violate the security properties proven in formal analysis of the 4-way and group key handshake." This is a good thing! One of the hard things for software developers to do is separate the theorem (spec) from the proof (implementation). I can see how the article author would posit such a question. The paper answers the question. What do we do about it? More theorems, modelling, and proofs. Research on synthesizing the implementation from its specification. Treat events like this as we treat auto-collisions and correct the processes, tools, and technology that enable attacks like this to occur in our systems... at least that's my 0.02. :)

danib31 9y ago

Definitely another big issue, inherent to cryptography (and maybe matematics in general), is the subtelty of creating the appropriate definitions. As the post says, they thought about the individual components, but failed (or maybe it is just too difficult) to define the security considering composability of schemes. This is a clear limitation of modern cryptography. Great post!

cryptonector 9y ago

This whole process is dumb and — in this specific case — probably just cost industry tens of millions of dollars. It should stop. Bingo. A pay-for-play standards development organization should charge to _participate_ in the standards-setting activity, and NOT charge the public for access to the standards. The ITU-T seems to have learned this, at least as to some things (e.g., the ASN.1 family of standards, such as x.680 and x.690). The IEEE should do the same. Better yet, they should look at the IETF model, which has been working for _decades_. In the IETF model there is no charge at all, except for attending physical meetings. Mailing list participation is free. RFC publication is free. The IETF is financed via meeting fees and donations. Vendors have an interest in the IETF staying afloat, so they see to it -- their interest is, of course, the IETF's overall low cost to them (by comparison to OASIS, IEEE, ANSI/ISO, or the ITU-T), and the amount of review their specifications get. Maybe 802.x dev should move to the IETF lock stock and barrel, you might say, but there is a problem: the IETF doesn't have a lot of expertise with physical layer protocol specifications. _Most_ IETF participants are at layer 2 and up. Of course, this can be fixed by... just moving all the 802.x work (and the people working on it) to the IETF. EDIT: Mind you, getting the work done at the IETF would not be a guarantee of no such bugs. It would address the procedural and public access problems TFA talks about. But that alone is a huge improvement over using the IEEE for highly consequential specifications that greatly affect the public.

pc2g4d 9y ago
I recently found the need to understand the 802.11 standards in detail and was shocked to discover how difficult it is to access IEEE standards. I even work for $BIGCORP, with institutional access to various IEEE publications, but 802.11 isn't part of our subscription. I'd venture a guess that much of 802.11's security is by way of obscurity.

cryptonector 9y ago

This will provide further impetus for not using CCM/GCM and similar AEAD cipher modes in any context other than octet stream protocols (e.g., TLS, but _not_ DTLS). There is ongoing work to produce AEAD cipher modes that do not fall apart when {key, nonce} pairs are reused (for different message plaintexts, naturally). Crypto is tricky... It's easy enough to construct AEAD cipher modes by generic composition that don't have this problem. For example, the Kerberos enctypes don't. The key is to construct AEAD cipher modes that are efficient (Kerberos' add a block's worth (16 bytes) of "confounder" to each message, bloating it, and also adds a block's worth of cipher operation, slowing it down) and don't require additional random numbers if at all possible (those confounders in Kerberos are random numbers prepended to the plaintext). Also, Kerberos' enctypes use HMAC for the integrity protection part, which is not a very fast MAC.