Concolic Enumeration of Logic Errors with Substructural Type Evaluation
CELESTE allows for efficient exploration of program state and synthesizes concrete input to reach a given state.
CELESTE's main technique is using "retroanalysis" (from retrograde analysis, a popular form of Chess puzzles). Retroanalysis allows us to model state in an easily-combineable way, and lets us efficiently explore vastly more state space than using traditional symbolic execution methods. Retroanalysis will provide a path from point A to point B in a program.
Retroanalysis can be used to discover other bug classes, and can be used as a basis for automatic exploit generation. However, implementation is not straightforward.
CELESTE is very much a prototype, and primarily is meant to show complex state spaces being handled that conventional binary symbolic execution engines cannot handle. Since this was our goal, CELESTE is not generally usable for generic binaries.
Future work required includes better platform support, symbolic operating system facilities (files, networking), better function and library and symbol support, and better Satisfiability Modulo Theories (SMT) usage to improve usability.
Building is only supported on Linux and currently only supports analyzing highly constrained Linux ELF binaries.
It can be built by running the build.sh script in the top level directory. The build script will install needed dependencies. CELESTE requires Go, yices2 (an SMT solver) and Ghidra SLA files. The needed SLA files are included in this repository.
bash build.sh
If you want to learn more about the build process, read build.md.
The build will output a binary named cel. Once you have that, you're ready to go!
Run CELESTE like this:
./cel -v -d ./your/binary
This will spawn a readline shell. Type help or ? for help.
Try one of the test binaries by running:
$ ./cel ./tests/D01_pickmem_loops
cel>
The abridged source code for this binary looks like:
int main(int argc, char** argv) {
# Start of main is 0x101195
char* a = argv[1];
int i = a[0];
char vals[8] = {0x41, 0x42, 0x43, 0x44, 0x45, 0x46, 0x47, 0x48};
char mem[30] = {i};
// Input gets to choose the arrangement of its input
for (int j = 0; j < i; j++) {
if (a[j] < 0x40 || a[j] > 0x52) {
break;
}
mem[a[j]-0x40] = a[j+1] % 0x7f;
}
if (a[1] == vals[0] && a[2] == mem[3] && a[4] == 'w' && a[3] != 0x21) {
puts("SOLVED"); # Solved is 0x10138c
}
}
The corresponding abridged disassembly looks like this:
0000000000001195 <main>:
// start of function is our starting point
1195: 55 push rbp
1196: 48 89 e5 mov rbp,rsp
1199: 48 83 ec 60 sub rsp,0x60
// main functionality elided
1380: 75 0f jne 1391 <main+0x1fc>
1382: 48 8d 05 81 0c 00 00 lea rax,[rip+0xc81] # 200a <_fini+0xc5e>
1389: 48 89 c7 mov rdi,rax
// this is the puts that we are looking for
138c: e8 8f fc ff ff call 1020 <puts@plt>
// cleanup elided
13ab: c3 ret
It's tough for symbolic execution engines to solve because it has a conditional inside of a loop, and uses symbolic memory indexing.
Once at the celeste prompt, you can type commands to set your start and end points, find a path between the points, then print the satisfying argv.
cel> path find 0x101195 0x10138c
cel> path explore
cel> mem args
0x7021735177305a44725141534b43525246484f464f414a420000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000
CELESTE in the above example has output the argv required to reach the specified address in the code. Here is the binary running on a musl libc system showing that the input is valid:
./tests/D01_pickmem_loops `echo 7021735177305a44725141534b43525246484f464f414a42 | xxd -r -p`
SOLVED
You can see more test files in the tests/ directory. Please consult the README there for a description of available samples.