Verifying Multi-vendor IoT Deployments Using Conditional Tables

In recent years, IoT devices have seen widespread deployments in critical environments such as healthcare, military, and home security systems. These deployments often involve managing a heterogeneous collection of devices by non-expert users, increasing the risk of errors that could lead to significant monetary and physical damage. Unfortunately, such deployments face unique challenges such as incomplete visibility (e.g., need to interoperate with closed software systems), incompatibility (e.g., need to interact across different protocols and control logic created by different vendors), and management complexity (e.g., need to express complex and diverse intentions in ways that can be understood by inexperienced users). While system verification has been crucial in catching errors early in other domains, these challenges complicate its application in IoT. To perform verification under these conditions, we propose Pyotr, a system based on a mathematical framework from the theory of database systems called incomplete databases. Pyotr can integrate data from heterogeneous devices, perform data analysis under failures and uncertain knowledge, verify intended behavior using easy-to-use database-styled queries, and provide a generalized algebraic framework for reasoning about IoT systems in a rigorous and intuitive way. Our experiments on large IoT networks show that Pyotr can scalably answer complex queries on thousands of connected IoT devices within a few milliseconds.