ECE Seminar: Automated IoT Safety and Security Analysis
The introduction of Internet of Things (IoT) devices that integrate online processes and services with the physical world has had profound effects on society. Yet, while IoT systems have been widely embraced by consumers and industry alike, safety and security failures have raised questions about the risks of embracing IoT-augmented lives. These failures range from compromised baby monitors to vehicle crashes and monetary theft. As with traditional security problems, many of these failures are a consequence of software bugs, user error, poor configuration, or faulty design. In this talk, we will examine new classes of failures: Interactions within the physical domain that lead to unsafe or insecure environments. I will then demonstrate how to model the interactions between devices within physical spaces through source code analysis and formally verify via model checking not only the correct operation of one device, but the joint behavior of all of the devices in an environment. Using these techniques, we successfully identify threats to safety and security, and enforce the correct operation of IoT devices and environments in physical spaces. In so doing, we create a richer model of IoT safety and security, and provide consumers, developers, and industry with systems that mitigate threats to IoT in practice.