Cqual++ Quick-Start

On this page we show you how to use Oink/Cqual++ to find printf format string bugs in your code as soon as possible. You can do other things with Oink as well, but we want to show you the end-to-end process of doing one useful thing right away. Some of this information is redundant with that of the main Oink page; I repeat it so these instructions would be self-contained. You need to do the following.

Get Oink

Get the latest release from the github repository per the instructions on the main page.

Configure and Build Oink

To build everything, in oink-stack/ type:

./configure && make clean all check

Upon successful build, you should see

DONE in all directories: check

If you have problems with the platform-model tests failing with a segmentation fault, this seems to often be due to problems with libzipios++ and zlib. Make sure that your version of these libraries was built with the same version of the compiler that you are building Oink with. Another solution is to just turn off zip archiving, falling back to a more primitive method. Do this from the oink-stack directory as follows.

./configure +platform-model:--archive-srz=dir +oink:-require-no-archive-srz-zip

Intercept your .i files

Oink works on files that have been through the preprocessor, usually known as .i files. You have to get these files from the build process of your project somehow. If your project has a simple build process and uses gcc, you can do this by just adding -save-temps to the compile flags, which we will use here. For industrial-strength build process interception of any build process using gcc you may want to use build-interceptor.

For demonstration purposes I have written a really simple example project in oink-stack/oink/Test/Quickstart1/. All of the changes to the makefile needed to produce the .i files amount to these as follows.

    TOCLEAN += *.i *.s
    CFLAGS += -save-temps

Here it the build process in action.

    cd /home/dsw/oink-stack/oink/Test/Quickstart1/
    make clean all check
    rm -f  *.i *.s *.o hello
    cc -save-temps -c -o main.o main.c
    cc -save-temps -c -o g.o g.c
    cc -o hello main.o g.o
    HELLO='good data' ./hello
    Hello, World!  The important data is good data
    HELLO='evil data' ./hello
    Hello, World!  The important data is evil data

Run Cqual++

We now want to run Oink/Cqual++, oink-stack/oink/qual, on the .i files. In general, to learn more about what Oink/Cqual++ it can do, see the Cqual++ documentation; for more on its command line flags, type oink-stack/oink/qual --help.

To illustrate how to get started, I have added to the oink-stack/oink/Test/Quickstart1/Makefile a section just to do this for you.

    OINK_STACK := ../../..
    LATTICE := $(OINK_STACK)/libqual/config/lattice
    .PHONY: analyze
    analyze: all
    	$(OINK_STACK)/oink/qual -q-config $(LATTICE) main.i g.i mini_libc.c

Here it is in action.

    make analyze
    ../../../oink/qual -q-config ../../../libqual/config/lattice main.i g.i mini_libc.c

(skipping warnings about assembly language not being analyzed.)

    Reporting 2 of 16 errors (including anonymous)
    /usr/include/stdio.h:277 WARNING (1 of 2):  const t2335-char treated as $tainted and $untainted

     const t2335-char: $tainted $untainted 
    mini_libc.c:3:15: $tainted <= getenv_ret'
    mini_libc.c:3:15: <= getenv_ret'
    main.c:13:16: <=  ( (getenv) ( ("HELLO")))'
    main.c:13:3: <= data''
    main.c:14:8: <=  t5400-char
    main.c:5:6: <=  t5400-char
    main.c:5:6: <= data''
    main.c:7:7: <=  t1637-char
    g.h:5:6: <=  t7032-char
    g.c:4:6: <=  t8452-char
    g.c:4:6: <= data''
    g.c:6:10: <=  const t7730-char
    /usr/include/stdio.h:277:5: <=  const t2335-char
    mini_libc.c:4:5: <=  const t10072-char
    mini_libc.c:4:34: <= $untainted

    main.c:5 WARNING (2 of 2):  t5400-char treated as $tainted and $untainted

(skipping repeated report of error)

    make: *** [analyze] Error 32

As you can see, Cqual++ is showing you a dataflow path from $tainted to $untainted; note that the output format is designed so that in emacs compile mode, C-x backtick should take you from one line to the next. Since $tainted does indeed flow to $untainted, Cqual++ returns error code 32, rather than 0.

Libc model

In order for this analysis to find that $tainted flowed to $untainted, it was necessary for $tainted and $untainted to be annotated in the code somewhere. This particular analysis finds a "format string bug": a vulnerability because data from outside the program is trusted as the first argument of printf(). For this analysis it is natural to annotate the $tainted onto the functions of libc that return data from outside the program and where libc takes data that it must trust. Therefore we provided a mini libc model in the file mini_libc.c that has these annotations. Oink comes with a real model of libc in oink-stack/platform-model. It is hard to make portable and is therefore failure-prone; therefore we make it easier for people to get started with oink by not compiling platform-model by default. You can either use platform-model or write your own annotations as we have done here in mini_libc.c:

    // provide annotations for part of libc; see
    // oink-stack/platform-model/ for the real thing
    char $tainted *getenv(char const *name);
    int printf(char const $untainted *fmt, ...);

Presentation bugs

Please note that we do not normally use Cqual++ manually in the way I am illustrating (we use it wrapped with other tools etc) so in preparing this Quick-Start a few bugs have been revealed to us.

Going further

For lots more, see the main Cqual++ Documentation.