Random Testing of a Higher-Order Blockchain Language (Experience Report)

【Author】 Hoang, Tram; Trunov, Anton; Lampropoulos, Leonidas; Sergey, Ilya

【Source】PROCEEDINGS OF THE ACM ON PROGRAMMING LANGUAGES-PACMPL

【影响因子】0.000

【Abstract】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.

【Keywords】random testing; property-based testing; definitional interpreters; higher-order control-flow analysis; smart contracts; QuickChick; Scilla

【发表时间】2022 AUG

【收录时间】2022-09-22

【文献类型】实验仿真

【主题类别】

区块链技术-核心技术-智能合约