See the following dumb crackme.

$ cat crackme.c

#include <stdio.h>
#include <sys/types.h>
#include <stdlib.h>
#include <fcntl.h>

char *serial = "\x30\x39\x3c\x21\x30";

int main(void)
{
  int fd, i = 0;
  char buf[260] = {0};
  char *r = buf;

  fd = open("serial.txt", O_RDONLY);
  read(fd, r, 256);
  close(fd);
  while (i < 5){
    if ((*r ^ 0x55) != *serial)
      return 0;
    r++, serial++, i++;
  }
  if (!*r)
    printf("Good boy\n");
  return 0;
}

$ cat serial.txt
ABCD

$ ../../../pin -t ./obj-intel64/ConcolicExecution.so -taint-file serial.txt -- ./crackme
[TAINT]                     bytes tainted from 0x7fff81674900 to 0x7fff81674a00 (via read)
[READ in 7fff81674900]      400698: movzx eax, byte ptr [rax]
[Constraint]                #0 = 0x41
                            eax is now tainted
[SPREAD]                    40069b: mov edx, eax
                            output: edx | input: eax
                            edx is now tainted
[FOLLOW]                    40069b: mov edx, eax
[Constraint]                #1 = #0
[FOLLOW]                    4195997: xor edx, 0x55
[Constraint]                #2 = xor(#1, 0x55)
[READ in 4007ec]            4006a7: movzx eax, byte ptr [rax]
                            eax is now freed
[FOLLOW]                    4006aa: cmp dl, al
[Equation]                  cmp(#2, 0x30)
[Equation]                  cmp(xor(0x41, 0x55), 0x30)
[SPREAD]                    7f0fef6ab7db: mov edx, 0x1
                            output: edx | input: constant
                            edx is now freed


-------------------


As you can see above, this Pin tool lists all constraints to prepare the
concolic execution ! The constraints are :

    [Constraint]                #0 = 0x41
    [Constraint]                #1 = #0
    [Constraint]                #2 = xor(#1, 0x55)
    [Equation]                  cmp(#2, 0x30)

And the full equation is :

    [Equation]                  cmp(xor(0x41, 0x55), 0x30)

Now we just need to use a theorem solver and re-run the analysis (Concolic
execution) to solve automaticaly this crackme.





-- Ref: https://twitter.com/JonathanSalwan/status/370915077093720064
-- Same project with Valgrind: https://twitter.com/JonathanSalwan/status/343990540699844609