Formal Verification of Code Obfuscations in Coq

These obfuscations have been specified using CompCert 2.5.

Browsable version of the Coq files:

• Control Flow Graph Flattening Transformation code
• Control Flow Graph Flattening Proof Proof code

The corresponding Coq files are available here:

• ControlFlowGraphFlattening.v
• ControlFlowGraphFlatteningproof.v

Compilation chain with Control Flow Graph Flattening transformation plugged in:

• Compiler
• Compiler.v

Here is an example of input/output:

int main(void) {
  int i = 0;
  while (i < 100) {
    i++;
  }
  return i;
}

int main(void)
{
  register unsigned int $34;
  register int $33;
  $34 = 4294967294U;
  while (1) {
    if (! ($34 != 4294967295U)) {
      break;
    }
    switch ($34) {
      case -2:
        $34 = 4294967293U;
        break;
      case -3:
        $34 = 4294967292U;
        break;
      case -4:
        $34 = 4294967291U;
        break;
      case -5:
        $33 = 0;
        $34 = 4294967290U;
        break;
      case -6:
        $34 = 4294967289U;
        break;
      case -7:
        $34 = 4294967288U;
        break;
      case -8:
        $34 = 4294967287U;
        break;
      case -9:
        $34 = 4294967286U;
        break;
      case -10:
        $34 = 4294967285U;
        break;
      case -11:
        if ($33 < 100) {
          $34 = 4294967284U;
          break;
        } else {
          $34 = 4294967283U;
          break;
        }
      case -12:
        $34 = 4294967282U;
        break;
      case -13:
        $34 = 4294967278U;
        break;
      case -14:
        $34 = 4294967281U;
        break;
      case -15:
        $34 = 4294967280U;
        break;
      case -16:
        $33 = $33 + 1;
        $34 = 4294967279U;
        break;
      case -17:
        $34 = 4294967289U;
        break;
      case -18:
        $34 = 4294967277U;
        break;
      case -19:
        $34 = 4294967276U;
        break;
      case -20:
        return $33;
        $34 = 4294967295U;
        break;
      
    }
  }
}