main.c

#include <unistd.h>

int main() {
   int a;
   int *c = malloc(sizeof(int));
   // 1. constraint: a[t - 3] = β, c = *μ
   // 2. concrete: a[t - 3] = 0, c = 0x10, mem[0x10][t - 2] = 0;
   
   read(fileno(stdin), &a, sizeof(a));
   // 1. constraint: a[t - 2] = α where α > 10 && α <= 11 
   // 2. concrete: a[t - 2] = 11
   int *b = NULL;
   
   if (a > 11) {
      printf("foobar\n");
   }
   
   // 1. constraint: *c[t - 2] = μ[t - 2] = α
   // 2. concrete: mem[0x10][t - 2] = 11
   *c = a;
   free(c);
   c = NULL;
   
   if (a > 10) {
     // 1. constraint: a[t - 2] = α;
     // 2. concrete: a[t - 2] = 11
     read(fileno(stdin), &a, sizeof(a));
     // 1. constraint: a[t - 1] = 5 - 1 = 4;
     // 2. concrete: a[t - 1] = 4
     a = a + 1;
   }

   if (a > 0) {
     // START HERE!
     // Program crash with the following information:
     // - core dump:
     //    - a[t] = 5, b = NULL;
     //    - (valid?) stack
     // - Complete control flow from processor trace;
     // GOAL: travel back in time and get an aquivalent previous core dump
     // Approach:
     // 1. Build constraint set by symbolically executing the program backwards
     // 2. At any point a previous version of a *concrete* coredump can be generated, that is forward executable
     *b = a;
   }
}