一句话:提出 Upbeat,一种针对 Q# 量子库输入检查缺陷的模糊测试工具,自动生成测试用例并发现 16 个缺陷。
Q# 等高层量子编程模型依赖基础库,但库实现对用户可见子程序输入的取值、长度和量子态等属性可能缺乏或不完整检查,从而引入错误。本文提出 Upbeat,一种用于生成 Q# 库输入检查相关缺陷测试用例的模糊测试工具。Upbeat 自动从 API 文档和开发者编写的输入检查语句中提取约束,并利用开源 Q# 代码样本合成测试程序;它将测试用例生成分别建模为经典计算中的约束满足问题和量子计算中的量子态模型,以生成有针对性的子程序输入。在不足 100 小时的自动测试中,Upbeat 在 API 实现中发现 16 个缺陷和 4 个文档错误,其中 14 个被确认,12 个已被库开发者修复。
High-level programming models like Q# significantly simplify the complexity of programming for quantum computing. These models are supported by a set of foundation libraries for code development. However, errors can occur in the library implementation, and one common root cause is the lack of or incomplete checks on properties like values, length, and quantum states of inputs passed to user-facing subroutines. This paper presents Upbeat, a fuzzing tool to generate random test cases for bugs related to input checking in Q# libraries. Upbeat develops an automated process to extract constraints from the API documentation and the developer implemented input-checking statements. It leverages open-source Q# code samples to synthesize test programs. It frames the test case generation as a constraint satisfaction problem for classical computing and a quantum state model for quantum computing to produce carefully generated subroutine inputs to test if the input-checking mechanism is appropriately implemented. Under 100 hours of automated test runs, Upbeat has successfully identified 16 bugs in API implementations and 4 documentation errors. Of these, 14 have been confirmed, and 12 have been fixed by the library developers.
@inproceedings{paperbot8562,
title = {UPBEAT: Test Input Checks of Q# Quantum Libraries},
author = {Tianmin Hu and Guixin Ye and Zhanyong Tang and Shin Hwei Tan and Huanting Wang and Meng Li and Zheng Wang},
booktitle = {ISSTA},
year = {2024},
doi = {10.1145/3650212.3652120}
}