Skip to content(if available)orjump to list(if available)

Compiler Fuzzing in Continuous Integration: A Case Study on Dafny [pdf]

Compiler Fuzzing in Continuous Integration: A Case Study on Dafny [pdf]

2 comments

·January 21, 2025
Visit

matt_d

Abstract:

"We present the design of CompFuzzCI, a framework for incorporating compiler fuzzing into the continuous integration (CI) workflow of the compiler for Dafny, an open-source programming language that is increasingly used in and contributed to by industry. CompFuzzCI explores the idea of running a brief fuzzing campaign as part of the CI workflow of each pull request to a compiler project. Making this effective involved devising solutions for various challenges, including how to deduplicate bugs, how to bisect the project’s revision history to find the commit responsible for a regression (challenging when project interfaces change over time), and how to ensure that fuzz testing complements existing regression testing efforts. We explain how we have engaged with the Dafny development team at Amazon to approach these and other problems in the design of CompFuzzCI, and the lessons learned in the process. As a by-product of our work with CompFuzzCI, we found and reported three previously-unknown bugs in the Dafny compiler. We also present a controlled experiment simulating the use of CompFuzzCI over time on a range of Dafny commits, to assess its ability to find historic bugs. CompFuzzCI prioritises support for the Dafny compiler and the fuzz-d fuzzer but has a generalisable design: with modest modification to its internal interfaces, it could be adapted to work with other fuzzers, and the lessons learned from our experience will be relevant to teams considering including fuzzing in the CI of other industrial software projects."

https://github.com/CompFuzzCI

madarcho

A pleasant surprise seeing an Alastair Donaldson supported paper. What I liked most at Imperial was the amount of professors pushing for things that sat between the fully theoretical world, and the more real engineering world. From a first quick skim this paper seems to hit that right on the head. I've been wanting to see how I could introduce more of the fun of formal verification into my job, so I'll be digging deep into this one for some inspiration.