Random testing of a higher-order blockchain language (experience report)
Random testing of a higher-order blockchain language (experience report)
复制标题
高阶区块链语言的随机测试（体验报告）
DOI：
10.1145/3547653
复制
发表时间：
2022
影响因子：
--
通讯作者：
Sergey, Ilya
中科院分区：
文献类型：
--
作者：
Hoang, Tram;Trunov, Anton;Lampropoulos, Leonidas;Sergey, Ilya
我们描述了我们使用基于属性的测试的经验-一种用于 自动生成随机输入以检查可执行程序 规范--在开发高阶智能合约语言， 为最先进的区块链提供动力，每天有数千名活跃用户。我们概述了整合QuickChick的过程-一个用于 建立在Coq证明助手之上的基于属性的测试-成为一个 OCaml中的真实语言实现。我们讨论我们面临的挑战 在为现实的高阶程序生成良好类型的程序时遇到的 智能合约语言，混合了纯函数式和命令式 计算和功能运行时资源会计。我们描述了一组 我们测试的语言实现属性，以及语义 进行验证所需的线束。属性的范围从 标准类型安全性与所使用的控制和类型流分析的可靠性之间的关系 优化编译器。最后，我们列出了发现的bug列表， 在QuickChick的帮助下重新发现，并讨论其严重性和可能的 后果
We describe our experience of using property-based testing---an approach for automatically generating random inputs to check executable program specifications---in a development of a higher-order smart contract language that powers a state-of-the-art blockchain with thousands of active daily users.We outline the process of integrating QuickChick---a framework for property-based testing built on top of the Coq proof assistant---into a real-world language implementation in OCaml. We discuss the challenges we have encountered when generating well-typed programs for a realistic higher-order smart contract language, which mixes purely functional and imperative computations and features runtime resource accounting. We describe the set of the language implementation properties that we tested, as well as the semantic harness required to enable their validation. The properties range from the standard type safety to the soundness of a control- and type-flow analysis used by the optimizing compiler. Finally, we present the list of bugs discovered and rediscovered with the help of QuickChick and discuss their severity and possible ramifications.
登录
查看更多内容
数字合约的资源感知会话类型
DOI：
10.1109/csf51468.2021.00004
发表时间：
2021
期刊：
2021 IEEE 34th Computer Security Foundations Symposium (CSF
影响因子：
--
作者：
Das, Ankush;Balzer, Stephanie;Hoffmann, Jan;Pfenning, Frank;Santurkar, Ishani
通讯作者：
Santurkar, Ishani
代表单子
DOI：
10.1145/174675.178047
发表时间：
1994
期刊：
SSRN Electronic Journal
影响因子：
--
作者：
Andrzej Filinski
通讯作者：
Andrzej Filinski
一元抽象解释器
DOI：
10.1145/2491956.2491979
发表时间：
2013
期刊：
Proceedings of the 34th ACM SIGPLAN Conference on Programming Language Design and Implementation
影响因子：
--
作者：
Ilya Sergey;Dominique Devriese;M. Might;Jan Midtgaard;David Darais;D. Clarke;Frank Piessens
通讯作者：
Frank Piessens
MLton 中的整个程序编译
DOI：
10.1145/1159876.1159877
发表时间：
2006
期刊：
Higher-Order and Symbolic Computation
影响因子：
--
作者：
Stephen Weeks
通讯作者：
Stephen Weeks
具有所有权和交换性分析的实用智能合约分片
DOI：
--
发表时间：
2021
期刊：
ACM-SIGPLAN Symposium on Programming Language Design and Implementation
影响因子：
--
作者：
George Pîrlea;Amrit Kumar;Ilya Sergey
通讯作者：
Ilya Sergey