{"id":379,"date":"2024-08-21T15:12:13","date_gmt":"2024-08-21T07:12:13","guid":{"rendered":"https:\/\/www.ndnlab.com\/?p=379"},"modified":"2024-08-21T15:12:14","modified_gmt":"2024-08-21T07:12:14","slug":"lido-linearizable-byzantine-distributed-objects-with-refinement-based-liveness-proofs","status":"publish","type":"post","link":"https:\/\/www.ndnlab.com\/?p=379","title":{"rendered":"LiDO: Linearizable Byzantine Distributed Objects with Refinement-Based Liveness Proofs"},"content":{"rendered":"\n<p>LiDO\uff1a\u5177\u6709\u57fa\u4e8e\u7ec6\u5316\u7684\u6d3b\u8dc3\u6027\u8bc1\u660e\u7684\u7ebf\u6027\u5316\u62dc\u5360\u5ead\u5206\u5e03\u5f0f\u5bf9\u8c61<\/p>\n\n\n\n<p><strong>Authors<strong>:\u00a0<\/strong><\/strong><\/p>\n\n\n\n<p>Longfei&nbsp;Qiu,&nbsp;Yoonseung&nbsp;Kim,&nbsp;Ji-Yong&nbsp;Shin,&nbsp;Jieung&nbsp;Kim,&nbsp;Wolf&nbsp;Honor\u00e9,&nbsp;Zhong&nbsp;ShaoAuthors Info &amp; Claims<\/p>\n\n\n\n<p><strong>Key words:<\/strong><\/p>\n\n\n\n<p>distributed systems, consensus protocols, byzantine fault-tolerance, safety, liveness, formal verification, refinement, proof assistants<\/p>\n\n\n\n<p>\u5206\u5e03\u5f0f\u7cfb\u7edf\u3001\u5171\u8bc6\u534f\u8bae\u3001\u62dc\u5360\u5ead\u5bb9\u9519\u3001\u5b89\u5168\u6027\u3001\u6d3b\u6027\u3001\u5f62\u5f0f\u5316\u9a8c\u8bc1\u3001\u7ec6\u5316\u3001\u8bc1\u660e\u52a9\u624b<\/p>\n\n\n\n<p><strong>Abstract<strong>:\u00a0<\/strong><\/strong><\/p>\n\n\n\n<p>Byzantine fault-tolerant state machine replication (SMR) protocols, such as PBFT, HotStuff, and Jolteon, are essential for modern blockchain technologies. However, they are challenging to implement correctly because they have to deal with any unexpected message from byzantine peers and ensure safety and liveness at all times. Many formal frameworks have been developed to verify the safety of SMR implementations, but there is still a gap in the verification of their liveness. Existing liveness proofs are either limited to the network level or do not cover popular partially synchronous protocols.<\/p>\n\n\n\n<p>We introduce LiDO, a consensus model that enables the verification of both safety and liveness of implementations through refinement. We observe that current consensus models cannot handle liveness because they do not include a pacemaker state. We show that by adding a pacemaker state to the LiDO model, we can express the liveness properties of SMR protocols as a few safety properties that can be easily verified by refinement proofs. Based on our LiDO model, we provide mechanized safety and liveness proofs for both unpipelined and pipelined Jolteon in Coq. This is the first mechanized liveness proof for a byzantine consensus protocol with non-trivial optimizations such as pipelining.<\/p>\n\n\n<div class=\"wp-block-image\">\n<figure class=\"aligncenter size-full is-resized\"><img loading=\"lazy\" decoding=\"async\" width=\"627\" height=\"570\" src=\"https:\/\/www.ndnlab.com\/wp-content\/uploads\/2024\/08\/image-39.png\"  class=\"wp-image-392\" style=\"width:500px\" srcset=\"https:\/\/www.ndnlab.com\/wp-content\/uploads\/2024\/08\/image-39.png 627w, https:\/\/www.ndnlab.com\/wp-content\/uploads\/2024\/08\/image-39-300x273.png 300w\" sizes=\"auto, (max-width: 627px) 100vw, 627px\" title=\"LiDO: Linearizable Byzantine Distributed Objects with Refinement-Based Liveness Proofs\u63d2\u56fe\" alt=\"LiDO: Linearizable Byzantine Distributed Objects with Refinement-Based Liveness Proofs\u63d2\u56fe\" \/><\/figure>\n<\/div>\n\n\n<p>\u62dc\u5360\u5ead\u5f0f\u5bb9\u9519\u72b6\u6001\u673a\u590d\u5236(SMR)\u534f\u8bae\uff0c\u5982PBFT\u3001HotStuff\u548cJolteon\uff0c\u5bf9\u4e8e\u73b0\u4ee3\u533a\u5757\u94fe\u6280\u672f\u81f3\u5173\u91cd\u8981\u3002\u7136\u800c\uff0c\u6b63\u786e\u5b9e\u73b0\u5b83\u4eec\u662f\u5177\u6709\u6311\u6218\u6027\u7684\uff0c\u56e0\u4e3a\u5b83\u4eec\u5fc5\u987b\u5904\u7406\u6765\u81ea\u62dc\u5360\u5ead\u5bf9\u7b49\u4f53\u7684\u4efb\u4f55\u610f\u5916\u6d88\u606f\uff0c\u5e76\u59cb\u7ec8\u786e\u4fdd\u5b89\u5168\u6027\u548c\u6d3b\u52a8\u6027\u3002\u5df2\u7ecf\u5f00\u53d1\u4e86\u8bb8\u591a\u6b63\u5f0f\u7684\u6846\u67b6\u6765\u9a8c\u8bc1SMR\u5b9e\u73b0\u7684\u5b89\u5168\u6027\uff0c\u4f46\u662f\u5728\u9a8c\u8bc1\u5176\u6709\u6548\u6027\u65b9\u9762\u4ecd\u7136\u5b58\u5728\u5dee\u8ddd\u3002\u73b0\u6709\u7684\u52a8\u6001\u8bc1\u660e\u8981\u4e48\u5c40\u9650\u4e8e\u7f51\u7edc\u7ea7\u522b\uff0c\u8981\u4e48\u4e0d\u6db5\u76d6\u6d41\u884c\u7684\u90e8\u5206\u540c\u6b65\u534f\u8bae\u3002<\/p>\n\n\n\n<p>\u6211\u4eec\u4ecb\u7ecd\u4e86LiDO\uff0c\u8fd9\u662f\u4e00\u4e2a\u5171\u8bc6\u6a21\u578b\uff0c\u53ef\u4ee5\u901a\u8fc7\u6539\u8fdb\u6765\u9a8c\u8bc1\u5b9e\u73b0\u7684\u5b89\u5168\u6027\u548c\u6d3b\u52a8\u6027\u3002\u6211\u4eec\u89c2\u5bdf\u5230\uff0c\u76ee\u524d\u7684\u5171\u8bc6\u6a21\u578b\u4e0d\u80fd\u5904\u7406\u6d3b\u8dc3\u6027\uff0c\u56e0\u4e3a\u5b83\u4eec\u4e0d\u5305\u62ec\u8d77\u640f\u5668\u72b6\u6001\u3002\u6211\u4eec\u8868\u660e\uff0c\u901a\u8fc7\u5728LiDO\u6a21\u578b\u4e2d\u6dfb\u52a0\u8d77\u640f\u5668\u72b6\u6001\uff0c\u6211\u4eec\u53ef\u4ee5\u5c06SMR\u534f\u8bae\u7684\u6d3b\u6027\u5c5e\u6027\u8868\u793a\u4e3a\u51e0\u4e2a\u53ef\u4ee5\u901a\u8fc7\u6539\u8fdb\u8bc1\u660e\u8f7b\u677e\u9a8c\u8bc1\u7684\u5b89\u5168\u5c5e\u6027\u3002\u57fa\u4e8e\u6211\u4eec\u7684LiDO\u6a21\u578b\uff0c\u6211\u4eec\u4e3aCoq\u7684\u672a\u7ba1\u9053\u548c\u7ba1\u9053Jolteon\u63d0\u4f9b\u4e86\u673a\u68b0\u5316\u5b89\u5168\u6027\u548c\u6d3b\u52a8\u6027\u8bc1\u660e\u3002\u8fd9\u662f\u9996\u4e2a\u5bf9\u62dc\u5360\u5ead\u5171\u8bc6\u534f\u8bae\u8fdb\u884c\u975e\u5e73\u51e1\u4f18\u5316(\u5982\u6d41\u6c34\u7ebf)\u7684\u673a\u68b0\u5316\u6d3b\u6027\u8bc1\u660e\u3002<\/p>\n\n\n<div class=\"wp-block-image\">\n<figure class=\"aligncenter size-large is-resized\"><img loading=\"lazy\" decoding=\"async\" width=\"1024\" height=\"344\" src=\"https:\/\/www.ndnlab.com\/wp-content\/uploads\/2024\/08\/image-40-1024x344.png\"  class=\"wp-image-393\" style=\"width:500px\" srcset=\"https:\/\/www.ndnlab.com\/wp-content\/uploads\/2024\/08\/image-40-1024x344.png 1024w, https:\/\/www.ndnlab.com\/wp-content\/uploads\/2024\/08\/image-40-300x101.png 300w, https:\/\/www.ndnlab.com\/wp-content\/uploads\/2024\/08\/image-40-768x258.png 768w, https:\/\/www.ndnlab.com\/wp-content\/uploads\/2024\/08\/image-40.png 1079w\" sizes=\"auto, (max-width: 1024px) 100vw, 1024px\" title=\"LiDO: Linearizable Byzantine Distributed Objects with Refinement-Based Liveness Proofs\u63d2\u56fe1\" alt=\"LiDO: Linearizable Byzantine Distributed Objects with Refinement-Based Liveness Proofs\u63d2\u56fe1\" \/><\/figure>\n<\/div>\n\n<div class=\"wp-block-image\">\n<figure class=\"aligncenter size-full is-resized\"><img loading=\"lazy\" decoding=\"async\" width=\"523\" height=\"314\" src=\"https:\/\/www.ndnlab.com\/wp-content\/uploads\/2024\/08\/image-30.png\"  class=\"wp-image-383\" style=\"width:500px\" srcset=\"https:\/\/www.ndnlab.com\/wp-content\/uploads\/2024\/08\/image-30.png 523w, https:\/\/www.ndnlab.com\/wp-content\/uploads\/2024\/08\/image-30-300x180.png 300w\" sizes=\"auto, (max-width: 523px) 100vw, 523px\" title=\"LiDO: Linearizable Byzantine Distributed Objects with Refinement-Based Liveness Proofs\u63d2\u56fe2\" alt=\"LiDO: Linearizable Byzantine Distributed Objects with Refinement-Based Liveness Proofs\u63d2\u56fe2\" \/><\/figure>\n<\/div>\n\n<div class=\"wp-block-image\">\n<figure class=\"aligncenter size-full is-resized\"><img loading=\"lazy\" decoding=\"async\" width=\"701\" height=\"453\" src=\"https:\/\/www.ndnlab.com\/wp-content\/uploads\/2024\/08\/image-31.png\"  class=\"wp-image-384\" style=\"width:500px\" srcset=\"https:\/\/www.ndnlab.com\/wp-content\/uploads\/2024\/08\/image-31.png 701w, https:\/\/www.ndnlab.com\/wp-content\/uploads\/2024\/08\/image-31-300x194.png 300w\" sizes=\"auto, (max-width: 701px) 100vw, 701px\" title=\"LiDO: Linearizable Byzantine Distributed Objects with Refinement-Based Liveness Proofs\u63d2\u56fe3\" alt=\"LiDO: Linearizable Byzantine Distributed Objects with Refinement-Based Liveness Proofs\u63d2\u56fe3\" \/><\/figure>\n<\/div>\n\n<div class=\"wp-block-image\">\n<figure class=\"aligncenter size-large is-resized\"><img loading=\"lazy\" decoding=\"async\" width=\"1024\" height=\"308\" src=\"https:\/\/www.ndnlab.com\/wp-content\/uploads\/2024\/08\/image-32-1024x308.png\"  class=\"wp-image-385\" style=\"width:500px\" srcset=\"https:\/\/www.ndnlab.com\/wp-content\/uploads\/2024\/08\/image-32-1024x308.png 1024w, https:\/\/www.ndnlab.com\/wp-content\/uploads\/2024\/08\/image-32-300x90.png 300w, https:\/\/www.ndnlab.com\/wp-content\/uploads\/2024\/08\/image-32-768x231.png 768w, https:\/\/www.ndnlab.com\/wp-content\/uploads\/2024\/08\/image-32.png 1035w\" sizes=\"auto, (max-width: 1024px) 100vw, 1024px\" title=\"LiDO: Linearizable Byzantine Distributed Objects with Refinement-Based Liveness Proofs\u63d2\u56fe4\" alt=\"LiDO: Linearizable Byzantine Distributed Objects with Refinement-Based Liveness Proofs\u63d2\u56fe4\" \/><\/figure>\n<\/div>\n\n<div class=\"wp-block-image\">\n<figure class=\"aligncenter size-large is-resized\"><img loading=\"lazy\" decoding=\"async\" width=\"1024\" height=\"518\" src=\"https:\/\/www.ndnlab.com\/wp-content\/uploads\/2024\/08\/image-33-1024x518.png\"  class=\"wp-image-386\" style=\"width:500px\" srcset=\"https:\/\/www.ndnlab.com\/wp-content\/uploads\/2024\/08\/image-33-1024x518.png 1024w, https:\/\/www.ndnlab.com\/wp-content\/uploads\/2024\/08\/image-33-300x152.png 300w, https:\/\/www.ndnlab.com\/wp-content\/uploads\/2024\/08\/image-33-768x389.png 768w, https:\/\/www.ndnlab.com\/wp-content\/uploads\/2024\/08\/image-33.png 1073w\" sizes=\"auto, (max-width: 1024px) 100vw, 1024px\" title=\"LiDO: Linearizable Byzantine Distributed Objects with Refinement-Based Liveness Proofs\u63d2\u56fe5\" alt=\"LiDO: Linearizable Byzantine Distributed Objects with Refinement-Based Liveness Proofs\u63d2\u56fe5\" \/><\/figure>\n<\/div>\n\n<div class=\"wp-block-image\">\n<figure class=\"aligncenter size-full is-resized\"><img loading=\"lazy\" decoding=\"async\" width=\"569\" height=\"277\" src=\"https:\/\/www.ndnlab.com\/wp-content\/uploads\/2024\/08\/image-34.png\"  class=\"wp-image-387\" style=\"width:500px\" srcset=\"https:\/\/www.ndnlab.com\/wp-content\/uploads\/2024\/08\/image-34.png 569w, https:\/\/www.ndnlab.com\/wp-content\/uploads\/2024\/08\/image-34-300x146.png 300w\" sizes=\"auto, (max-width: 569px) 100vw, 569px\" title=\"LiDO: Linearizable Byzantine Distributed Objects with Refinement-Based Liveness Proofs\u63d2\u56fe6\" alt=\"LiDO: Linearizable Byzantine Distributed Objects with Refinement-Based Liveness Proofs\u63d2\u56fe6\" \/><\/figure>\n<\/div>\n\n<div class=\"wp-block-image\">\n<figure class=\"aligncenter size-full is-resized\"><img loading=\"lazy\" decoding=\"async\" width=\"842\" height=\"433\" src=\"https:\/\/www.ndnlab.com\/wp-content\/uploads\/2024\/08\/image-35.png\"  class=\"wp-image-388\" style=\"width:500px\" srcset=\"https:\/\/www.ndnlab.com\/wp-content\/uploads\/2024\/08\/image-35.png 842w, https:\/\/www.ndnlab.com\/wp-content\/uploads\/2024\/08\/image-35-300x154.png 300w, https:\/\/www.ndnlab.com\/wp-content\/uploads\/2024\/08\/image-35-768x395.png 768w\" sizes=\"auto, (max-width: 842px) 100vw, 842px\" title=\"LiDO: Linearizable Byzantine Distributed Objects with Refinement-Based Liveness Proofs\u63d2\u56fe7\" alt=\"LiDO: Linearizable Byzantine Distributed Objects with Refinement-Based Liveness Proofs\u63d2\u56fe7\" \/><\/figure>\n<\/div>\n\n<div class=\"wp-block-image\">\n<figure class=\"aligncenter size-full is-resized\"><img loading=\"lazy\" decoding=\"async\" width=\"465\" height=\"368\" src=\"https:\/\/www.ndnlab.com\/wp-content\/uploads\/2024\/08\/image-36.png\"  class=\"wp-image-389\" style=\"width:500px\" srcset=\"https:\/\/www.ndnlab.com\/wp-content\/uploads\/2024\/08\/image-36.png 465w, https:\/\/www.ndnlab.com\/wp-content\/uploads\/2024\/08\/image-36-300x237.png 300w\" sizes=\"auto, (max-width: 465px) 100vw, 465px\" title=\"LiDO: Linearizable Byzantine Distributed Objects with Refinement-Based Liveness Proofs\u63d2\u56fe8\" alt=\"LiDO: Linearizable Byzantine Distributed Objects with Refinement-Based Liveness Proofs\u63d2\u56fe8\" \/><\/figure>\n<\/div>\n\n<div class=\"wp-block-image\">\n<figure class=\"aligncenter size-full is-resized\"><img loading=\"lazy\" decoding=\"async\" width=\"495\" height=\"285\" src=\"https:\/\/www.ndnlab.com\/wp-content\/uploads\/2024\/08\/image-37.png\"  class=\"wp-image-390\" style=\"width:500px\" srcset=\"https:\/\/www.ndnlab.com\/wp-content\/uploads\/2024\/08\/image-37.png 495w, https:\/\/www.ndnlab.com\/wp-content\/uploads\/2024\/08\/image-37-300x173.png 300w\" sizes=\"auto, (max-width: 495px) 100vw, 495px\" title=\"LiDO: Linearizable Byzantine Distributed Objects with Refinement-Based Liveness Proofs\u63d2\u56fe9\" alt=\"LiDO: Linearizable Byzantine Distributed Objects with Refinement-Based Liveness Proofs\u63d2\u56fe9\" \/><\/figure>\n<\/div>\n\n<div class=\"wp-block-image\">\n<figure class=\"aligncenter size-full is-resized\"><img loading=\"lazy\" decoding=\"async\" width=\"387\" height=\"283\" src=\"https:\/\/www.ndnlab.com\/wp-content\/uploads\/2024\/08\/image-38.png\"  class=\"wp-image-391\" style=\"width:500px\" srcset=\"https:\/\/www.ndnlab.com\/wp-content\/uploads\/2024\/08\/image-38.png 387w, https:\/\/www.ndnlab.com\/wp-content\/uploads\/2024\/08\/image-38-300x219.png 300w\" sizes=\"auto, (max-width: 387px) 100vw, 387px\" title=\"LiDO: Linearizable Byzantine Distributed Objects with Refinement-Based Liveness Proofs\u63d2\u56fe10\" alt=\"LiDO: Linearizable Byzantine Distributed Objects with Refinement-Based Liveness Proofs\u63d2\u56fe10\" \/><\/figure>\n<\/div>\n\n\n<p>\u8bba\u6587\u8be6\u60c5\uff1a<a href=\"https:\/\/dl.acm.org\/doi\/10.1145\/3656423\">https:\/\/dl.acm.org\/doi\/10.1145\/3656423<\/a><\/p>\n\n\n\n<p>PDF\uff1ahttps:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3656423<\/p>\n","protected":false},"excerpt":{"rendered":"<p>LiDO\uff1a\u5177\u6709\u57fa\u4e8e\u7ec6\u5316\u7684\u6d3b\u8dc3\u6027\u8bc1\u660e\u7684\u7ebf\u6027\u5316\u62dc\u5360\u5ead\u5206\u5e03\u5f0f\u5bf9\u8c61 Authors:\u00a0 Longfei&nbsp;Qiu,&nbsp;Yoonseung&nbsp;Kim,&nbsp;Ji-Yong&nbsp;Shin,&nbsp;Jieung&nbsp;Kim,&nbsp;Wolf&nbsp;Honor\u00e9,&nbsp;Zhong&nbsp;ShaoAuthors Info &amp; Claims Key words: distributed systems, consensus  &hellip; <a href=\"https:\/\/www.ndnlab.com\/?p=379\">\u7ee7\u7eed\u9605\u8bfb <span class=\"meta-nav\">&rarr;<\/span><\/a><\/p>\n","protected":false},"author":1,"featured_media":381,"comment_status":"closed","ping_status":"closed","sticky":false,"template":"","format":"standard","meta":{"footnotes":""},"categories":[4,6],"tags":[],"class_list":["post-379","post","type-post","status-publish","format-standard","has-post-thumbnail","hentry","category-blockchain","category-weilaiwangluo"],"_links":{"self":[{"href":"https:\/\/www.ndnlab.com\/index.php?rest_route=\/wp\/v2\/posts\/379","targetHints":{"allow":["GET"]}}],"collection":[{"href":"https:\/\/www.ndnlab.com\/index.php?rest_route=\/wp\/v2\/posts"}],"about":[{"href":"https:\/\/www.ndnlab.com\/index.php?rest_route=\/wp\/v2\/types\/post"}],"author":[{"embeddable":true,"href":"https:\/\/www.ndnlab.com\/index.php?rest_route=\/wp\/v2\/users\/1"}],"replies":[{"embeddable":true,"href":"https:\/\/www.ndnlab.com\/index.php?rest_route=%2Fwp%2Fv2%2Fcomments&post=379"}],"version-history":[{"count":2,"href":"https:\/\/www.ndnlab.com\/index.php?rest_route=\/wp\/v2\/posts\/379\/revisions"}],"predecessor-version":[{"id":394,"href":"https:\/\/www.ndnlab.com\/index.php?rest_route=\/wp\/v2\/posts\/379\/revisions\/394"}],"wp:featuredmedia":[{"embeddable":true,"href":"https:\/\/www.ndnlab.com\/index.php?rest_route=\/wp\/v2\/media\/381"}],"wp:attachment":[{"href":"https:\/\/www.ndnlab.com\/index.php?rest_route=%2Fwp%2Fv2%2Fmedia&parent=379"}],"wp:term":[{"taxonomy":"category","embeddable":true,"href":"https:\/\/www.ndnlab.com\/index.php?rest_route=%2Fwp%2Fv2%2Fcategories&post=379"},{"taxonomy":"post_tag","embeddable":true,"href":"https:\/\/www.ndnlab.com\/index.php?rest_route=%2Fwp%2Fv2%2Ftags&post=379"}],"curies":[{"name":"wp","href":"https:\/\/api.w.org\/{rel}","templated":true}]}}