Symbolic Execution of Security Protocol Implementations: Handling Cryptographic Primitives
https://papers.mathyvanhoef.com/woot2018.pdf [papers.mathyvanhoef.com]
2018-08-20 01:03
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.
Slides: https://papers.mathyvanhoef.com/woot2018-slides.pdf
source: grugq