| Building secure and reliable Internet of Things(Io T)systems becomes more challenging as the scale and complexity of Io T increases.Communication security plays a crucial role in addressing this challenge.In addition,although the high mobility of Io T devices improves people’s life convenience and work efficiency,it may also increase the instability of the communication environment,even leading to security accidents and other issues.Additionally,the real-time sensing and processing capability of data provided by Io T systems will directly affect user experiences.It is evident that security,mobility,and real-time are the three vital features for constructing secure and reliable Io T systems.Formal methods,a technology based on rigorous mathematical theory,are widely used to describe,analyze,model,and verify software and hardware systems,which can significantly improve the security and reliability of systems.Therefore,it is a crucial research topic to explore how to describe,analyze,and verify the features of Io T systems from the perspective of formal methods to enhance system reliability and security.This thesis uses formal methods to study Io T deeply,aiming to provide a solid theoretical framework for building secure and reliable Io T systems.The first signification issue is how to accurately depict the behavior of Io T systems,especially their key features such as security,mobility,and real-time behaviors.To solve this problem,this thesis proposes a secure mobile real-time process calculus SMrCa IT,which supports the modeling and verification of Io T systems before actual implementation.After giving this calculus,how to strictly define the meaning of the SMrCaIT program is the next problem that needs to be solved.Based on the Unifying Theories of Programming(UTP)jointly proposed by Professors C.A.R.Hoare(Turing Award Winner)and Jifeng He(Academician of Chinese Academy of Sciences),this thesis gives the formal semantics of SMrCaIT calculus,including operational semantics,proof system(axiomatic semantics),denotational semantics,and algebraic semantics.Consequently,we can explain the meaning of the SMrCaIT program from various perspectives based on these semantics.Firstly,to describe the program execution process intuitively and in detail,this thesis proposes the operational semantics of the SMrCaIT calculus.Secondly,to prove the correctness of the SMrCaIT programs,this thesis builds a proof system for the SMrCaIT calculus.Thirdly,to abstractly elaborate the mathematical meaning of the SMrCaIT programs and enable us to predict its execution effect before the program is executed,this thesis gives the denotational semantics of the SMrCaIT calculus.Finally,to succinctly describe the properties of programs and the relationships between them in the form of equations,this thesis provides the algebraic semantics of the SMrCaIT calculus.Through the Internet of Vehicles case,this thesis demonstrates the usability of SMrCaIT calculus and its formal semantics.The main contributions of this thesis include:· Secure Mobile Real-time Process Calculus SMrCaIT for Io TTo strictly characterize the behavior of IoT systems,this thesis presents a secure mobile real-time process calculus SMrCaIT.At first,to enhance communications security,the SMrCaIT calculus introduces the notion of channel restriction,which limits the visible scope of communication information to specific areas,thereby preventing nodes in the environments from eavesdropping on the communication content.In addition,this thesis also adopts the notion of scope extrusion to present the dynamic changes in scopes,enhancing the flexibility of description.Secondly,the SMrCaIT calculus provides parametric mobility models,strictly separating the modeling of process actions and node mobility,which allows us to describe the node movement trajectory in an accurate and flexible way.Finally,the SMrCaIT calculus can also describe actions with timeouts to simulate the real-time dynamic evolution of Io T systems.· Formal Semantics of the SMrCaIT CalculusTo explain the meaning of the program rigorously,this thesis gives the formal semantics of the SMrCaIT calculus,including operational semantics,proof system,denotational semantics,and algebraic semantics.(1)Operational Semantics: To describe the execution details of the program,this thesis proposes the operational semantics of the SMrCaIT calculus,which includes a series of transition rules related to communications,mobility function replacement,channel restriction,and scope extrusion.This thesis applies real-time Maude in rewriting the SMrCa IT calculus and its operational semantics.By further simulating and verifying the Internet of Vehicles case,this thesis fully demonstrates the usability of the calculus and its operational semantics.(2)Proof System: To verify the correctness of the SMrCaIT programs,this thesis constructs a proof system for the SMrCaIT calculus,based on the extended Hoare Logic with time.When designing the proof rules for parallel compositions,we introduce the concept of cooperation test,and further combine it with channel restriction and scope extrusion,ensuring that information is correctly transmitted between entities while improving information security.Furthermore,we also prove the soundness of this proof system.(3)Denotational Semantics: To show the execution effect of the program mathematically,we define the denotational semantics for the SMrCaIT calculus based on the trace model.The trace model contains two types of traces: communication traces for message exchanges,and scope traces for implementing channel restriction and scope extrusion to ensure data security.(4)Algebraic Semantics: To describe the properties of SMrCaIT programs and the relationships between them,we give the algebraic semantics of the SMrCaIT calculus,including the laws related to channel restriction,scope extrusion,etc.The introduction of the notion of guarded choice can not only express programs in a unified form,but also transform complex concurrent programs into a more intuitive and simple linear sequential structure. |
PDF Full Text Request