Executive Summary : | Recently, unprecedented growth has been witnessed in the adoption of different types of IoT devices as part of smart living, starting from smart watches, smart lighting, voice assistants, etc. The IoT market is a rapidly expanding industry that covers a wide range of devices, spanning across different business verticals starting from retail to health, transport, manufacturing, entertainment, etc. with endless applications. The IoT technology ecosystem is comprised of constrained physical devices, communication technologies (like WiFi), protocols and the application software. The vast application environment of IoT technologies has created an immense market potential with businesses and organizations competing across sectors to design customized IoT solutions. However, this rapid development of IoT products followed by their uncontrolled deployments has created a cyber-security challenge. Typically, the companies that manufacture these devices are small, where the product development life cycle is short and they tend to prioritize profit over security. Many other factors including the lack of expertise in all areas of product development, lack of standards, etc., leave scope for security risks. Features such as secure boot, trusted execution, and memory protection are mostly not even considered for IoT devices. Thus, the majority of the security attacks on IoT devices exploit the vulnerabilities in the device, protocols, or software application to launch different attacks. The impact of such attacks increases multi-fold when a group of such vulnerable devices is compromised by an attacker to launch coordinated attack. As most of the protocols employed by these devices are customized to meet application requirements, it leads to different vulnerabilities in protocol implementations. Previous research on protocol security has reported that the majority of protocol vulnerabilities that are disclosed can be attributed to message parsing that has been implemented incorrectly. The parsing errors often arise due to the absence of sanity checks, particularly for the sizes of message fields, and parsing ambiguities that are caused by differences in understanding the specification among developers. Moreover, the state machine components exhibit protocol implementation weaknesses as well. Even though the use of automated software testing techniques like fuzzing can find vulnerabilities and bugs in software, it is not an exhaustive approach. In this work, we aim to develop a formal framework to verify IoT protocol implementations for security using the protocol specifications, which are written in domain-specific languages. The proposed framework specifically addresses message-parsing vulnerabilities, memory safety-related vulnerabilities, and fundamental state-transition errors in protocol implementations. The proposed work also lists specific custom changes to the protocol implementation to address vulnerabilities identified during the formal verification. |