borzacchiello

Using KLEE on the DARPA CGC challenge binaries (as ported to Linux/OS X by Trail of Bits) is currently not a fun time. Here are a few of the current obstacles.

I'm working off of KLEE master, built against LLVM 3.4, running on Linux (Ubuntu 16.04). Some of this may be easier or harder on other platforms supported by cb-multios (i.e. OS X and maybe someday Windows).

KLEE wants a standard int main(int argc, char *argv[]). Most of the challenges instead have int main(void) instead, and some, perversely, use the first int argument to main to hold the address of the flag page. (Edit: this has been fixed in the windows_support branch of cb-multios and should make its way into master soon)
The challenge binaries use lots of symbols that conflict with things in libc. For example, many of them define the symbol stdin and then implement a FILE* struct themselves. So when trying to link in klee-uclibc.bc you get symbol clashes. This already has an [

	#!/bin/sh

	set -eu

	create_iconset() {
	mkdir -p Ghidra.iconset
	cat << EOF > Ghidra.iconset/Contents.json
	{
	"images":
	[