Testing and Verifying Network Protocol Implementations

As more and more systems are being connected to the Internet, adequately securing them has become a vital but error-prone task. One well-known example of something that can go wrong is the Heartbleed vulnerability in OpenSSL. This vulnerability had a major impact on the Internet, because OpenSSL was (and still is) widely used to securely transmit information. Unfortunately, there are many more examples of vulnerabilities in network protocol implementations, and these form the root cause of various security incidents. The goal of the proposed project is to detect and prevent security bugs in implementations of network protocols such as OpenSSL. We will accomplish this by automatically analysing the source code of an implementation. Our proposed techniques can detect various kinds of security issues, and are in particular designed to detect logical vulnerabilities. These are flaws where the system does not crash, but instead incorrectly processes or reacts to certain inputs. One method we propose to detect such flaws is to compare the behaviour of two protocol implementations. Note that current state-of-the-art solutions cannot automatically (and efficiently) detect logical implementation flaws. With the increasing reliance on network-connected devices, ranging from traditional web servers to Internet-of-Things devices such as home routers, the impact of this project on the security of the Internet could be very high.