In today’s tech-driven society, we increasingly rely on the security of internet commu-

nication to handle personal data, financial transactions and digital infrastructure. TLS

1.3 is one of the most used cryptographic communications protocols for securing internet

communication, ensuring confidentiality, authenticity, and integrity. However, imple-

mentations remain vulnerable to critical software defects: Heartbleed and Apple’s ”goto

fail;” are two of the major discovered security bugs which risked data leakage and enabled

authentication-bypasses, respectively. For this reason systematic methods are needed to

find bugs before they are exploited. This thesis presents a KLEE-based Differential Sym-

bolic Execution framework to test the parsing of the ServerHello message in OpenSSL

and wolfSSL implementations. The framework progressively introduces message fields as

symbolic variables in order to detect end-to-end divergences between implementations. It

is developed and guided by a proof of concept (PoC) implementation, in which it discovers

9 out of 12 injected bugs. Applied onto the real TLS implementations, two unique diver-

gences are found through four runs of Differential symbolic execution for which OpenSSL

is classified as non-conformant to the RFC 8446 (TLS 1.3). Furthermore, through the

runs discrepancies in build configurations was uncovered, assisting in ensuring a correct

setup. The results demonstrate that Differential Symbolic Execution is a viable method

for finding parsing level divergences, but is prone to state-space explosion and hence faces

difficulties in making larger fields of the message symbolic, and finding deeper vulnera-

bilities. It is also solely capable of finding divergences between implementations, possibly

vulnerabilities, and is no guarantee of proving absence of bugs.