In this talk I will explain how I discovered various vulnerabilities in implementations of WPA2’s 4-way handshake. This was accomplished by symbolically executing implementations using KLEE. I demonstrate how one of the discovered buffer overflows leads to remote code execution on the router (as the root user), and how another vulnerability can be abused as a decryption oracle to recover the group key used in a Wi-Fi network.
Symbolic execution is an increasingly popular technique to discover vulnerabilities in programs. Commonly it is used in combination with traditional fuzzing to explore otherwise hard-to-reach code paths. In this talk I will first give an introduction to symbolic execution, and in particular will introduce the publicly available symbolic execution engine called KLEE.
After this introduction, I will show how to use KLEE to analyze implementations of the 4-way handshake. Our first obstacle is that cryptographic primitives (e.g. decrypting, authentication, and hashing functions) cannot be efficiently analyzed. Put differently, KLEE fails to analyze the code within reasonable time because of this. Fortunately, we show that we can easily solve this problem by replacing the cryptographic primitives with stub functions that do almost nothing (technically these stub functions simulate cryptographic primitives).
Concretely I will first show how I managed to get KLEE working on Intel’s iwd daemon. This was a fairly straightforward process, because it’s possible to reuse the unit tests of iwd to initialize symbolic execution. Then we tackle a harder case, and symbolically execute Linux’s and Android’s wpa_supplicant Wi-Fi client. This is a harder case study, but by assuming some knowledge of the C language, I will show it’s still doable to get symbolic execution working on this program. Finally I’ll get a high –level overview how I symbolically executed MediaTek’s kernel driver that implements the 4-way handshake on home routers. This was accomplished by simulating the driver in userspace. Although a more advanced example, experienced C programmers will be able to replicate this idea themselves after the talk.
In the last part of the talk, I will discuss some of the most interesting vulnerabilities I discovered. The first one is a stack-based buffer overflow that is present in MediaTek routers. This allows an insider (someone with access to the password of the network) to execute arbitrary code on the router. Another interesting use case is a decryption oracle that I discovered in wpa_supplicant. I will explain how this oracle can be abused to recover the group key (which is used to protect broadcast and multicast traffic) of a Wi-Fi network.
To conclude the talk, I will end with a recap of some lessons learned on how to get symbolic execution working in practice. In particular there are some unique challenges when analyzing protocol implementations. I hope this will teach the audience more about symbolic execution, and how it can be used in practice.
