微信服务号

微信订阅号

2025-4-21- 15
Home > Archive>Volume 31, Issue 8, 2020 >2362-2374. DOI:10.13328/j.cnki.jos.005960
PDF HTML XML Export Cite reminder
Formal Modeling and Verification of Paxos Based on Coq
Author:
Affiliation:

Fund Project:

National Natural Science Foundation of China (61672229, 61832015)

  • Article
    • | |
  • Metrics
    • |
  • Reference [23]
    • |
  • Related [20]
    • | | |
  • Comments
    Abstract:

    Paxos is a family of algorithms that solve consensus problems in unreliable distributed processor networks. Consensus is a process in which a group of participants in the system reach agreement on a result. As Paxos is widely used in large distributed systems, such as block chain system and Google file system, its security verification becomes more and more important. With Coq, a theorem proving tool, the formal description and definition of Lamport's basic Paxos algorithm are described, and it is proved that it satisfies the consensus property.

    Reference
    [1] Bertot Y, Castéran P. Interactive Theorem Proving and Program Development:Coq' Art:The Calculus of Inductive Constructions. Springer Science & Business Media, 2013.
    [2] Gonthier G. A computer-checked proof of the four colour theorem. 2005. https://www.cl.cam.ac.uk/~lp15/Pages/4colproof.pdf
    [3] Paulin-Mohring C. Circuits as streams in Coq:Verification of a sequential multiplier. In:Proc. of the Int'l Workshop on Types for Proofs and Programs. Springer-Verlag, 1995. 216-230.
    [4] Leroy X. Formal certification of a compiler back-end or:Programming a compiler with a proof assistant. ACM SIGPLAN Notices, 2006,41(1):42-54.
    [5] Affeldt R, Kobayashi N. Formalization and verification of a mail server in Coq. In:Proc. of the Int'l Symp. on Software Security. Springer-Verlag, 2002. 217-233.
    [6] Deng YX, Monin JF. Verifying self-stabilizing population protocols with Coq. In:Proc. of the 3rd IEEE Int'l Symp. on Theoretical Aspects of Software Engineering. IEEE, 2009. 201-208.
    [7] Lamport L. The part-time parliament. ACM Trans. on Computer Systems, 1998,16(2):133-169.
    [8] Burrows M. The Chubby lock service for loosely-coupled distributed systems. In:Proc. of the 7th Symp. on Operating Systems Design and Implementation. USENIX Association, 2006. 335-350.
    [9] Isard M. Autopilot:Automatic data center management. ACM SIGOPS Operating Systems Review, 2007,41(2):60-67.
    [10] Zheng JJ, Lin Q, Xu JT, Wei C, Zeng CW, Yang PA, Zhang YF. Paxos store:High-availability storage made practical in wechat. Proc. of the VLDB Endowment, 2017,10(12):1730-1741.
    [11] Lamport L. My writings. 2019. http://lamport.azurewebsites.net/pubs/pubs.html#lamport-paxos
    [12] Lamport L, et al. Paxos made simple. ACM SIGACT News, 2001,32(4):18-25.
    [13] Lamport L. Specifying Systems:The TLA+ Language and Tools for Hardware and Software Engineers. Addison-Wesley, 2002.
    [14] Microsoft Research-Inria Joint Center. TLA+Proof System (TLAPS). 2019. http://tla.msr-inria.inria.fr/tlaps
    [15] Chand S, Liu YA, Dstoller S. Formal verification of multi-Paxos for distributed consensus. In:Proc. of the Int'l Symp. on Formal Methods. Springer-Verlag, 2016. 119-136.
    [16] Kellomäki P. An annotated specification of the consensus protocol of Paxos using superposition in PVS. Technical Report, No.36, Institute of Software Systems, Tampere University of Technology, 2004.
    [17] Jaskelioff M, Merz S. Proving the correctness of disk Paxos. In:The Archive of Formal Proofs, 2005. http://afp.sf.net/entries/DiskPaxos.shtml
    [18] Padon O, Losa G, Sagiv M, Shoham S. Paxos made EPR:Decidable reasoning about distributed protocols. In:Proc. of the ACM on Programming Languages 1(OOPSLA), 2017. 108:1-108:31.
    [19] García-Pérez Á, Gotsman A, Meshman Y, Sergey I. Paxos consensus, deconstructed and abstracted. In:Proc. of the European Symp. on Programming. Cham:Springer-Verlag, 2018. 912-939.
    [20] Lamport L. Byzantizing Paxos by refinement. In:Proc. of the Int'l Symp. on Distributed Computing. Springer-Verlag, 2011. 211-224.
    [21] The Coq Development Team. The Coq Proof Assistant Reference Manual. 2019. https://coq.inria.fr/distrib/current/refman
    [22] Lamport L. Fast Paxos. Distributed Computing, 2006,19(2):79-103.
    [23] Chandra TD, Griesemer R, Redstone J. Paxos made live:An engineering perspective. In:Proc. of the 26th Annual ACM Symp. on Principles of Distributed Computing. ACM, 2007. 398-407.
    Cited by
    Comments
    Comments
    分享到微博
    Submit
Get Citation

李亚男,邓玉欣,刘静.基于Coq的Paxos形式化建模与验证.软件学报,2020,31(8):2362-2374

Copy
Share
Article Metrics
  • Abstract:
  • PDF:
  • HTML:
  • Cited by:
History
  • Received:August 31,2019
  • Revised:November 02,2019
  • Online: April 20,2020
  • Published: August 06,2020
Links:Institute of Software, CASChina Computer FederationCASNSFC
You are the first2036684Visitors
Copyright: Institute of Software, Chinese Academy of Sciences Beijing ICP No. 05046678-4
Address：4# South Fourth Street, Zhong Guan Cun, Beijing 100190,Postal Code：100190
Phone：010-62562563 Fax：010-62562533 Email：jos@iscas.ac.cn
Technical Support：Beijing Qinyun Technology Development Co., Ltd.

Beijing Public Network Security No. 11040202500063