Formal Modeling And Verification Of Paxos Based On Coq

With the rapid development and popularization of the Internet,network data traffic is becoming larger and larger.With the continuous enhancement of enterprise informatization,a large number of data need to be processed,and data have become the lifeblood of all kinds of enterprises.Traditional application services use a single server model,but because of the instability of network environment,servers are prone to data loss and node downtime,which seriously affects the availability of the system.In the case of stand-alone services gradually unable to meet the needs of enterprise data processing,people began to build distributed systems of server clusters.Replication technology improves the reliability of distributed systems,which can achieve load balancing under the condition of large network load and ease the pressure of the server.However,the introduction of replication technology also brings some problems such as replica data consistency.In order to ensure the high availability and consistency of the system,we need to use distributed consistency algorithm,Paxos algorithm is one of the most important ones.Consensus problem is a process in which a group of participants agree on a result in a distributed system.Paxos can solve the consensus problem well.More and more researchers focus on the optimization of the algorithm itself or the implementation of specific projects.Paxos has been widely used in large-scale distributed systems,such as block chain system and Google file system.Although Paxos is implemented more and more in engineering,there is little formal work on algorithm security.In order to enhance the application information of Paxos for researchers and enterprises,its security verification is more and more important.Therefore,with Coq,a theorem proving assistant tool,we describe the formal description and definition of Lamport's Basic Paxos algorithm.Paxos is a distributed consistency algorithm based on asynchronous communication network applied in non Byzantine fault tolerant model.Messages may be delayed,lost and disordered,system nodes may fail or restart;however,malicious nodes will not appear in the system.Using these properties,we set up a global message channel to solve the problem of defining the sending and receiving messages of nodes in asynchronous networks;At the same time,Paxos message types are very complex,we use Coq's type checking mechanism to complete the unification of message types;finally,because Paxos algorithm process involves the past information of system nodes,in order to avoid stack overflow of function recursion,we add the definition of these past information fields and update them in time to solve the problem of complex calculation.We select arbitrary system time point and prove that it satisfies the consensus property,thus completing the formal verification of Paxos.