Google CTF 2020 [.Net-RE]

I got to know that Google CTF had some interesting rev challs. I was late for it so I didn’t participate in the event with a team and also we aren’t quite active these days.
I picked up 2nd least solved reversing challenge ie. .Net. Its an interesting challenge and I learnt a lot from it as well, so it might be a little longer than usual but its worth it in the end.


.Net is great, especially because of all its weird features.
Download : chall.tar.gz


  • Dynamic Instrumentation using HarmonyLib
  • C# <=> Native asm FFI
  • IDAPython Scripting to assist in native functions analysis
  • Replicate algo in python and then finding a valid solution for it using z3


The challenge includes two files ie. 0Harmony.dll and EKTORPFlagValidator.exe.
So the name looks a bit weird. I just googled them and found that Harmony is actually a libary for doing some runtime patching stuff in .Net apps.

With the help of a sample run, we see that it requires a string of length = 30 and also that it validates a checksum from our input.


Static Analysis

So lets start at the entrypoint. And yeah at first I tried to analyse the constructor too but it looked kinda hard to understand statically and I left it for debugging at last.


So there is this main method which later calls LaunchGui() and as a result we are now in KVOT class.



Now we are inside KVOT and it looks like method names are weird.


After the basic initialization part for the GUI there is an event handler submit_button_Click() which looks exactly how we want it to be.


Ahmmm It does the string length check here, and if it succeeds then call another method with our input string as an argument to SOCKERBIT.GRUNDTAL_NORRVIKEN which returns a list.
Also after that it does a basic check that the elements of the returned list are all less than 63 which looks like a character range check from the failure string.


And yeah, There is more to it, just hold up.
GRUNDTAL_NORRVIKEN then calls DecodeBase64Bytewise on each of the element of our string.


Hmm, now it gets weird… the DecodeBase64Bytewise method looks like it is trying to instead encode our input and also it checks some conditions which would never return true except the 123('{') and 125('}') check.


That means if we input some lowercase characters which should be valid, then it’ll just return a list of 30 -1’s.


But the signness trick here casts it to an unsigned integer.
Something like this :

if ((uint)(byte)(arg + 191) <= 25u)
  Console.WriteLine((uint)(byte)(arg + 191));  // overflows  
  return (sbyte)(arg - 55);

For eg. ‘H’(72) fulfills the above condition since (byte)(72+191) is 7 when cast to a byte and not 263.

This is the 2nd part of the check routine with methods DAGSTORP, SMORBOLL and HEROISK.
A list is initialized and passed to DAGSTORP along with our encrypted input.


Ahh, It just looks like a simple xor, ezpz!


Then there is this checksum as you’ve guessed it from the failure string. It calculates the checksum on the basis that it does different calculations according to the index value.
The index value checks are just for checking whether the index is divisible by 2,3,5 or 7 and FYI, it doesn’t include the index 28 as it is later compared with the final checksum value.


And then there is method VAXMYRA which just checks if there are any duplicates in the encrypted array.


And after bypassing through the checksum validation and VAXMYRA we get to the main condition checks that validates our encrypted input. And Yes, I smell z3!


Dynamic Analysis

Getting to the main fun part ie. debugging it in dnsPy.
Huh wait a sec where is FYRKANTIG. Instead we get redirected to NUFFRA and now it looks more complicated and gibberish to deal with.


So to explain this inner magic and so called weirdness we’ll have to debug right from the constructor. If you’d traced the execution accurately, you’ll find that there is a calli instruction which calls a method by specifying its address as an argument.


I noticed that it calls several functions and just noted down the method addresses ie. from num variable.

0x600003B   # Debugger.IsAttached() check (native)
0x6000046   # patch functions routine (native)

0x60000D9   # we don't care about the 0xD6-0xDC functions

0x600003B has a simple anti-debug check with System.Diagnostics.Debugger.IsAttached!


0x6000046 is the magic method here which in turn calls another native function.


That native function has another anti-debug technique implemented ie kernel32.dll::IsDebuggerPresent and if it is true it returns 1 which eventually doesn’t do anything and the latter will call a c# method which is indeed responsible for changing the methods.


And Fortunately it happens that dnsPy has got us covered and was successful in deafeating those anti-debug techniques like a ninja. All thanks to this issue

Harmony Magic

So this is the function called if the isDebuggerPresent returns false and it looks like it is patching the original methods we found during the static analysis to some other methods.


How Harmony works

Harmony docs explains it better but basically here it just patches a method body at runtime.

From docs :
Where other patch libraries simply allow you to replace the original method, Harmony goes one step further and gives you:

  • A way to keep the original method intact
  • Execute your code before and/or after the original method
  • Modify the original with IL code processors
  • Multiple Harmony patches co-exist and don’t conflict with each other


As a reference we can have this Patched Method List :

Original method Patched Method
(static fcn caller)
(native fcn caller)
(DecodeBase64ByteWise() caller)
(str to list convertor)
(xor implementation)
(anti-debug check [GODDAG])

Analysing Native Functions with IDAPython

Digging Deeper we need to analyse these native functions in some dissasembler like IDA, as dnsPy fails for them. These are the three main native functions called by method NUFFRA. Also, note down the RVAs marked in Red, these are the references to the native functions.


In IDA, we should load it as a normal PE file and then define some code at different locations as IDA doesn’t recognise it very well. Here we can either rebase the program to make it try to load from 0x0 or add 0x400000 to the RVA and then analyse it.


Func 1 [GODDAG]

We can just go over that address (0x00001930) and defining it as code pretty much clears what is it used for. So there is a anti-debug check, and this looks like the right function as well since it returns True/False, which is then used in the C# code to progress further if False.



The second important function is performing some functions on our input string elements.


Now this native function is interesting as the defined functions are just dwords and If we observe these are just referencing the C# code instead.

This can be illustrated by the following :


For automatically renaming these dwords we first we need to navigate to Storage Stream -> Method to get a full list of methods.


We can then copy them, make a json file with token and method names as the keys and values respectively. Now we can write an IDAPython script to rename the dwords recognised by IDA with the name as ‘dword_xxxx’ accordingly.
TBH this idea of scripting IDA struck to me while doing this writeup lol.

def rename_dwords():
  f = open('method_map.json') 
  method_map = json.load(f) 
  token_list = [int(x,16) for x in method_map.keys()]

  data_seg_selector = idc.SegByName('.data')
  data_seg_startea = idc.SegByBase(data_seg_selector)
  data_seg_endea = idc.SegEnd(data_seg_startea)

  #maybe compability issue
  SN_FORCE = 0x800

  for ea in range(data_seg_startea, data_seg_endea):
    var_name = Name(ea)
    if 'dword' in var_name:
      dword_val = Dword(ea)

      if dword_val in token_list:
        formatted_token = "0x0%X" % dword_val
        new_name = str(method_map[formatted_token])
        idc.set_name(ea, new_name, SN_NOCHECK | SN_FORCE)
        print "done renaming " + var_name +" to " + new_name

Ahh We get a nice and clean view of all the renamed referenced dwords as functions though I’ll not refer to this renaming fashion in this writeup since it is not the best way to make a third person understand the algo as afterall it has method names which will be long af along with their class which we don’t care about here.


Continuing with the analysis of NativeGRUNDTAL_NORRVIKEN, we see some offset calculations and dereferencing a pointer from that offset and later returning it.


Yes! This looks like the main encryption algo. This checks if the character is in the valid chars range and then encrypts it. The last two checks are similar for curly braces.


And after some renaming, the NativeGRUNDTAL_NORRVIKEN function looks like the following which concludes that it is only used for encrypting the string.
Also FYI, it uses another list for storing the encrypted string as there is another get_element_from_index func.


Func 3 [FYRKANTIGImpl]


So There are two vars used from the .rdata section in the function, one of them is an array and other one doesn’t look interesting as it is a stack variable.


The function which uses is referenced in C# and looks like it is just used to initialize the array.


And yeah we get that xor function in sub_39D0 and FYI sub_4DFC is same as net51_offset_calc.
So till now It has xored our encrypted input with the array it just initialized.


Moving on, we can clearly see that sub_3F10 is used for performing some random shuffling on the resulting xored array.


There is no point in wasting time on analysing it as we can just note the num ie. the offset (randomly generated but seeded with a static value) by setting the breakpoint as shown below and watching its value on every iteration which makes some swaps with the encrypted input list.


This is what the native function looked after renaming some stuff.


So the main algo of FYRKANTIGImpl is just to xor and random shuffle our encrypted input. I’ve renamed some other functions now for better understanding.


We can also script some part of defining and renaming functions just from their RVAs.
This also let me think that this can be implemented into a plugin package.

def define_functions():
  native_rvas = [0x1930, 0x3A90, 0x44b0,]
  native_rvas = [(0x400000 + x) for x in native_rvas]

  for ea in native_rvas:
    if ea == 0x401930:
      # undefine and force convert to code as IDA doesn't analyse it at first
      print "Defining fcn GODDAG at 0x%x" % ea
      print "Making", ea, "unknown and defining it to code..."
      if ea == 0x403A90:
        fcn_name = "NativeGRUNDTAL_NORRVIKEN"
        print "Defining fcn %s at 0x%x" % (fcn_name, ea)
      elif ea == 0x4044B0:
        fcn_name = "FYRKANTIGImpl"
        print "Defining fcn %s at 0x%x" % (fcn_name, ea)
      idc.MakeNameEx(ea, fcn_name, idc.SN_NOWARN)

This was the main algo part implemented in the native functions, which were added at runtime. Incase you are wondering what does SPARSAM function does, so it just converts the list returned from these native functions to a string.

Z3 & Profit

Hell yeah! time for z3 as we are quite sure about how this challenge works :)
FYI, I’m not much experienced with z3 and it always has some surprises for me.

So at first I tried to just replicate the algo and check if it finds any valid solution. I initialized the input with the following constraints.

s.add(And(inp[i]<=48, inp[i]>=125))

Then I add some If’s to encrypt our input so kinda do it all in z3

  for i in range(len(inp)):
    inp[i] = If ( inp[i] - 48 <= 9,
          inp[i] - 48,
    inp[i] = If ( inp[i] - 65 <= 25,
          inp[i] - 55,
    inp[i] = If ( inp[i] - 97 <= 25,
          inp[i] - 61,
    inp[i] = If ( inp[i] == 123,
    inp[i] = If ( inp[i] == 125,

And I got UNSAT! :(
I asked for some help from my friends but the timezones messed up and I was determined enough to solve it myself now!

Finally I came up with an idea of removing just the z3 If statements and rather began with the encrypted input initially which had a range of (0, 63). And simply wrote a decrypt function for it.

def decode_inp(enc):
  dec = ""
  valid_range1 = ord('9') - ord('0')
  valid_range2 = ord('Z') - ord('0') - 7
  valid_range3 = ord('z') - ord('0') - (7+6)

  for c in enc:
    if c <= valid_range1:
      dec += chr(c + 48)
    elif c <= valid_range2:
      dec += chr(c + 55)
    elif c <= valid_range3:
      dec += chr(c + 61)
    elif c == 62:
      dec += '{'
    elif c == 63:
      dec += '}'

  return dec

WTH, Still UNSAT !!


And after spending some time tinkering around I figured out that it was some unsigned expressions shit in z3 which just made me mad (indescribable).

s.add(UGE(MATHOPEN[29], 1))
s.add(ULE(MATHOPEN[0] + MATHOPEN[1] + MATHOPEN[2] + MATHOPEN[3] + MATHOPEN[4] - 130, 10))

In Z3Py, the operators <, <=, >, >=, /, % and » correspond to the signed versions. The corresponding unsigned operators are ULT, ULE, UGT, UGE, UDiv, URem and LShR.

Reference :

from z3 import *

def xor_mod(mod_list):
  xor_mask = [0x1F, 0x23, 0x3F, 0x3F, 0x1B, 0x07, 0x37, 0x21, 0x04, 0x33, 0x09, 0x3B, 0x39, 0x28, 0x30, 0x0C, 0x0E, 0x2E, 0x3F, 0x25, 0x2A, 0x27, 0x3E, 0x0B, 0x27, 0x1C, 0x38, 0x31, 0x1E, 0x3D]

  lol = []
  for i in range(len(mod_list)):
    lol.append(mod_list[i] ^ xor_mask[i])
  return lol

def get_checksum(mod_list):
  num = 16

  for i in range(len(mod_list)):
    if (i != len(mod_list) - 2):
      num = mod_list[i] + num

      if (i % 2 == 0):
        num = mod_list[i] + num
      if (i % 3 == 0):
        num = mod_list[i] * 4294967294 + num
      if (i % 5 == 0):
        num = mod_list[i] * 4294967293 + num
      if (i % 7 == 0):
        num = mod_list[i] * 4 + num
      num &= 0xffffffff

  return num & 63

def random_shuffle(arg_list):
  num_list = [0, 1, 0, 2, 3, 3, 7, 0, 6, 7, 7, 0, 3, 0xa, 0x6, 0xf, 0x3, 0x5, 0xc, 0xe, 0x3, 0x5, 0x8, 0x11, 0x17, 0x16, 0xa ]
  j = 1
  for i in num_list:
    if i != j:
      #print "Swapping :", (hex(arg_list[i]), hex(arg_list[j]) )
      #print "num =", hex(i)
      arg_list[i], arg_list[j] = arg_list[j], arg_list[i]
    #print i,j  

  return arg_list

def swap_more(arg_list):
  for j in range(0,len(arg_list)-3,3):
    arg_list[j], arg_list[j+1] = arg_list[j+1], arg_list[j]

  return arg_list

def decode_inp(enc):
  dec = ""
  valid_range1 = ord('9') - ord('0')
  valid_range2 = ord('Z') - ord('0') - 7
  valid_range3 = ord('z') - ord('0') - (7+6)

  for c in enc:
    if c <= valid_range1:
      dec += chr(c + 48)
    elif c <= valid_range2:
      dec += chr(c + 55)
    elif c <= valid_range3:
      dec += chr(c + 61)
    elif c == 62:
      dec += '{'
    elif c == 63:
      dec += '}'

  return dec

def final_conds(MATHOPEN, s):
  s.add(MATHOPEN[1] == 25)
  s.add(MATHOPEN[2] == 23)
  s.add(MATHOPEN[9] == 9)
  s.add(MATHOPEN[20] == 45)
  s.add(MATHOPEN[26] == 7)
  s.add(UGE(MATHOPEN[8], 15))
  s.add(ULE(MATHOPEN[12], 4))
  s.add(UGE(MATHOPEN[14], 48))
  s.add(UGE(MATHOPEN[29], 1))

  s.add(ULE(MATHOPEN[0] + MATHOPEN[1] + MATHOPEN[2] + MATHOPEN[3] + MATHOPEN[4] - 130, 10))
  s.add(ULE(MATHOPEN[5] + MATHOPEN[6] + MATHOPEN[7] + MATHOPEN[8] + MATHOPEN[9] - 140, 10))
  s.add(ULE(MATHOPEN[10] + MATHOPEN[11] + MATHOPEN[12] + MATHOPEN[13] + MATHOPEN[14] - 150 ,10)) 
  s.add(ULE(MATHOPEN[15] + MATHOPEN[16] + MATHOPEN[17] + MATHOPEN[18] + MATHOPEN[19] - 160 ,10)) 
  s.add(ULE(MATHOPEN[20] + MATHOPEN[21] + MATHOPEN[22] + MATHOPEN[23] + MATHOPEN[24] - 170 ,10)) 

  s.add(ULE(MATHOPEN[0] + MATHOPEN[5] + MATHOPEN[10] + MATHOPEN[15] + MATHOPEN[20] + MATHOPEN[25] - 172, 6)) 
  s.add(ULE(MATHOPEN[1] + MATHOPEN[6] + MATHOPEN[11] + MATHOPEN[16] +MATHOPEN[21] + MATHOPEN[26] - 162, 6)) 
  s.add(ULE(MATHOPEN[2] + MATHOPEN[7] + MATHOPEN[12] + MATHOPEN[17]+ MATHOPEN[22] + MATHOPEN[27] - 152, 6)) 
  s.add(ULE(MATHOPEN[3] + MATHOPEN[8] + MATHOPEN[13] + MATHOPEN[18] + MATHOPEN[23] - 142, 6)) 
  s.add(ULE(MATHOPEN[4] + MATHOPEN[9] + MATHOPEN[14] + MATHOPEN[19] + MATHOPEN[24] + MATHOPEN[29] - 132, 6)) 

  num45 = ((MATHOPEN[7] + (MATHOPEN[27] * 3)) * 3 - MATHOPEN[5] * 13) - 57
  s.add(ULE(num45, 28))
  num45 = (MATHOPEN[22] * 3 + ((MATHOPEN[14] << 2) - (MATHOPEN[20] * 5))) - 12
  s.add(ULE(num45, 70))

  num46 = (MATHOPEN[14] + (MATHOPEN[16] * 2)) * 2 + ((MATHOPEN[15] - ( MATHOPEN[18] * 2)) * 3) - MATHOPEN[17] * 5
  s.add(MATHOPEN[13] + num46 == 0)

  s.add(MATHOPEN[5] == MATHOPEN[6] * 2)
  s.add(MATHOPEN[29] + MATHOPEN[7] == 59)
  s.add(MATHOPEN[0] == MATHOPEN[17] * 6)
  s.add(MATHOPEN[8] == MATHOPEN[9] * 4)
  s.add(MATHOPEN[11] << 1 == MATHOPEN[13] * 3)
  s.add(MATHOPEN[13] + MATHOPEN[29] + MATHOPEN[11] + MATHOPEN[4] == MATHOPEN[19])
  s.add(MATHOPEN[10] == MATHOPEN[12] * 13)

def main():
  s = Solver()
  inp = []

  for i in range(30):
    b = BitVec("%d_i" % i, 32)
    s.add(ULE(inp[i], 63))

  xor_res_list = xor_mod(inp)
  res1 = random_shuffle(xor_res_list)
  res2 = swap_more(res1)

  ret_num = get_checksum(res2)

  s.add(res2[28] == ret_num )

  final_conds(res2, s)

  print s.check()

  if s.check() == sat:
    sol = s.model()
    flag = []
    for i in range(len(inp)):
      c = inp[i]
    print flag
    print decode_inp(flag)

if __name__ == "__main__":
[12, 29, 15, 62, 12, 51, 51, 12, 47, 53, 18, 54, 32, 40, 44, 53, 39, 11, 56, 55, 27, 40, 36, 47, 47, 60, 15, 56, 49, 63]

Solution Files

I’ve uploaded all the files including the IDAPython and z3 solver scripts along with the idb file on my github here :


I hope you liked this writeup :)
Well, Thanks for reading it…