DARPA’s Cyber Grand Challenge (CGC) was the world’s first all-machine hacking tournament. S2E was a key component in CodeJitsu’s Cyber Reasoning System (CRS) and was used to automatically to find vulnerabilities and exploit them. This demo walks you through the process of using S2E to find and generate a “proof of vulnerability” (POV - i.e. an exploit) in a CGC challenge binary (CB).
You may want to refer to the tutorial on Automated Generation of Proofs of Vulnerability with S2E in order to understand what S2E does behind the scenes in order to generate PoVs.
The first step is to setup the environment. This can be done automatically using the
Follow these instructions to create your S2E environment and build S2E.
The CGC Final Event (CFE) ran on the DECREE operating system. DECREE is a modified Linux OS with a reduced number of system calls. In addition to this, the DECREE OS has been modified to add “hook points” for S2E (e.g. to signal process creation, termination, etc.) and to allow S2E to inject symbolic values. The source code for the DECREE OS is available at https://github.com/S2E/s2e-linux-kernel. A DECREE virtual machine image can be built by running the following command:
s2e image_build cgc_debian-8.7.1-i386
Once we have an image we can start analyzing CBs. Sample CBs are available here and can be built using the instructions here . The remainder of this tutorial will focus on the CADET_00001 program (which is available here), but the ideas and techniques should be applicable to all of the CBs.
Once you have built the CADET_00001 binary you can create an S2E analysis project using
s2e-env. To do so, run:
s2e new_project --image cgc_debian-8.7.1-i386 ./source/s2e/decree/samples/CADET_00001
This will create a
projects/CADET_00001 directory with various scripts and configuration files needed by S2E, as
described here. Lets examine some of the generated files.
There are a number of CGC-specific plugins enabled in
s2e-config.lua. These are:
- Coordinates all the CGC plugins.
- Plugin that tracks various system events (e.g. segmentation fault, process creation, etc.) in the DECREE OS.
- Plugin that combines the information from the
POVGeneratorplugins to generate an actual exploit.
- Plugin for generating POVs using the standard defined by DARPA.
- Used for defining the conditions necessary for exploit generation. S2E supports Type 1 and Type 2 POVs. POV generation will not work without recipes.
Other plugins that are required for CB analysis but are not specific to the CGC include:
Seed files (or test inputs) are concrete inputs for the program under analysis. These files can be anything that the program accepts (PNG files, documents, etc.). They can be obtained from a fuzzer, generated by hand, etc. For CGC, seeds are binary executables compiled from XML of C PoV format.
SeedSearcherplugin fetches seed files to concolically guide execution in the target program. Seed files are placed in the seeds directory. During analysis, the
SeedSearcherplugins polls the seeds directory for new seeds.When it finds new seeds, the plugin forks a new state that fetches the new seed and then runs the binary using that seed as input.
Seed files can have different priorities. For example, if a fuzzer finds a seed that crashes the program, S2E may want to use that seed before others that, e.g., only cover new basic blocks. The priority of a seed is specified in its name. Seed files use the following naming convention:
The index specifies the order of the seed.
SeedSearcherfetches seed files by increasing index number. Higher priorities are specified with higher integer. In a given batch of seeds,
SeedSearcherwill schedule those with the highest priority first.
When there are many seed files, it is advantageous to run S2E on multiple cores. In this mode, the
SeedSearcherwill automatically load balance available seeds across all available cores. For example, if there are 40 cores available,
SeedSearcherwill attempt to run 40 seeds in parallel.
SeedSearcherplugin works in conjunction with the guest bootstrap file. The bootstrap file is built in such a way that state 0 runs in an infinite loop and forks a new state when a new seed is available. If there are no seed files, the bootstrap forks a state in which the program is run without seeds.
- CUPA Searcher
- This searcher implements the Class Uniform Path Analysis (CUPA) algorithm as described in this paper. It can work together with the
The bootstrap script is a file called
bootstrap.sh that the guest fetches from the host and executes. It contains
instructions on how to execute the program under analysis. More detail can be found in the s2e-env
bootstrap.sh script slightly differs from Linux bootstraps. One key difference is that seeds will always be
enabled for CGC projects, so the
while loop in the
execute function will exist even if you do not intend to use
seed files. Note that it will not affect symbolic execution - the
SeedSearcher (described above) will simply never
schedule this state (state 0) for execution. This state will always exist, which means that even if S2E explores all
execution paths in the CB (which is possible for simple binaries such as CADET_00001), the analysis will not end
because not all states have been killed. The analysis must therefore be manually stopped.
To start S2E, run the following command:
s2e run CADET_00001
This will display a TUI-based dashboard, similar to that used by the American Fuzzy Lop (AFL) fuzzer. As S2E finds
vulnerabilities, it generates POV files in the
s2e-last directory. These files have either
file extensions. Once some POV files have been generated you can press
q to stop S2E.
Alternatively, you can run S2E without the TUI by using the
-n option in
s2e run. Instead of the TUI you will
see the standard S2E output. Once some POVs have been generated you can stop S2E by killing the process with
killall -9 qemu-system-i386.
For a deeper understanding of what S2E is doing you may wish to have a look at the
debug.txt log file in
POVs are an XML description of an exploit (for more detail, see here). They can be compiled to C code and then to an executable format to test that the exploit is correct.
- Follow the instructions here to setup and run the CGC testing VM
- As discussed in the instructions in the previous step, files can be shared between the host and CGC testing VM via
/vagrantdirectory. Copy the CADET_00001 binary, the POV XML files generated by S2E and this script (located in your S2E environment in
bin/cgc-tools/test_pov.sh) to the CGC testing VM.
vagrant sshto access the VM and copy the files from
/home/vagrant. Then run the
test_pov.shscript to check your POV’s correctness.