Note: This trace demonstrates how it's possible to solve a dumb crackme via the concolic execution. The crackme checks a serial in a file and prints "Good boy" if the serial is valid. First, I set a serial to "ABCD" and I run the Pin tool which finds and generates the good key. For each run the Pin tool finds only one character, So we need to run the Pin tool until the serial is found. For each step I display the serial.txt to show you that the key is generated at runtime. $ cat crackme1.c #include #include #include #include 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 -- ./crackme1 [TAINT] bytes tainted from 0x7fff2d60e7d0 to 0x7fff2d60e8d0 (via read) [READ in 7fff2d60e7d0] 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(x, 0x55), 0x30) [Z3 Solver]------------------------------------- (solver (= (bvxor x #x00000055) #x00000030)) (define-fun x () (_ BitVec 32) #x00000065) The good value is 0x65 [Z3 Solver]------------------------------------- [SPREAD] 7ff3541837db: mov edx, 0x1 output: edx | input: constant edx is now freed $ cat serial.txt e% $ ../../../pin -t ./obj-intel64/ConcolicExecution.so -taint-file serial.txt -- ./crackme1 [TAINT] bytes tainted from 0x7fff6d1f8730 to 0x7fff6d1f8830 (via read) [READ in 7fff6d1f8730] 400698: movzx eax, byte ptr [rax] [Constraint] #0 = 0x65 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(x, 0x55), 0x30) [Z3 Solver]------------------------------------- (solver (= (bvxor x #x00000055) #x00000030)) (define-fun x () (_ BitVec 32) #x00000065) The good value is 0x65 [Z3 Solver]------------------------------------- [READ in 7fff6d1f8731] 400698: movzx eax, byte ptr [rax] [Constraint] #3 = 0x00 eax is now tainted [FOLLOW] 40069b: mov edx, eax [Constraint] #4 = #3 [FOLLOW] 4195997: xor edx, 0x55 [Constraint] #5 = xor(#4, 0x55) [READ in 4007ed] 4006a7: movzx eax, byte ptr [rax] eax is now freed [FOLLOW] 4006aa: cmp dl, al [Equation] cmp(#5, 0x39) [Equation] cmp(xor(x, 0x55), 0x39) [Z3 Solver]------------------------------------- (solver (= (bvxor x #x00000055) #x00000039)) (define-fun x () (_ BitVec 32) #x0000006c) The good value is 0x6c [Z3 Solver]------------------------------------- [SPREAD] 7fe0b6aa47db: mov edx, 0x1 output: edx | input: constant edx is now freed $ cat serial.txt el% $ ../../../pin -t ./obj-intel64/ConcolicExecution.so -taint-file serial.txt -- ./crackme1 [TAINT] bytes tainted from 0x7fff2d1e1e00 to 0x7fff2d1e1f00 (via read) [READ in 7fff2d1e1e00] 400698: movzx eax, byte ptr [rax] [Constraint] #0 = 0x65 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(x, 0x55), 0x30) [Z3 Solver]------------------------------------- (solver (= (bvxor x #x00000055) #x00000030)) (define-fun x () (_ BitVec 32) #x00000065) The good value is 0x65 [Z3 Solver]------------------------------------- [READ in 7fff2d1e1e01] 400698: movzx eax, byte ptr [rax] [Constraint] #3 = 0x6c eax is now tainted [FOLLOW] 40069b: mov edx, eax [Constraint] #4 = #3 [FOLLOW] 4195997: xor edx, 0x55 [Constraint] #5 = xor(#4, 0x55) [READ in 4007ed] 4006a7: movzx eax, byte ptr [rax] eax is now freed [FOLLOW] 4006aa: cmp dl, al [Equation] cmp(#5, 0x39) [Equation] cmp(xor(x, 0x55), 0x39) [Z3 Solver]------------------------------------- (solver (= (bvxor x #x00000055) #x00000039)) (define-fun x () (_ BitVec 32) #x0000006c) The good value is 0x6c [Z3 Solver]------------------------------------- [READ in 7fff2d1e1e02] 400698: movzx eax, byte ptr [rax] [Constraint] #6 = 0x00 eax is now tainted [FOLLOW] 40069b: mov edx, eax [Constraint] #7 = #6 [FOLLOW] 4195997: xor edx, 0x55 [Constraint] #8 = xor(#7, 0x55) [READ in 4007ee] 4006a7: movzx eax, byte ptr [rax] eax is now freed [FOLLOW] 4006aa: cmp dl, al [Equation] cmp(#8, 0x3c) [Equation] cmp(xor(x, 0x55), 0x3c) [Z3 Solver]------------------------------------- (solver (= (bvxor x #x00000055) #x0000003c)) (define-fun x () (_ BitVec 32) #x00000069) The good value is 0x69 [Z3 Solver]------------------------------------- [SPREAD] 7f7e919ef7db: mov edx, 0x1 output: edx | input: constant edx is now freed $ cat serial.txt eli% $ ../../../pin -t ./obj-intel64/ConcolicExecution.so -taint-file serial.txt -- ./crackme1 [TAINT] bytes tainted from 0x7fff597b37a0 to 0x7fff597b38a0 (via read) [READ in 7fff597b37a0] 400698: movzx eax, byte ptr [rax] [Constraint] #0 = 0x65 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(x, 0x55), 0x30) [Z3 Solver]------------------------------------- (solver (= (bvxor x #x00000055) #x00000030)) (define-fun x () (_ BitVec 32) #x00000065) The good value is 0x65 [Z3 Solver]------------------------------------- [READ in 7fff597b37a1] 400698: movzx eax, byte ptr [rax] [Constraint] #3 = 0x6c eax is now tainted [FOLLOW] 40069b: mov edx, eax [Constraint] #4 = #3 [FOLLOW] 4195997: xor edx, 0x55 [Constraint] #5 = xor(#4, 0x55) [READ in 4007ed] 4006a7: movzx eax, byte ptr [rax] eax is now freed [FOLLOW] 4006aa: cmp dl, al [Equation] cmp(#5, 0x39) [Equation] cmp(xor(x, 0x55), 0x39) [Z3 Solver]------------------------------------- (solver (= (bvxor x #x00000055) #x00000039)) (define-fun x () (_ BitVec 32) #x0000006c) The good value is 0x6c [Z3 Solver]------------------------------------- [READ in 7fff597b37a2] 400698: movzx eax, byte ptr [rax] [Constraint] #6 = 0x69 eax is now tainted [FOLLOW] 40069b: mov edx, eax [Constraint] #7 = #6 [FOLLOW] 4195997: xor edx, 0x55 [Constraint] #8 = xor(#7, 0x55) [READ in 4007ee] 4006a7: movzx eax, byte ptr [rax] eax is now freed [FOLLOW] 4006aa: cmp dl, al [Equation] cmp(#8, 0x3c) [Equation] cmp(xor(x, 0x55), 0x3c) [Z3 Solver]------------------------------------- (solver (= (bvxor x #x00000055) #x0000003c)) (define-fun x () (_ BitVec 32) #x00000069) The good value is 0x69 [Z3 Solver]------------------------------------- [READ in 7fff597b37a3] 400698: movzx eax, byte ptr [rax] [Constraint] #9 = 0x00 eax is now tainted [FOLLOW] 40069b: mov edx, eax [Constraint] #10 = #9 [FOLLOW] 4195997: xor edx, 0x55 [Constraint] #11 = xor(#10, 0x55) [READ in 4007ef] 4006a7: movzx eax, byte ptr [rax] eax is now freed [FOLLOW] 4006aa: cmp dl, al [Equation] cmp(#11, 0x21) [Equation] cmp(xor(x, 0x55), 0x21) [Z3 Solver]------------------------------------- (solver (= (bvxor x #x00000055) #x00000021)) (define-fun x () (_ BitVec 32) #x00000074) The good value is 0x74 [Z3 Solver]------------------------------------- [SPREAD] 7f9ac23db7db: mov edx, 0x1 output: edx | input: constant edx is now freed $ cat serial.txt elit% $ ../../../pin -t ./obj-intel64/ConcolicExecution.so -taint-file serial.txt -- ./crackme1 [TAINT] bytes tainted from 0x7fff313be550 to 0x7fff313be650 (via read) [READ in 7fff313be550] 400698: movzx eax, byte ptr [rax] [Constraint] #0 = 0x65 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(x, 0x55), 0x30) [Z3 Solver]------------------------------------- (solver (= (bvxor x #x00000055) #x00000030)) (define-fun x () (_ BitVec 32) #x00000065) The good value is 0x65 [Z3 Solver]------------------------------------- [READ in 7fff313be551] 400698: movzx eax, byte ptr [rax] [Constraint] #3 = 0x6c eax is now tainted [FOLLOW] 40069b: mov edx, eax [Constraint] #4 = #3 [FOLLOW] 4195997: xor edx, 0x55 [Constraint] #5 = xor(#4, 0x55) [READ in 4007ed] 4006a7: movzx eax, byte ptr [rax] eax is now freed [FOLLOW] 4006aa: cmp dl, al [Equation] cmp(#5, 0x39) [Equation] cmp(xor(x, 0x55), 0x39) [Z3 Solver]------------------------------------- (solver (= (bvxor x #x00000055) #x00000039)) (define-fun x () (_ BitVec 32) #x0000006c) The good value is 0x6c [Z3 Solver]------------------------------------- [READ in 7fff313be552] 400698: movzx eax, byte ptr [rax] [Constraint] #6 = 0x69 eax is now tainted [FOLLOW] 40069b: mov edx, eax [Constraint] #7 = #6 [FOLLOW] 4195997: xor edx, 0x55 [Constraint] #8 = xor(#7, 0x55) [READ in 4007ee] 4006a7: movzx eax, byte ptr [rax] eax is now freed [FOLLOW] 4006aa: cmp dl, al [Equation] cmp(#8, 0x3c) [Equation] cmp(xor(x, 0x55), 0x3c) [Z3 Solver]------------------------------------- (solver (= (bvxor x #x00000055) #x0000003c)) (define-fun x () (_ BitVec 32) #x00000069) The good value is 0x69 [Z3 Solver]------------------------------------- [READ in 7fff313be553] 400698: movzx eax, byte ptr [rax] [Constraint] #9 = 0x74 eax is now tainted [FOLLOW] 40069b: mov edx, eax [Constraint] #10 = #9 [FOLLOW] 4195997: xor edx, 0x55 [Constraint] #11 = xor(#10, 0x55) [READ in 4007ef] 4006a7: movzx eax, byte ptr [rax] eax is now freed [FOLLOW] 4006aa: cmp dl, al [Equation] cmp(#11, 0x21) [Equation] cmp(xor(x, 0x55), 0x21) [Z3 Solver]------------------------------------- (solver (= (bvxor x #x00000055) #x00000021)) (define-fun x () (_ BitVec 32) #x00000074) The good value is 0x74 [Z3 Solver]------------------------------------- [READ in 7fff313be554] 400698: movzx eax, byte ptr [rax] [Constraint] #12 = 0x00 eax is now tainted [FOLLOW] 40069b: mov edx, eax [Constraint] #13 = #12 [FOLLOW] 4195997: xor edx, 0x55 [Constraint] #14 = xor(#13, 0x55) [READ in 4007f0] 4006a7: movzx eax, byte ptr [rax] eax is now freed [FOLLOW] 4006aa: cmp dl, al [Equation] cmp(#14, 0x30) [Equation] cmp(xor(x, 0x55), 0x30) [Z3 Solver]------------------------------------- (solver (= (bvxor x #x00000055) #x00000030)) (define-fun x () (_ BitVec 32) #x00000065) The good value is 0x65 [Z3 Solver]------------------------------------- [SPREAD] 7f0d00e1f7db: mov edx, 0x1 output: edx | input: constant edx is now freed $ cat serial.txt elite% $ ./crackme1 Good boy