The goal would be to create a a benchmark suite based on real-world vulnerabilities. Initially, I though we should focus on race condition benchmarks, these are all fairly complicated. There are enough CVE entries that mention races, so it may be a good place to start.
CVE-2019-19537 (fix) drivers/usb/core/file.c --- We are able to detect this. The race is more conceptual than accessing the same memory location, but the type-based data race exposes it.
Maybe
CVE-2009-4895 (fix) drivers/char/tty_io.c --- has a nice , but needs Linux 2.6 headers. Running goblint on more recent versions of drivers/tty/tty_io.c gives 62 unsafe warnings.
CVE-2021-32399 (fix) net/bluetooth/hci_request.c --- This moves operations within a critical section, but this is a newer kernel version than we can analyze. Older versions of this file are significantly different.
Not based on locks
CVE-2019-11815 (fix) net/rds/tcp.c --- seems based on intricate logic.
CVE-2019-11599 (fix) mm/mmap.c and others --- adds extra checks; synchronization is not added yet.
CVE-2018-12633 (fix) drivers/virt/vboxguest/vboxguest_linux.c --- This is a double fetch race when data is moved from user space to kernel space and can be changed in-between the fetches.
The goal would be to create a a benchmark suite based on real-world vulnerabilities. Initially, I though we should focus on race condition benchmarks, these are all fairly complicated. There are enough CVE entries that mention races, so it may be a good place to start.
Included
Maybe
Not based on locks