Enabling Dynamic Symbolic Execution for TLS Implementation Analysis

Sammanfattning

Ensuring TLS implementations behave as outlined in their specification is essential for secure communication over networks. Security flaws in protocol implementations can have severe consequences, as demonstrated by incidents like the Heartbleed vulnerability and the POODLE attack, leading to data breaches, man-in-the-middle attacks, and unauthorised access to sensitive information. This thesis investigates the use of dynamic symbolic execution to analyse WolfSSL, an open-source implementation of the TLS 1.3 protocol, with a specific focus on its ServerHello message parser. To uncover potential implementation errors, we derive conditions from the TLS 1.3 specification and use them to constrain symbolic execution to program paths where nonconformances may occur. We also investigate how the placement of such constraints, either directly when the message is received, before validation logic, or after message acceptance, affects time overhead, input space coverage, and generalisability. Additionally, we propose an alternative approach to accelerate the testing of multiple requirements by inserting them as logical queries into KQuery files, the intermediate representation of symbolic constraints generated by KLEE, after symbolic execution has completed. This approach eliminates the need to re-run KLEE for each requirement. Our methods are evaluated against a previous test-case–based approach by Wilson and Asplund, showing that our approaches manage to find the same number of nonconformances. The results indicate that the placement of assume statements affects execution time and state space exploration when running KLEE on WolfSSL, and these factors along with generalisability affect how the assume statements should be placed to obtain more desirable results in different scenarios. Our results also indicate that modifying KQuery files can significantly reduce time overhead while still allowing complete exploration of all input cases where a requirement might be violated.