DARPA Cyber Grand Challenge

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).

Note

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.

Setting up the S2E environment

The first step is to setup the environment. This can be done automatically using the s2e-env tool. Follow these instructions to create your S2E environment and build S2E.

Creating a CGC image

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-9.2.1-i386

Analyzing a sample CB

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.

Creating a project

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-9.2.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.

s2e-config.lua

There are a number of CGC-specific plugins enabled in s2e-config.lua. These are:

CGCInterface
Coordinates all the CGC plugins.
DecreeMonitor
Plugin that tracks various system events (e.g. segmentation fault, process creation, etc.) in the DECREE OS.
ExploitGenerator
Plugin that combines the information from the Recipe and POVGenerator plugins to generate an actual exploit.
POVGenerator
Plugin for generating POVs using the standard defined by DARPA.
Recipe
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:

SeedSearcher

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.

The SeedSearcher plugin fetches seed files to concolically guide execution in the target program. Seed files are placed in the seeds directory. During analysis, the SeedSearcher plugins 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:

<index>-<priority>.<extension>

The index specifies the order of the seed. SeedSearcher fetches seed files by increasing index number. Higher priorities are specified with higher integer. In a given batch of seeds, SeedSearcher will 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 SeedSearcher will automatically load balance available seeds across all available cores. For example, if there are 40 cores available, SeedSearcher will attempt to run 40 seeds in parallel.

The SeedSearcher plugin 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 SeedSearcher plugin.

The bootstrap script

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 documentation.

The CGC 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.

Starting an analysis

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 .xml or .c file extensions. Once some POV files have been generated you can press q to stop S2E.

../../../_images/cadet_00001_tui.png

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 Ctrl+C or 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 s2e-last.

Replaying POVs

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.

  1. Follow the instructions here to setup and run the CGC testing VM
  2. As discussed in the instructions in the previous step, files can be shared between the host and CGC testing VM via the /vagrant directory. 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.
  3. Run vagrant ssh to access the VM and copy the files from /vagrant into /home/vagrant. Then run the test_pov.sh script to check your POV’s correctness.