面向高并发软件系统的动态缺陷检测技术研究

Software bugs make software less available and reliable, and may even cause serious loss on human lives, economy and national security. As a major approach in guaranteeing software safety, dynamic bug detection techniques are widely used in practice. However, as software becomes more concurrent and complex, the state space of software gets more complicated, which further poses great challenges on bug detection techniques. Existing solutions cannot handle diverse concurrent platforms and achieve a good balance between detection efficiency and accuracy, thus are insufficient in practice. This proposal targets at concurrent software and exploring practical dynamic bug detection techniques. First, this proposal plans to define a unified formalization framework which is compatible across diverse concurrency. Moreover, this proposal aims at improving the detection efficiency and accuracy based on fuzzing testing and symbolic execution. Support tools will be developed in this proposal and applied in practical real-world software systems to help find real bugs and improve the reliability of software.

软件缺陷对软件的可用性、可靠性带来了巨大隐患，甚至能够造成重大的生命财产、社会经济、国家安全的损失。动态缺陷检测技术在软件开发全生命周期是最主要的保障手段，并且在工业级场景中有着广泛的应用。然而，伴随着软件系统的高并发化，软件的运行时状态更为复杂，对缺陷检测技术提出了新的理论难题和工程应用挑战。现有的动态缺陷检测技术对于多样性复杂并发环境的支持程度有限、检测效率不足、覆盖率难以保障，因此不足以有效应用于实用软件系统的缺陷检测中。本项目面向软件运行时的高并发环境，研究实用化的动态缺陷检测技术。本项目首先拟研究统一的并发语义抽取方法，用于建模软件中所包含的不同并发特性。此外，本项目拟研究基于模糊测试和符号执行技术的高效动态缺陷检测框架，提高检测过程的效率和对软件程序代码的覆盖率。本项目还将输出支撑工具，并对实用软件进行缺陷检测，从而辅助复杂软件质量保障过程，提高软件的可用、可靠性。

“软件定义”将成为软件和信息技术服务业发展的突出特征。“软件定义”也将渗透至智能制造、工业生产、国防安全、国民经济的各行业领域之中，催生一批新的产业主体、业务平台、融合性业态和新型消费。伴随着软件行业的飞速发展，软件安全、可信、可靠的问题成为了影响产业良性升级的重要因素。而软件缺陷，成为了影响软件质量的重要来源和指标性因素。软件缺陷的存在，一方面降低了软件质量，影响了业务服务性能，从而提高了软件开发过程中的开销和成本，带来了经济算是。另一方面，软件缺陷可能造成严重的安全问题，威胁社会稳定。并发软件作为重要的软件类型，同样存在严重的缺陷问题，并且由于其高并发运行环境，形成了更严峻的挑战。..本项目针对高并发软件系统的软件质量与安全问题，重点从三个方面进行了系统性研究，分别是系统并发语义的统一形式化描述及自动化抽取方法、面向并发环境的导向型模糊测试技术和基于符号执行的并发路径覆盖技术研究。课题研究中，首先形成了对于多线程、微服务、区块链等多类并发软件环境下的并发语义定义框架，支持对异构软件语义的形式化定义和描述。其次，课题提出了在二进制字节码层面上的基于软件依赖关系导向的自动化分析框架，能够解决并发软件状态空间难以遍历覆盖的问题。最后，课题提出了基于符号执行技术的并发软件分析算法，能够有效解决内存的建模精度问题。在此基础上，课题实现了面向不同并发环境的自动化缺陷检测工具集，并在区块链场景下进行了大规模缺陷检测，实现了对于EVM和WASM等主流架构的支持，并在分析精度和效率上优于同类型方法和工具。本课题对于并发软件缺陷分析的根本性挑战进行了研究，对并发软件抽象建模和自动化分析方向具有较高的科学意义。