Model Based Security Testing And Verification For Trigger-Action-Programming Home Automation IoT Systems

With the continuous development of modern information technology,the Internet of Things(IoT)has entered various fields and has been widely applied.Taking home automation Internet of Things(HA-IoT)as an example,it has also developed rapidly and entered millions of households.The trigger-action-programming(TAP)IoT system control framework,represented by IFTTT framework,makes HA-IoT systems smarter and more personalized.Users can simply and efficiently build their own home automa-tion systems by writing IFTTT style rules.However,there exist serious security issues behind this commonly used mecha-nism.Common users usually lack the comprehensive understanding of behaviors of the rules they write.With the increasing number of rules,users' abilities to understand and grasp the systems quickly decline.How to ensure that the home automation systems designed by the users can run according to the users' expectations without acciden-tal insecure results,and how to verify the security of the home automation systems in various situations.These basic questions are difficult for common users to answer.Therefore,it is very important to help users perform security inspections on HA-IoT systems.This paper proposes an automatic modeling and security checking method for TAP-style HA-IoT systems.This method automatically builds models for HA-IoT systems with comprehensive consideration of the security related factors of the home automation systems,and then applies model checking and fuzz testing to con-duct model-driven system verification and testing.In this way,we conduct the security checking for HA-IoT systems.The main contributions of this paper are as follows:? An automatic modeling and security verification method is designed for trigger-action-programming home automation systems.This paper uses finite state ma-chine(FSM)to model the user-defined HA-IoT systems with consideration of the security related factors of HA-IoT systems,and provides the security specifications that can be generated automatically.Based on the models and specifications of the systems,the model checking based security verification can be conducted for TAP-style HA-IoT systems.? Based on the models of the TAP-style HA-IoT systems,a security fuzz testing method for system models is proposed.This paper provides a fuzz testing method for system model security inspections.This method defines the model inputs,and generates the state paths corresponding to the model inputs in the system model state space,and then verifies the state paths based on the given security specifications.In this way,we attempt to find out counterexample paths of the model and conduct testing for system models.In order to better explore state paths of the models and optimize the test method,a distance calculation method is proposed to measure the model inputs,so as to select better model inputs and mutate them.? A user-oriented platform,MenShen,is designed and implemented for security check-ing of TAP-style HA-IoT systems.MenShen provides intuitive system configura-tion and security checking functions to help users conduct security inspections on HA-IoT systems.This paper collected experimental data from two aspects.Based on the collected data,the system security verification and fuzz testing experiments were conducted.The experiment results show that the methods of this paper per-form well in both problem detection and checking efficiency.