Palindrome Progress


Palindrome Progress

I usually keep my updates down to one a week, but I thought I’d share a little earlier.

Right now I’m working on solving the Palindrome challenge (the infamous CADET_00001) from the Cyber Grand Challenge with Falcon, my Binary Analysis Framework. The Trail of Bits team has been kind enough to provide these binaries for Linux (and other OSs) in their cb-multios repository.

If you’re not familiar with the Palindrome challenge, it’s a classic buffer overflow, with an easier-to-reach, “Easter Egg.” The binary reads up to 128-bytes into a 64-byte stack buffer using a function, “receive_delim,” which will receive bytes up to the first newline. It then verifies that a palindrome exists. After this, it will check whether the first character is ^, and if it is you have reached an, “Easter Egg,” condition. As of now, I can reach the Easter Egg condition, but I will need more work, most likely state-merging (read Veritesting), to get around state explosion and progess to the buffer overflow.

A snippet from the rust code I’m using interact with Symbolic Executors over Palindrome with Falcon follows. I’ve left it in raw, uncleaned form:

        for driver in drivers {
            if let Some(address) = driver.address() {
                if address == 0x804880d {
                    println!("0x804880d - Resting read loop");
                    for constraint in driver.engine().constraints() {
                        println!("\t{}", constraint);
                if address == 0x8048869 {
                    println!("Driver at 0x8048869 return from check");
                if address == 0x8048944 {
                    let eax = driver.engine().get_scalar("eax").unwrap();
                    let eax = driver.engine().eval(eax, None)?.unwrap();
                    if eax.value() < 0x10 || eax.value() > 0x200 {
                    println!("0x8048944 eax={}", eax);
                if address == 0x80489a8 {
                    println!("0x80489a8 easteregg");
                    for scalar in driver.platform().symbolic_scalars() {
                        let byte = driver.engine().eval(&scalar.clone().into(), None)?.unwrap();
                        assert!(byte.bits() == 8);
                        println!("{} 0x{:x}",, byte.value());
                    bail!("easteregg found");
                if address == 0x80489ce {
                    let esp = driver.engine().get_scalar("esp").unwrap();
                    println!("0x80489ce esp={}", esp);

        drivers = step_drivers.into_par_iter()
                              .map(|d| d.step().unwrap())
                              .reduce(|| Vec::new(), |mut v, mut d| { v.append(&mut d); v });

I’ve done some constraining here to terminate states that return after the check function, and to ignore everything if we read less than 16 bytes. The resulting output looks like this:

0x8048944 eax=0x12:32
TRACE - SYS_READ 0x0:32 0xAFFFEEE6:32 0x1:32
0x8048944 eax=0x10:32
0x8048944 eax=0x11:32
0x80489a8 easteregg
fd_0_0 0x5e
fd_0_1 0x1
fd_0_2 0x1
fd_0_3 0x1
fd_0_4 0x1
fd_0_5 0x1
fd_0_6 0x1
fd_0_7 0x1
fd_0_8 0x1
fd_0_9 0x1
fd_0_10 0x1
fd_0_11 0x1
fd_0_12 0x1
fd_0_13 0x1
fd_0_14 0x1
fd_0_15 0x5e
fd_0_16 0xa
error: easteregg found

real    0m27.766s
user    0m14.612s
sys     0m27.576s

I’m not sure if I’m happy with those execution times, but so far pretty neat.