During the evaluation of Kirenenko, we have collected a relatively large set of path constraints that might be useful for tasks like test or benchmarking path constraint solvers like traditional SMT solvers (e.g., Z3, CVC4, Yices) and fuzzing-based solvers (e.g., JFS, fuzzolic). The main difference from other path constraint dataset is that we’ve also recorded concrete values of inputs bytes, which can be useful for solving nested branch constraints as the current input already satisfies the all previous path constraints so searching from current input could be easier to find a new input that can flip the last branch.

The constraints are collected from 14 programs. We first used AFL to fuzz them for over 24 hours, then use Kirenenko to collect the path constraints. We applied a lightweight filter (calling context + branch address) to reduce the number of potential duplicated constraints. Collected constraints are then serialized using protobuf. Constraints from nested branches are also included (as pointers to previous records).

The list of programs are:

  • dtls
  • file
  • libjpeg
  • libxml2
  • nm (binutils)
  • objdump (binutils)
  • openssl
  • readelf (binutils)
  • readpng (libpng)
  • size (binutils)
  • sqlite3
  • tcpdump (libpcap)
  • tiff2pdf (libtiff)
  • vorbis

You can download the archives here. My student has also prepared an example on how to load the constraints and feed to Z3, which can be find here.

Have fun!

Update: I haven’t fully enabled collecting floating pointer and string constraints in Kireneko yet (in slow progress), so all constraints are QF_BV now.