04 Mar 2014 @ 12:56 AM 

Rarverseme is a rar file, and rar has an inbuilt VM which can be programmed(http://blog.cmpxchg8b.com/2012/09/fun-with-constrained-programming.html). Given challenge contains a custom bytecode which will print 🙁 every time upon unraring. Our target is to understand the bytecode, reverse it to find the flag.

Idea is to disassemble/debug the rarVM to figure out what exactly is getting executed. After getting unrar source compiled, rest was pretty straight forward.

rarvm
Running a trace resulted in this.

MOVD [010DC294], 0x00002000
MOVD [010FFC30], 0x796f7572 ;your
MOVD [010FFC34], 0x666c6167 ;flag
MOVD [010FFC38], 0x676f6573 ;goes
MOVD [010FFC3C], 0x68657275 ;heru
MOVD [010DC298], 0x00005000
MOVD [01102C30], 0x31337357 ;13sW
MOVD [01102C34], 0x63561227 ;cV.'
MOVD [01102C38], 0x6666654a ;ffeJ
MOVD [01102C3C], 0x78584148 ;xXAH
JMP 0x000000ae
MOVD [010DC290], 0x796f7572 ; flag[i]
AND 0x796f7572, 0x000000ff
MOVD [010DC29C], 0x31337357 ; arr[i]
AND 0x31337357, 0x000000ff
MUL 0x00000072, 0x00000057 ; flag[i] * arr[i]

MOVD [010DC28C], 0x000026be
MOVD [010DC290], 0x796f7572
SHR 0x796f7572, 0x00000008 
AND 0x00796f75, 0x000000ff
MOVD [010DC29C], 0x63561227
AND 0x63561227, 0x000000ff
MUL 0x00000075, 0x00000027
ADDD 0x00003891, 0x000011d3 ; sum the results

MOVD [010DC290], 0x796f7572
SHR 0x796f7572, 0x00000010
AND 0x0000796f, 0x000000ff
MOVD [010DC29C], 0x6666654a
AND 0x6666654a, 0x000000ff
MUL 0x0000006f, 0x0000004a
ADDD 0x000058a7, 0x00002016

MOVD [010DC290], 0x796f7572
SHR 0x796f7572, 0x00000018
AND 0x00000079, 0x000000ff
MOVD [010DC29C], 0x78584148
AND 0x78584148, 0x000000ff
MUL 0x00000079, 0x00000048
ADDD 0x00007aaf, 0x00002208

CMPD 0x00007aaf, 0x0000706f

its doing a multiplication of flag values and a fixed array and comparing to a hardcoded value. If the comparison is wrong, it is jumping to bad_boy. The whole checking code can be dumped by setting CMPD as success. As we have the code figured, rest was simple bruteforcing. Before I started bruteforcing, my friend wrote a z3 code which runs much faster and yielded the flag as: evenmoarvms?rly?

V = [0x706f, 0x7972, 0x89d1, 0x9cc5]
#add rest of hardcoded values

w0, w1, w2, w3 = BitVecs("w0 w1 w2 w3", 16)

solve( w0 * 0x57 + w1 * 0x27 + w2 * 0x4a + w3 * 0x48 == V[0],  
	   w0 * 0x73 + w1 * 0x12 + w2 * 0x65 + w3 * 0x41 == V[1],  
	   w0 * 0x33 + w1 * 0x56 + w2 * 0x66 + w3 * 0x58 == V[2], 
	   w0 * 0x31 + w1 * 0x63 + w2 * 0x66 + w3 * 0x78 == V[3],
	   ULT(w0, 128), ULT(w1, 128))

Posted By: Dan
Last Edit: 04 Mar 2014 @ 12:56 AM

EmailPermalink
Tags
Categories: CTF, Reverse Engineering


 

Responses to this post » (2 Total)

 
  1. anonymous says:

    I think you also need to patch some fixed values to get the right flag. In this case V[13] = 0x7A0A is not right, it must be 0x7A8A. So how do you managed to fix it?

    • Dan says:

      You are correct about the invalid ‘hash’ value. But it can be solved with 3 equations(4 unknowns and 4 equations are preferred, but still we can solve by providing proper constraints)
      #z3 code
      V = [0x6be4, 0x7a0a, 0x80dc, 0x8d54]

      w0, w1, w2, w3 = BitVecs(“w0 w1 w2 w3”, 16)

      solve( w0 * 0x57 + w1 * 0x27 + w2 * 0x4a + w3 * 0x48 == V[0],
      #w0 * 0x73 + w1 * 0x12 + w2 * 0x65 + w3 * 0x41 == V[1],
      w0 * 0x33 + w1 * 0x56 + w2 * 0x66 + w3 * 0x58 == V[2],
      w0 * 0x31 + w1 * 0x63 + w2 * 0x66 + w3 * 0x78 == V[3],
      ULT(w0, 128), ULT(w1, 128),ULT(w2, 128), ULT(w3, 128))

Post a Comment

XHTML: You can use these tags: <a href="" title=""> <abbr title=""> <acronym title=""> <b> <blockquote cite=""> <cite> <code> <del datetime=""> <em> <i> <q cite=""> <s> <strike> <strong>


 Last 50 Posts
Change Theme...
  • Users » 1
  • Posts/Pages » 19
  • Comments » 41
Change Theme...
  • VoidVoid « Default
  • LifeLife
  • EarthEarth
  • WindWind
  • WaterWater
  • FireFire
  • LightLight

About



    No Child Pages.