Abstract
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. EBF 4.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, EBF strives 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.
challenge in doing so is how to take advantage of the strengths of each technique while compensating for their weaknesses. EBF 4.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, EBF strives 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.
| Original language | English |
|---|---|
| Title of host publication | 29th International Conference on Tools and Algorithms for the Construction and Analysis of Systems |
| Publication status | Accepted/In press - 11 Feb 2023 |