diff options
Diffstat (limited to 'docs')
| -rw-r--r-- | docs/syz_verifier.md | 105 |
1 files changed, 65 insertions, 40 deletions
diff --git a/docs/syz_verifier.md b/docs/syz_verifier.md index 7443b8ceb..31985c400 100644 --- a/docs/syz_verifier.md +++ b/docs/syz_verifier.md @@ -1,68 +1,90 @@ # syz-verifier -Testing and fuzzing aim to verify a subset of the behaviours of running programs: any logical error can cause -bugs that make the program behave incorrectly, possibly producing unintended output. Many bugs, however, do -not cause the program to crash nor produce assertion failures. - -The behaviour of a program can be classified as either defined or undefined. Undefined behaviour can easily be detected by either static (e.g. compiler warnings) or dynamic analysis (e.g. sanitizers). However, logical errors that result in defined program behaviour, yet are still causing -bugs that make the program behave incorrectly (according to some documented or otherwise expected intent), -are much harder to detect. One way to detect such bugs is setting up test cases that compare program outputs -against a set of expected results (e.g. by manually creating integration or unit tests). - -Differential fuzzing automates this process by providing the same input to different implementations and then -cross-comparing the resulting behaviour to determine whether it is identical. Here it is assumed that one of the implementations is a correct reference implementation. -For example, such a reference implementation could be an identically behaving model, but otherwise very different implementation; but it could also be an older, assumed correct version of the same implementation. - - -`syz-verifier` is a differential fuzzing tool that cross-compares the execution of programs, -generated using `syzlang`, on different versions of the Linux kernel. +Many bugs are easy to detect: they might cause assertions failures, crash our +system, or cause other forms of undefined behaviour detectable by various +dynamic analysis tools. However, certain classes of bugs, referred to as +*semantic bugs*, cause none of these while still resulting in a misbehaving +faulty system. + +To find semantic bugs, one needs to establish a specification of the system's +*intended behaviour*. Depending on the complexity of the system, creating and +centralising such specifications can be difficult. For example, the +"specification" of the Linux kernel is not found in one place, but is rather a +collection of documentation, man pages, and the implied expectations of a vast +collection of user space programs. As such, detecting semantic bugs in the +Linux kernel is significantly harder than other classes of bugs. Indeed, many +test suites are meant to detect regressions, but creating and maintaining test +cases, as well as covering new features requires significant amounts of +engineering effort. + +*Differential fuzzing* is a way to automate detection of semantic bugs by +providing the same input to different implementations of the same systems and +then cross-comparing the resulting behaviour to determine whether it is +identical. In case the systems disagree, at least one of them is assumed to be +wrong. + +`syz-verifier` is a differential fuzzing tool that cross-compares the execution +of programs on different versions of the Linux kernel to detect semantic bugs. The architecture of `syz-verifier` is shown in the following diagram.  -The `syz-verifier` process starts and manages VM instances with the kernels to be cross-compared. It also starts the `syz-runner` process on the VMs. Communication between the host and the guest is done via RPCs. - -`syz-verifier` generates and sends a continuous stream of programs to `syz-runner` via RPCs while -`syz-runner` is responsible for starting `syz-executor` processes and turning the program into input for -those. `syz-executor` processes the input, which triggers a sequence of syscalls in the kernel. Then, -`syz-runner` collects the results and sends them back to the host. - - At the moment, the results contain the errnos returned by each system call. When `syz-verifier` has received results from all the kernels for a specific program, it verifies them to - ensure they are identical. If a mismatch is found, the program is rerun on all the kernels to ensure the - mismatch is not flaky (i.e. it didn't occur because of some background activity or external state). If the - mismatch occurs in all reruns, `syz-verifier` creates a report for the program and write it to persistent - storage. +The `syz-verifier` process starts and manages VM instances with the kernels to +be cross-compared. It also starts the `syz-runner` process on the VMs. +Communication between the host and the guest is done via RPCs. + +`syz-verifier` generates and sends a continuous stream of programs to +`syz-runner` via RPCs while `syz-runner` is responsible for starting +`syz-executor` processes and turning the program into input for those. +`syz-executor` processes the input, which triggers a sequence of syscalls in +the kernel. Then, `syz-runner` collects the results and sends them back to the +host. + +At the moment, the results contain the errnos returned by each system call. +When `syz-verifier` has received results from all the kernels for a specific +program, it verifies them to ensure they are identical. If a mismatch is found, +the program is rerun on all the kernels to ensure the mismatch is not flaky +(i.e. it didn't occur because of some background activity or external state). +If the mismatch occurs in all reruns, `syz-verifier` creates a report for the +program and write it to persistent storage. # How to use `syz-verifier` -After cloning the repository (see how [here](/docs/linux/setup.md#go-and-syzkaller)), build the tool as: +After cloning the repository (see how +[here](/docs/linux/setup.md#go-and-syzkaller)), build the tool as: ``` make verifier runner executor ``` -To start using the tool, separate configuration files need to be created for each kernel you want to include -in the verification. An example of Linux configs can be found [here](/docs/linux/ -setup_ubuntu-host_qemu-vm_x86-64-kernel.md#syzkaller). The configuration files are identical to those used by `syz-manager`. +To start using the tool, separate configuration files need to be created for +each kernel you want to include in the verification. An example of Linux +configs can be found [here](/docs/linux/ +setup_ubuntu-host_qemu-vm_x86-64-kernel.md#syzkaller). The configuration files +are identical to those used by `syz-manager`. -If you want to generate programs from a specific set of system calls, these can be listed in the kernel -config files using the `enable_syscalls` option. If you want to disable some system calls, use the `disable_syscalls` option. +If you want to generate programs from a specific set of system calls, these can +be listed in the kernel config files using the `enable_syscalls` option. If you +want to disable some system calls, use the `disable_syscalls` option. Start `syz-verifier` as: ``` ./bin/syz-verifier -configs=kernel0.cfg,kernel1.cfg ``` -`syz-verifier` will also gather statistics throughout execution. They will be printed to `stdout` by default, but an alternative file can be specified using the `stat` flag. +`syz-verifier` will also gather statistics throughout execution. They will be +printed to `stdout` by default, but an alternative file can be specified using +the `stat` flag. # How to interpret the results Results can be found in `workdir/results`. -When `syz-verifier` finds a mismatch in a program, it will create a report for that program. The report lists -the results returned for each system call, by each of the cross-compared kernels, highlighting the ones were -a mismatch was found. The system calls are listed in the order they appear in the program. +When `syz-verifier` finds a mismatch in a program, it will create a report for +that program. The report lists the results returned for each system call, by +each of the cross-compared kernels, highlighting the ones were a mismatch was +found. The system calls are listed in the order they appear in the program. An extract of such a report is shown below: @@ -83,9 +105,12 @@ ERRNO mismatches found for program: ... ``` -The order of the results is given by the order in which configuration files were passed so `Pool: 0 ` reports results for the kernel created using `kernel0.cfg` and so on. +The order of the results is given by the order in which configuration files +were passed so `Pool: 0 ` reports results for the kernel created using +`kernel0.cfg` and so on. -The [Flags](/pkg/ipc/ipc.go#L82) can be used to determine the state reached by the system call: +The [Flags](/pkg/ipc/ipc.go#L82) can be used to determine the state reached by +the system call: * `0` = syscall not even started * `1` = syscall started * `3` = syscall finished executing |