Formal Modeling And Verification Of Ad Hoc Routing Protocols And Task-level Timing Constraints With Event-B

Mobile ad hoc network is a temporary communication network built on mobile nodes.There does not exist fixed infrastructure and centralized management equipment.Since nodes can move around freely,the network topology may change at any time.Therefore ad hoc routing protocols have to find a valid route from the source to the destination under the dynamic environment.In such network,searching routes is more challenge than the one in the wired network.Currently,researchers have proposed some ad hoc routing protocols under the cred-ible network environment.They can be classified into three categories:proactive routing protocols,reactive routing protocols and hybrnd routing protocols.Nodes in mobile ad hoc networks communicate each other by wireless method without any fixed infrastruc-ture and centralized security control.Compared with wired networks,mobile ad hoc networks are more vulnerable to communication and physical attacks.Security of such networks has attracted more and more attention.Based on the ad hoc routing protocols under the credible environment,researchers have proposed some secure ad hoc rout-ing protocols under the adversarial environment.It is a challenge task to determine the correctness of the proposed routing protocols or algornthms.The paper deeply studies the current formal verification of ad hoc routing protocols,then concludes the analysis process from system requirements to formal modeling and verification with Event-B.Moreover,since Event-B does not support the description of timing properties,the paper proposes task-level timing constraint patterns.The main contributions of the paper are as follows:· In the credible network environment,most researchers focus on the formal model-ing and analysis of individual proactive routing protocols or reactive routing pro-tocols.The paper adopts Event-B to model and analyze hybrid routing protocol ZRP.The paper concentrates on modeling the highlighted aspects of the proto-col:the connectivity of the network topology,the construction of routing zones according to the periodically exchanged neighbor information,the route discovery with the bordercasting service,the routing update in the reactive component.With the Rodin platform,we prove the automatically generated proof obligations along with the model construction to guarantee the correctness of the refinement and the loop-free and validity of discovered routes.Furthermore,we utilize ProB to vali-date the consistency between the model and system requirements.Thus we prove that the route discovery mechanism in ZRP protocol is correct· In the adversarial network environment,the paper presents the formal modeling and analysis of secure ad hoc on-demand routing protocol SRP.Firstly,we pro-pose the definition of correct routes as the criterion for judging whether the dis-cussed protocol is correct.Then according to the system assumptions and system requirements,we construct the Event-B model containing the environment model,the route discovery process and the attack model.The environment model takes into account the instability of the network topology.The attack model formalizes the behaviors of attackers containing node drop attack,creation of routing loops and creation of non-exist routes.Through the analysis of the unprovable property which states the existence of routes,the routing protocol does not prevent node drop attack or the creation of non-exist routes.Then the paper presents several examples to illustrate the discovered attacks· In the adversarial network environment,the paper presents the formal modeling and analysis of secure ad hoc on-demand routing protocol Ariadne.Attacks usu-ally occur in some particular network topologies.The model is constructed under the inactive network environment.Thus the model is different from the model of SRP on the construction for the existence of correct discovered route and the net-work environment.The model considers the creation of routing loops,creation of non-exist routes,node deletion attack and wormhole attack.Through the analysis of the unprovable existence property of discovered routes,the protocol can not prevent creation of non-exist routes,node deletion attack and wormhole attack.At last,the paper shows some examples to illustrate such cases.· Since Event-B does not directly support the description of timing properties,the paper proposes some task-level timing constraint patterns.The task-level timing constraints coincidence,exclusion,precedence and sub-occurrence are modeled with Event-B.Firstly,the pattern for task deadline that states timing properties within a task is introduced.Then patterns for different task-level timing constraints are built on top of this one by the refinement mechanism.They can be potentially applicable to a wide range of modeling and analysis of real-time systems.Final-ly,the paper illustrates the application of proposed patterns for precedence and coincidence with the formal specification and analysis of an example.