search

GaloisInc / pate

Patches Assured up to Trace Equivalence
Other
14 stars 3 forks source link

challenge 06 desync issues #285

Closed robdockins closed 5 months ago

robdockins commented 2 years ago

The simplified challenge 06 example also suffers from control-flow desync issues, as of https://github.com/GaloisInc/pate/commit/0d80f8dbe336d47a056a83567de1fe0ceae9b741 and with the programtargets patch 41765a26fd93c58bd4f0c34233c2f2b29ba96f9e

cabal run pate -- -o ~/code/programtargets/challenge06-simplified/build/program_c -p ~/code/programtargets/challenge06-simplified/build/program_c.patched -V Debug --log-file ch06.log --strongestpost -b ~/code/programtargets/challenge06-simplified/build/challenge06.toml
ConcreteAddress 0x1065c (original) vs. ConcreteAddress 0x10698 (patched) program control flow desynchronized
  Original: 0x10680 analysis failure Just (0x1067c,"0x1067c: BX_A1(0001xxxx.IIIIIIII.0010IIII.xxxx0001) Rm 14, cond 0, QuasiMask0 QuasiMask\"(\"12): 4095")
  Patched:  0x106bc analysis failure Just (0x106b8,"0x106b8: BX_A1(0001xxxx.IIIIIIII.0010IIII.xxxx0001) Rm 14, cond 0, QuasiMask0 QuasiMask\"(\"12): 4095")
ConcreteAddress 0x1065c (original) vs. ConcreteAddress 0x10698 (patched) program control flow desynchronized
  Original: 0x10680 analysis failure Just (0x1067c,"0x1067c: BX_A1(0001xxxx.IIIIIIII.0010IIII.xxxx0001) Rm 14, cond 0, QuasiMask0 QuasiMask\"(\"12): 4095")
  Patched:  0x106bc analysis failure Just (0x106b8,"0x106b8: BX_A1(0001xxxx.IIIIIIII.0010IIII.xxxx0001) Rm 14, cond 0, QuasiMask0 QuasiMask\"(\"12): 4095")
ConcreteAddress 0x10a84 (original) vs. ConcreteAddress 0x10ac0 (patched) program control flow desynchronized
  Original: 0x10554 function call Just (0x10ab4,"0x10ab4: BLX_r_A1(0011xxxx.IIIIIIII.0010IIII.xxxx0001) Rm 3, cond 14, QuasiMask0 QuasiMask\"(\"12): 4095")
  Patched:  0x10588 function call Just (0x10af0,"0x10af0: BLX_r_A1(0011xxxx.IIIIIIII.0010IIII.xxxx0001) Rm 3, cond 14, QuasiMask0 QuasiMask\"(\"12): 4095")
Overall verification verdict: Inequivalent

The BLX is an indirect call, I think, which might be kind of tricky. Perhaps the constant-propagation pass will help.

travitch commented 2 years ago

That is likely the memcpy that was called by function pointer. Constant propagation could (in principle) help there. More generally, we could be in trouble with function pointers. I guess the WP verifier was super unsound around those anyway, but doing it well will be challenging. The mitigation to that complexity is #269.

robdockins commented 2 years ago

Backing up to c0f3626c60114863b4d23dae53ee9d0f1517971f does not seem like it makes a difference for this example.