Tools and Algorithms for the Construction and Analysis of Systems - 29th International Conference, TACAS 2023, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2023, Paris, France, April 22-27, 2023, Proceedings, Part II
Tools and Algorithms for the Construction and Analysis of Systems - 29th International Conference, TACAS 2023, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2023, Paris, France, April 22-27, 2023, Proceedings, Part II
复制标题
系统构建和分析的工具和算法 - 第 29 届国际会议，TACAS 2023，作为欧洲软件理论与实践联合会议的一部分举行，ETAPS 2023，法国巴黎，2023 年 4 月 22-27 日，会议记录，部分
DOI：
10.1007/978-3-031-30820-8_33
复制
发表时间：
2023
期刊：
影响因子：
--
通讯作者：
Aljaafari F
中科院分区：
文献类型：
--
作者：
Aljaafari F
至少在理论上，将不同的验证和测试技术结合在一起可以比单独使用每种技术获得更好的结果。这样做的挑战是如何利用每种技术的优点，同时弥补其弱点。EBF4.2 通过创建有界模型检查器和灰盒模糊器的集成来解决并发漏洞的这一挑战。与简单地并行运行所有可能的技术的投资组合相比，EBF 力求在它们之间获得更紧密的合作。这一目标是通过黑匣子方式实现的。一方面，模型检查器被迫通过在被测程序中注入额外的漏洞来向模糊器提供种子。另一方面，现成的模糊器被迫通过添加轻量级仪器并系统地重新播种来探索不同的交错。
Combining different verification and testing techniques together could, at least in theory, achieve better results than each individual one on its own. The challenge in doing so is how to take advantage of the strengths of each technique while compensating for their weaknesses.EBF4.2 addresses this challenge for concurrency vulnerabilities by creating Ensembles of Bounded model checkers and gray-box Fuzzers. In contrast with portfolios, which simply run all possible techniques in parallel,EBFstrives to obtain closer cooperation between them. This goal is achieved in a black-box fashion. On the one hand, the model checkers are forced to provide seeds to the fuzzers by injecting additional vulnerabilities in the program under test. On the other hand, off-the-shelf fuzzers are forced to explore different interleavings by adding lightweight instrumentation and systematically re-seeding them.