Using Requirement-Driven Symbolic Execution to Test Implementations of the CoAP and EDHOC Network Protocols

Abstract: As the number of Internet of Things devices is increasing rapidly, it is of utmost significance that the implementations of protocols for constrained devices are bug-free. In general implementations of network protocols are error-prone due to their complex nature and ambiguities in the protocol specification. Implementations of network protocols often contain critical errors which could be exploited. To avoid bugs and vulnerabilities, the implementation of network protocols has to adhere to their specifications. The objective of this thesis is to use symbolic execution to test one implementation of the Ephemeral Diffie-Hellman Over COSE (EDHOC) protocol and one implementation of the Constrained Application Protocol (CoAP) against their specifications. The goal is to identify bugs such as crashes, non-conformances, memory errors, and security vulnerabilities that may occur if the implementations are not adhering to their specifications. The methodology to do this consists of three steps: 1) extracting requirements from the protocols Request For Comments and expressing them as formulas, 2) preparing the system under test for symbolic execution and applying the formulas during symbolic execution to detect any paths that violate a requirement, 3) for every path which violates a requirement, the concrete value that the symbolic execution engine provided is used in the unmodified implementation to validate the bug. In total seven non-conformances were found which have been reported to developers. One non-conformance was found in the EDHOC implementation and six were found in the CoAP implementation.