Please check this doc first before you proceed.
Race condition can be tricky to be dealt with if they are hard to trigger, especially when running in S2E where only one CPU core is used. What's worse, Syzkaller has limited support for producing reliable PoC in C, and thus in this case more human intervention is required.
It seems that for different machines, the likehood of triggering CVE-2017-7533 with S2E varies siginificantly. To increase the race window, one common trick can be used as follows. From the description, we learn that the race happens in two functions inotify_handle_event and vfs_rename, and thus we could simply add a function call printk at this line. To the end, we need to modify and recompile the kernel and then create a new image for S2E, which can be done by following this doc to build a kernel of version 4.9.3.
Since this PoC is not come from syzbot, we do not have a syzbot testcase convenient for automated annotation. Instead, we have to annotate the PoC directly. Apart from adding s2e_invoke_plugin("ProgramMonitor", "s", 1) and s2e_invoke_plugin("ProgramMonitor", "e", 1); to indicating the start/end of the PoC, we need to use s2e_make_symbolic to make some arguments symbolic. Particularly for race condition in which multiple loops running inside different threads, we can mark the start of the each iteraction with s2e_invoke_plugin("ProgramMonitor", "m", 1).
Check file poc.c for final output.
sh make.sh
s2e new_project -n inotify -i debian-9.2.1-x86_64-4.9.3 -f poc
cd aeg-analysis
python main.py pahole -i ../s2e/source/s2e/s2e-linux-kernel/linux-4.9.3/vmlinux --known
python main.py genconf -p inotify -i ../s2e/source/s2e/s2e-linux-kernel/linux-4.9.3/vmlinux -e -m 1
cd ${S2EDIR}/projects/inotify && ./launch-s2e.sh
Note that race may never succeed, you may need to force it to terminate and re-run.
python main.py genconf -p inotify -i ../s2e/source/s2e/s2e-linux-kernel/linux-4.9.3/vmlinux -e -m 2 -r 200
cd ${S2EDIR}/projects/inotify && ./launch-s2e.sh
Note that we add an extra option -r 200 to indicate that it is a race condition bug. With this, we disable our symbolic expression assisted OOB dection scheme and fall back to default KASAN (that may give incorrect results). However, it is a trade off between performance and correctiveness as race condition typically requires to run the same sequence of syscalls hundreds of times. The extra parameter 200 will be explained later.
python main.py genconf -p inotify -i ../s2e/source/s2e/s2e-linux-kernel/linux-4.9.3/vmlinux -e -m 3 -r 200
cd ${S2EDIR}/projects/inotify && ./launch-s2e.sh
Note that we add an extra option -r 200 to denote that race could occur at most 200 times. Without it, the program may run too long until the race succeed, resulting in prohibitive performance overhead. If the race failed after 200 iterations, we could simply re-run it.
Since syzkaller does not support producing C code for race condition very well and we do not have PoC in Syzkaller's format, we have to manully adapt the PoC based on the solutions generated by invoking the following command: python main.py parselog -p inotify --solution. You can find ans_ip_mc_socklist_next_rcu.json on ${S2EDIR}/projects/inotify, which consists of the concrete input for those arguments we make symbolic in the PoC. Moreover, it tells what's the critical field (i.e., target) it allows to overwrite (check candidates.lua under the same directory for more information about the object). For this particular case, it can temper a data pointer to 0xffff800076801040 (check the pointer field) which resides in physmap.
Of course, it is not enough to only adjust the syscalls' arguments. You also have to incorporate with heap feng shui to manipulate the heap layout and exploit the target object (i.e., ip_mc_socklist) in which a data pointer we could modify points to another struct containing a function pointer.