使用 F* 验证 Merkle Patricia 树库
编程语言
2021-06-10 v1 密码学与安全
软件工程
摘要
Merkle 树是一种将键值存储表示为树的数据结构。Merkle 树的每个节点都配备由其后代节点计算得到的哈希值。Merkle 树常用于表示区块链系统的状态，因为它可用于以无信任方式高效审计状态。由于区块链的安全关键性质，确保其实现的正确性至关重要。我们展示了使用 F* 对 Plebeia 核心部分的形式化验证实现。Plebeia 是一个操作 Merkle 树扩展（称为 Plebeia 树）的库，正作为 Tezos 区块链系统存储系统的一部分被实现。为此，我们将 Plebeia 逐步移植到 F*；从移植到 F* 的模块中提取的 OCaml 代码与 Plebeia 未验证部分链接。通过这种逐步移植过程，我们可以从部分验证的 Plebeia 实现中获得可工作代码；我们确认该二进制文件通过了 Plebeia 的所有单元测试。更具体地，我们验证了 Plebeia 实现上的以下性质：(1) 每个树操作函数保持 Plebeia 树数据结构的不变式，并满足作为嵌套键值存储的功能需求；(2) 每个将 Plebeia 树序列化/反序列化到低级存储/从低级存储反序列化的函数均被正确实现；(3) 相对于 blake2b 哈希函数的密码学安全性，Plebeia 树的哈希函数具有相对抗碰撞性。在将 Plebeia 移植到 F* 期间，我们在 Plebeia 的旧版本中发现了一个被原实现所附测试遗漏的 bug。据我们所知，这是首个使用 F* 验证生产级 Merkle 树库实现的工作。
引用
@article{arxiv.2106.04826,
title = {Verification of a Merkle Patricia Tree Library Using F*},
author = {Sota Sato and Ryotaro Banno and Jun Furuse and Kohei Suenaga and Atsushi Igarashi},
journal= {arXiv preprint arXiv:2106.04826},
year = {2021}
}