search

GaloisInc / pate

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

challenge 03 instruction desync #282

Closed robdockins closed 5 months ago

robdockins commented 2 years ago

As of 0d80f8dbe336d47a056a83567de1fe0ceae9b741, the challenge 03 variant problem does not have the expected result.

$ cabal run pate -- -o demos/challenge03-variant/challenge03.orig.exe -p demos/challenge03-variant/challenge03.patched.exe -V Debug --log-file pate.log -b demos/challenge03-variant/challenge03.toml --strongestpost

ConcreteAddress 0x10778 program control flow desynchronized
  Original: 0x1079c analysis failure Just (0x10798,"0x10798: BX_A1(0001xxxx.IIIIIIII.0010IIII.xxxx0001) Rm 14, cond 0, QuasiMask0 QuasiMask\"(\"12): 4095")
  Patched:  0x1079c analysis failure Just (0x10798,"0x10798: BX_A1(0001xxxx.IIIIIIII.0010IIII.xxxx0001) Rm 14, cond 0, QuasiMask0 QuasiMask\"(\"12): 4095")
ConcreteAddress 0x116bc program control flow desynchronized
  Original: 0x116dc branch Just (0x11700,"0x11700: B_A1(xxxxxxxx.xxxxxxxx.xxxxxxxx.xxxx1010) cond 9, imm24 16777205")
  Patched:  0x116dc branch Just (0x11700,"0x11700: B_A1(xxxxxxxx.xxxxxxxx.xxxxxxxx.xxxx1010) cond 9, imm24 16777205")
Overall verification verdict: Inequivalent

The interesting aspects of the analysis seems to be masked by issues with the listed instructions. It's not clear to me why, but perhaps this is also related to conditional call/return issues.

travitch commented 2 years ago

Ah yes, we still need conditional calls. Let me open a ticket specifically about that (with reference to this one)

robdockins commented 2 years ago

To be clear, I'm not sure this is about conditional calls. I'm not 100% what to make of the listed instructions.

travitch commented 2 years ago

Ah I guess neither of those is a call (call would be branch and link, so BL or BLX).

robdockins commented 2 years ago

NB, backing up to c0f3626c60114863b4d23dae53ee9d0f1517971f gives slightly different results. I'm not sure what to make of the difference.

ConcreteAddress 0x10778 program control flow desynchronized
  Original: 0x1079c analysis failure Just (0x10798,"0x10798: BX_A1(0001xxxx.IIIIIIII.0010IIII.xxxx0001) Rm 14, cond 0, QuasiMask0 QuasiMask\"(\"12): 4095")
  Patched:  0x1079c analysis failure Just (0x10798,"0x10798: BX_A1(0001xxxx.IIIIIIII.0010IIII.xxxx0001) Rm 14, cond 0, QuasiMask0 QuasiMask\"(\"12): 4095")
ConcreteAddress 0x11e7c program control flow desynchronized
  Original: 0x11e88 syscall Just (0x11e84,"0x11e84: BX_A1(0001xxxx.IIIIIIII.0010IIII.xxxx0001) Rm 14, cond 0, QuasiMask0 QuasiMask\"(\"12): 4095")
  Patched:  0x11e88 syscall Just (0x11e84,"0x11e84: BX_A1(0001xxxx.IIIIIIII.0010IIII.xxxx0001) Rm 14, cond 0, QuasiMask0 QuasiMask\"(\"12): 4095")
Overall verification verdict: Inequivalent