Symbolic Execution of Security Protocol Implementations: Handling Cryptographic Primitives

We show how to efficiently simulate cryptographic primitives during symbolic execution. This allows analysis of security protocol implementations, and revealed several flaws in implementations of WPA2's 4-way handshake.

Traditional symbolic execution engines cannot handle cryptographic primitives, because analyzing them results in complex symbolic expressions that cannot be handled by the SMT solver. We prevent this by simulating their behaviour under the Dolev-Yao model. This enables efficient symbolic execution of security protocols implementations, making it possible to detect common programming mistakes in them. We also show how to detect misuse of cryptographic primitives. That is, we can detect trivial timing side-channels, and we can identify decryption oracles where unauthenticated decrypted data influences the program's behaviour. We apply our technique on three client-side implementations of WPA2's 4-way handshake. This uncovered timing side-channels when verifying authentication tags, a denial-of-service attack, a stack-based buffer overflow, and also revealed a non-trivial decryption oracle. We confirmed all vulnerabilities in practice, and discuss them in detail.