WIP：在Coq中正式确定Concordium共识协议
作者：
Thomas Dinsdale-Young
Concordium Ap S，Aarhus大学
Søren Eller Thomsen
Aarhus大学计算机科学
2019年计算机机械协会。
Bas Spitters
Aarhus大学计算机科学
Daniel Tschudi
Aarhus大学计算机科学
PDF下载链接：https://kdocs.cn/l/sIIP17EeZ?f=111
[文档] WIP：在Coq中正式确定Concordium共识协议_translate.pdf
ACM参考格式：
Thomas Dinsdale-Young, Bas Spitters, Søren Eller Thomsen, 和Daniel Tschudi。2019. WIP：在Coq中将Concordium共识协议正规化。 《编程语言Coq讲习班会议记录》（Coq PL19）。 2 ACM，纽约，纽约，美国，2页。
我们报告了Coq的工业应用：我们的工作是使Concordium区块链共识协议正规化。 这项工作目前处于NDA之下，但我们希望能够在Coq正式发布前公布更多信息。最终，所有代码都将在允许的开源许可下发布。这项工作是Concordium和Aarhus大学之间的合作。
Concordium共识协议是一个可证安全的安全保证（POS）协议，在Haskell中有一个原型实现。 我们的目标是将crep-tographic安全证明与Haskell实现连接起来。 理想情况下，我们要么使用Coq的提取机制，要么使用hs-to-coq[ SB RW17]将形式化与Haskell实现连接起来。 我们的工作松散地基于Coq[PS18]中的Toychain形式化。Toychain是一种改进的类比特币工作证明(PoW)协议。像toychain一样，我们构建数学组件库。
正式化PoS协议本质上不同于正式化PoW协议。 在PoS中，块的正确性不是固定在特定的块上，而是固定在特定的插槽上。然而，基于[BM TZ17]，我们的目标是找到一个良好的模块化协议。 这将允许PoS和PoW协议的共同推广。
在我们的Coq正式化中，我们从点对点层中抽象出来，并将一个理想的半同步网络功能形式化。在Toychain中，每一个对等点都会向所有的对等点传递一条消息，该消息包含当前块的散列，每次该对等点接收到一个块。
我们验证了一个没有信息冗余的协议。在研讨会上，我们将介绍该协议的Coq实现及其功能正确性。
为了证明安全性，我们需要添加概率计算。这允许我们添加加密原语，如散列函数。为了做到这一点，我们将在Coq中使用一个概率库:要么是来自信息论[AG15]的一个，接着是toychain [GS18]的一个继承者，要么是用于形式的经典数学组件分析库整理easycrypt背后的逻辑。
接下来，我们将需要对对手进行推理。这很可能结合了easycrypt [HKO+18, ABB+18]中mul- tiparty计算的形式化思想，以及抽象密码框架[BDLKK18, Mau11]的见解和比特币的理性分析[BGM+18]。
最后，为了支持使用提取的代码可以是有效的，我们提到了令人印象深刻的工作筏(每个任务)的共识协议，这是正式在Coq使用verdi框架[WWP+15, WWA+16]。证明了该协议是可线性化的，并提出了一种高效的协议实现方法，使协议的性能达到了最先进的水平。一个小型的可信shim将提取的功能代码连接到正在运行的分布式代码。
Concordium的目标是与其他科技含量高的公司合作，共同努力为区块链制定清晰的质量标准。在这节课的最后，我们邀请讨论Coq如何在这个过程中得到最好的应用。
声明
本文允许为个人或课堂使用而制作本作品的全部或部分的数字或硬拷贝，但不得用作商用，条件是副本不是为了利润或商业利益而制作或分发的，并且副本在第一页上附有本通知和完整的引文。除了ACM以外，其他人拥有的作品的版权必须得到尊重。 允许信用提取。 以其他方式复制或重新发布，在服务器上发布或重新分发到列表，需要事先的特定许可和/或费用。请邮件与permissions@acm.org.获取许可。
Coq PL19，2019年1月19日，美国纽约
致谢
Ilya Sergey致力于帮助他们即将进行的比特币主干协议正规化工作。
这项工作得到了丹麦Aarhus大学Concordium区块链研究中心的支持。
[ABB+18] José Bacelar Almeida, Manuel Barbosa, Gilles Barthe, Hugo Pacheco, Vitor Pereira, and Bernardo Portela. Enforcing ideal- world leakage bounds in real-world secret sharing MPC frame- works. In 31st IEEE Computer Security Foundations Symposium, CSF 2018, Oxford, United Kingdom, July 9-12, 2018 [DBL18],
[AG15] Reynald Affeldt and Jacques Garrigue. Formalization of error- correcting codes: from hamming to modern coding theory. In International Conference on Interactive Theorem Proving, pages17–33. Springer, 2015.
[BDLKK18] Chris Brzuska, Antoine Delignat-Lavaud, Konrad Kohbrok, and Markulf Kohlweiss. State-separating proofs: A reduc- tion methodology for real-world protocols. Cryptology ePrint Archive, Report 2018/306, 2018. https://eprint.iacr.org/2018/306.
[BGM+18] Christian Badertscher, Juan Garay, Ueli Maurer, Daniel Tschudi,
and Vassilis Zikas. But why does it work? a rational protocol design treatment of bitcoin. In Annual International Conference on the Theory and Applications of Cryptographic Techniques,pages 34–65. Springer, 2018.
[BMTZ17] Christian Badertscher, Ueli Maurer, Daniel Tschudi, and Vas- silis Zikas. Bitcoin as a transaction ledger: A composable treat- ment. In Annual International Cryptology Conference, pages324–356. Springer, 2017.
[DBL18] 31st IEEE Computer Security Foundations Symposium, CSF 2018, Oxford, United Kingdom, July 9-12, 2018. IEEE Computer Soci-ety, 2018.
[GS18] Kiran Gopinathan and Ilya Sergey. Towards mechanising prob- abilistic properties of a blockchain. In CoqPL 2019 The Fifth
International Workshop on Coq for Programming Languages,2018.
[HKO+18] Helene Haagh, Aleksandr Karbyshev, Sabine Oechsner, Bas
Spitters, and Pierre-Yves Strub. Computer-aided proofs for multiparty computation with active security. In 31st IEEE Computer Security Foundations Symposium, CSF 2018, Oxford,United Kingdom, July 9-12, 2018 [DBL18], pages 119–131.
[Mau11] Ueli Maurer. Constructive cryptography–a new paradigm for security definitions and proofs. In Theory of Security andApplications, pages 33–56. Springer, 2011.
[PS18] George Pîrlea and Ilya Sergey. Mechanising blockchain con- sensus. In Proceedings of the 7th ACM SIGPLAN International Conference on Certified Programs and Proofs, pages 78–90. ACM,2018.
[SBRW17] Antal Spector-Zabusky, Joachim Breitner, Christine Rizkallah, and Stephanie Weirich. Total haskell is reasonable coq. CoRR,abs/1711.09286, 2017.
[WWA+16] Doug Woos, James R. Wilcox, Steve Anton, Zachary Tatlock,
Michael D. Ernst, and Thomas Anderson. Planning for change in a formal verification of the raft consensus protocol. In Proceedings of the 5th ACM SIGPLAN Conference on Certified Programs and Proofs, CPP 2016, pages 154–165, New York, NY,USA, 2016. ACM.
[WWP+15] James R. Wilcox, Doug Woos, Pavel Panchekha, Zachary Tat-
lock, Xi Wang, Michael D. Ernst, and Thomas Anderson. Verdi: A framework for implementing and formally verifying dis- tributed systems. In Proceedings of the 36th ACM SIGPLAN Conference on Programming Language Design and Implemen- tation, PLDI ’15, pages 357–368, New York, NY, USA, 2015. ACM.
