4

I have this pseudo code:

v5 = serial[6] + serial[0] - serial[7] - serial[2];
LOBYTE(v5) = serial[1];
v8 = serial[3] + v5 - serial[4];
if ( v8 != serial[5] )
    goto FAIL;

The variable serial[] is an array representing the bytes of the key abcdefgh. Dor example, serial[0] = 0x61. If we assume that serial[5] is 0x66 (the letter 'f'), how can I calculate the needed key to get a 0x66 in v8 as you can see some calculations are done to decide the possible values of v8.

1
  • 1
    i would prefer disasm instead of this pseudo form from what i see i think the algo might be discarding the sign bits with movzx so it would end up with b+ d - e = result so result would be a ie abcdeagh see if it makes sense – blabb Jul 2 '17 at 7:53
4

Well, the equation is pretty simple, you say that the hashing is done through the following formula:

v5 = serial[6] + serial[0] - serial[7] - serial[2];
LOBYTE(v5) = serial[1];
v8 = serial[3] + v5 - serial[4];
if ( v8 != serial[5] )
    goto FAIL;

We can use an SMT-solver, such as Z3 to find out a possible key for these equations:

$> python
Python 2.7.13 (default, Jan 19 2017, 14:48:08) 
[GCC 6.3.0 20170118] on linux2
Type "help", "copyright", "credits" or "license" for more information.
>>> from z3 import *
>>> serial0 = BitVec('serial0', 8)
>>> serial1 = BitVec('serial1', 8)
>>> serial2 = BitVec('serial2', 8)
>>> serial3 = BitVec('serial3', 8)
>>> serial4 = BitVec('serial4', 8)
>>> serial5 = BitVec('serial5', 8)
>>> serial6 = BitVec('serial6', 8)
>>> serial7 = BitVec('serial7', 8)
>>> v5 = BitVec('v5', 16)
>>> v8 = BitVec('v8', 16)
>>> v5 = ((serial6 + serial0 - serial7 - serial2) & 0xff00) + serial1
>>> v8 = serial3 + v5 - serial4
>>> s = Solver()
>>> s.add(v8 == serial5)
>>> s.check()
sat
>>> s.model()
[serial3 = 0, serial1 = 0, serial4 = 0, serial5 = 0]
>>> 
>>> s.add(serial1 != 0)
>>> s.check()
sat
>>> s.model()
[serial1 = 128, serial3 = 172, serial5 = 0, serial4 = 44]

As, I got a degenerated solution, I added the constraint that serial1 has to be different from zero. In fact, you can add any constraint as you wish (you may try to force the serials to be within the standard printable ASCII characters if you wish (beware, it may admit no solution!).

7
  • thus smt solver also generalised it to b+d -e = f so adding a constraint as assert ( > f 0x60 ) should yield 0x61 i think – blabb Jul 4 '17 at 6:20
  • thanks a lot that's exactly what i need. (sorry i can't accept the answer since the question was submitted before i joined in) – 0x3h Jul 4 '17 at 7:27
  • Hmmm, this article remind me something --> 'Assemby to pseudo-code manually'. – perror Jul 5 '17 at 12:26
  • @0x3h in case you did not get my flag message, use "contact us" link at the bottom to merge the two accounts. – Igor Skochinsky Jul 5 '17 at 13:08
  • @perror lol yes that's right :) i removed the blog anyway.. i discovered i'm not really a blog person. – 0x3h Jul 6 '17 at 5:35
3

expanding a bit on the answer by perror and my initial hypothesis

the result for the provided input string "abcdefgh" would result in "b+d-e = f"

providing constraints for input string z3 indeed returns back

the char "a" as the first possible model() here is a slightly modified python script posted by perror in his answer

:\>cat z3t.py
from z3 import *
s0,s1,s2,s3,s4,s5,s6,s7 = BitVecs( 's0 s1 s2 s3 s4 s5 s6 s7', 8)
v5,v8 = BitVecs ('v5 v8', 16)
v5 = ((s6 + s0 - s7 - s2) & 0xff00) | s1
v8 = s3 + v5 - s4
s = Solver()
s.add(v8 == s5,s0 == ord('a'),s1 == ord('b'),s2 == ord('c'),s3 == ord('d'))
s.add(s4 == ord('e'), s5 > 0x60,s6 == ord('g'),s7 == ord('h'))
s.check()
print chr((s.model()[s5]).as_long())


:\>python .\z3t.py
a
1
  • Yes, I should have restricted to alphanum, you are definitely right and complete in your answer... You deserved to get my vote (I am just a lazy bastard sometimes! :-)). – perror Jul 4 '17 at 10:54

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.