Study On Internet Of Things Security Modeling And Exact Acceleration Principle

Internet of Things(IoT)has been widely used in commercial field and national security application field,such as industrial IoT,military IoT and critical infrastructure.Through real-time perception of all kinds of data in the real world and connection of physical and virtual objects,IoT can provide intelligent services,in which security issues are particularly important.To study the IoT security,we should promote the security design and verification of different services and business processes from the design stage of the system,so as to realize cross-disciplinary collaboration.As a formal method,model checking is a mathematical method based on strict reasoning and proof,which has strict syntax and semantics in the description of the system.It can be automatically verified by model checking tools in property verification.In view of the real-time,concurrency and large-scale characteristics of IoT system,formal analysis based on timed automata in model checking can effectively model,characterize and verify the logical process and implication properties of such complex real-time systems.In the existing research,there are still several difficulties to break through when model checking is combined with IoT security: 1)Current IoT frameworks or models consider less from a security perspective,and some security strategies lack strict proof and deduction.It is necessary to propose an IoT security modeling method which is easy to use modeling language and logic formula.2)For the abstract modeling and analysis of IoT system,its large-scale state and concurrent execution will lead to the state space explosion,and corresponding technical means are required to ensure the effectiveness of model verification.3)Exact acceleration can alleviate the state space explosion,but the existing methods may not be implemented in complex real-time models.Therefore,an exact acceleration method that can be applied to the complex real-time system model checking should be studied.In order to solve the above problems,this paper studies the exact acceleration of IoT security model and its application.The main research contents and innovations are as follows:1)Combining with model checking theory,the formal modeling method of IoT system security is studied.Service computing can analyze the heterogeneity of IoT security services.A modeling framework for IoT based on security requirements has been proposed,which can divide the conceptual hierarchy of IoT system into services,environment entities and security requirements to interact.On this basis,a formal modeling method of IoT security has been proposed,and modeling principles based on behavior rules was developed.IoTSML language is used to implement the method: Services and environment entities can be modeled by timed automata,and security properties can be depicted by temporal logic.Finally,model checking tools are used to realize automatic verification of security properties.2)In order to alleviate the state space explosion,the exact acceleration principle is studied,and the calculation algorithm of the window of acceleratable cycle has been proposed.The application premise of the exact acceleration principle is the size of the window of acceleratable cycle.Through the analysis of the principle,the calculation algorithm of the window was proposed,which can accurately compress the identified acceleratable cycle,reduce the state and clock irrelevant to verification,and partially alleviate the state space explosion.The algorithm selects any node with clock reset on the inner edge of the cycle as the starting location,obtains data such as location invariants,edge constraints and reset clocks according to the exact acceleration,and forms a new accelerable cycle by reducing the size of nodes.The new cycle can directly calculate the size of the window,avoid manual deduction,and optimize the time and memory of model verification.3)In the formal analysis of complex IoT system,the exact acceleration method based on overlapping cycle of complex real-time model checking is studied.The original exact acceleration technology is suitable for a single acceleratable cycle model.If it is applied to a complex real-time system,a large number of additional states or clock zones need to be added,which results in insufficient physical memory and cannot be verified.Aiming at this problem,an exact acceleration method based on overlapping cycle has been proposed.By analyzing the difference of acceleration effect between acceleratable cycles,the cycle with the highest acceleration efficiency was selected for abstraction,and a single overlapping cycle with fixed length was constructed.The constructed automaton model does not need to rely on each window of every acceleratable cycle,which can effectively reduce the space-time overhead and verify the complex real-time model which cannot be verified by the original technology.4)The IoT security modeling method and the exact acceleration principle are combined to apply in two practical cases to verify the efficiency of the proposed method.Case 1 studies the industrial control system(ICS)in the industrial IoT.By modeling the control process of ICS,we can analyze and discover the rules of malware.According to the counterexamples given by the verification,we can judge the behavior of malware and help to improve the security of the system.For all acceleratable cycles in ICS,the size of nodes is reduced by using the window algorithm of acceleratable cycle.The verification efficiency is greatly improved,and the simplified system model does not affect the verification of other properties.Case 2 studies the IoT gateway security system.We design the security technical framework of IoT gateway to control the logic flow of the system by polling.The formal analysis and verification of the IoT gateway system can embed different security protocols or algorithms to improve the security performance of the gateway.For complex real-time systems embedded with multiple services,the exact acceleration method based on overlapping cycle can accelerate the situation that cannot be handled in large-scale system.