Ensuring the Functional Correctness of IoT through Formal Modeling and Verification

Recent research initiatives dedicated to formal modeling, functional correctness and security analysis of
IoT systems, are generally limited to, model abstract behavioral patterns and look forward possible attacks
beneath gauging and providing feasible attacks. This research considers the complementary problem by
looking for more accurate attacks in IoT by capturing richer behaviors -technical, physical, and socialincluding
their quantitative features. We propose IoT-SEC framework that establishes an adequate
semantics to the IoT’s components and their interactions including social actors that behave differently
than automated processes. For security analysis, we develop a general approach based on a library of attack
trees from where we generate automatically the monitor, the security policies and requirements to harden
the IoT model and to check how well the model is secure. We use PRISM model checker to analyze the
functionality and to check security of the IoT model. Precisely this contribution ensures the functionality of
IoT systems by analyzing their functional correctness.