Finalize article "Writeups for ... (#36-#74)".

1 files changed, 224 insertions, 70 deletions

diff --git a/org/Writeups for Dennis Yurichev's Reverse Engineering Challenges (#36-)/challenges-re-writeups-4.org b/org/Writeups for Dennis Yurichev's Reverse Engineering Challenges (#36-#74)/challenges-re-writeups-4.org
index a3a1990..1108af7 100644
--- a/org/Writeups for Dennis Yurichev's Reverse Engineering Challenges (#36-)/challenges-re-writeups-4.org
+++ b/org/Writeups for Dennis Yurichev's Reverse Engineering Challenges (#36-#74)/challenges-re-writeups-4.org
@@ -1,6 +1,14 @@
-#+TITLE: Writeups for Dennis Yurichev's Reverse Engineering Challenges (#36-)
+#+TITLE: Writeups for Dennis Yurichev's Reverse Engineering Challenges (#36-#74)
+#+DATE: <2019-12-29 Sun 19:55>
 #+TAGS: writeup, reverse-engineering, x86
 
+This is the fourth and final set of for my self-imposed challenge of completing
+at least fifty of the exercises on Dennis Yurichev's [[https://challenges.re][challenges.re]] by the end of
+the year. The previous set is available [[http:///jakob.space/challenges-re-writeups-3.html][here]].
+
+We'll actually be covering twenty challenges in this one. I'd been so busy with
+school that I forgot to make a post when I hit forty.
+
 * Challenge #36
 
 The description this time describes that this is "[a] well-known algorithm
@@ -86,7 +94,7 @@ definition of the Ackermann–Péter function.
 
 * Challenge #38
 
-Ah, fun. Another challenge provided as a binary.
+Fun. Another challenge provided as a binary.
 
 #+BEGIN_SRC prog
 jakob@Upsilon ~ $ sha256sum 17
@@ -164,8 +172,8 @@ to =stdout= is the current time.
 
 * Challenge #39
 
-The description for this challenge had me quite excited. "This program requires
-a password. Find it." Yes, I love crackmes!
+The description for this challenge got me excited. "This program requires a
+password. Find it."
 
 #+BEGIN_SRC prog
 jakob@Upsilon ~ $ sha256sum password2
@@ -565,8 +573,8 @@ void f(float *a, float *b, float *c)
 * Challenge #64
 
 I was swamped with preparing for finals this weekend, so I decided to skip
-challenge #64 in favor of something a bit more manageable. The question for this
-one is, "[a]n array of array[x][y] form is accessed here. Try to determine the
+challenge #63 in favor of something less arduous. The question for this one is,
+"[a]n array of array[x][y] form is accessed here. Try to determine the
 dimensions of the array, at least partially, by finding y."
 
 #+BEGIN_SRC c
@@ -580,6 +588,8 @@ The array has some number of rows each containing 15 elements.
 
 * Challenge #65
 
+The question here is the same as the previous challenge.
+
 #+BEGIN_SRC c
 int f(int *array, int x, int y, int z)
 {
@@ -591,6 +601,13 @@ Assuming an array of integers, the dimensions of the array are 15 x 20 x ...
 
 * Challenge #74
 
+I skipped way ahead this time because I was done with finals and knew that this
+was the last of the challenges I'd be doing this year. So I looked through what
+remained in search of something difficult, but interesting, and settled on this
+one.
+
+We're given a binary,
+
 #+BEGIN_SRC prog
 jakob@Epsilon ~ $ sha256sum challenge74
 6d2ac11d1e6200d6a2cca988189764b6acdb7811d24619e8e66f1796c8c27394  challenge74
@@ -598,11 +615,16 @@ jakob@Epsilon ~ $ file challenge74
 challenge74: ELF 64-bit LSB executable, x86-64, version 1 (SYSV), dynamically linked, interpreter /lib64/ld-linux-x86-64.so.2, for GNU/Linux 2.6.24, BuildID[sha1]=7fa3bd4aa738bced5aaccb161090818646e07704, stripped
 #+END_SRC
 
+as well as a few valid keys.
+
 #+BEGIN_SRC prog
 2Z7A7-EK270-TMHR4-BHC71-CEB52-HELL0-HELL0-EONP9
 2Z7A7-6I7R9-MZGO9-FDQJ3-JN0Q6-HELL0-HELL0-72KJ9
 #+END_SRC
 
+I took this as an opportunity to try out the [[https://github.com/radareorg/r2ghidra-dec][r2ghidra-dec]] plugin for Radare.
+Let's see how it does.
+
 #+BEGIN_SRC c
 // WARNING: Could not reconcile some variable overlaps
 // WARNING: [r2ghidra] Detected overlap for variable var_20h// WARNING: [r2ghidra] Failed to match type signed int64_t for variable var_10h to Decompiler type: Unknown type
@@ -661,6 +683,9 @@ undefined8 main(uint32_t argc, char **argv)
 }
 #+END_SRC
 
+When I saw this, I was blown away. Damn. The NSA did a great job with this.
+Here's my cleaned up version.
+
 #+BEGIN_SRC c
 #include <stdint.h>
 
@@ -695,30 +720,47 @@ int main(int argc, char **argv)
 }
 #+END_SRC
 
-- Removed iVar1, since that's just the stack canary.
+Aside from getting rid of temporary variables, I removed =iVar1= as it's no more
+than a stack canary, and I fixed up a few "errors" that the decompiler made. As
+an example, notice that strange assignment to =var_24h._0_4_=? Let's see what the
+disassembly says.
+
+#+BEGIN_SRC asm
+    pushq %rbp
+    movq %rsp, %rbp
+    subq $0x30, %rsp
+    movl %edi, var_24h ; argc
+    movq %rsi, var_30h ; argv
+#+END_SRC
+
+This is the only write to =var_24h=, so the line should have been =var_24h = argv=.
+For some reason, the decompiler saw this as assignment to a =struct= field. I
+ended up removing it anyway. Using 'argc' is clearer.
 
-# For var_24h:
-#
-# pushq %rbp
-# movq %rsp, %rbp
-# subq $0x30, %rsp
-# movl %edi, var_24h ; argc
-# movq %rsi, var_30h ; argv
-#
-# Ended up removing it anyway. Using 'argc' is clearer.
+There's also that odd =(void *)((int64_t)&var_24h + 4)=, but if we look at the
+disassembly,
 
-# leaq var_20h, %rdx
-# movq %rdx, %rsi
-# movq %rax, %rdi
-# callq fcn.00400bb5
+#+BEGIN_SRC asm
+    leaq var_20h, %rdx
+    movq %rdx, %rsi
+    movq %rax, %rdi
+    callq fcn.00400bb5
+    ...
+    leaq var_20h, %rax
+    movq %rax, %rdi
+    callq fcn.0040085e
+#+END_SRC
 
-# leaq var_20h, %rax
-# movq %rax, %rdi
-# callq fcn.0040085e
+So that should've just been =var_20h= in the decompilation. Regardless, I'm
+impressed. And I have to say, as a plugin, r2ghidra is really good. =pdg= takes a
+few seconds, but if you rename some variables with =afvn= and run it again, it
+spits out the updated version instantly, which makes me think that it's probably
+doing some sort of caching and quick substitution.
 
-We can tell already that the sixth and seventh components must be "HELL0-HELL0".
+Anyway, back to the challenge. We can tell from the decompilation already that
+the sixth and seventh components must be "HELL0-HELL0". It also has to contain
+eight components, delimited by '-', as we can see from =fcn_00400bb5=:
 
-# From fcn_00400bb5
 #+BEGIN_SRC c
 var_10h._0_4_ = 0;
 while ((int32_t)var_10h < 7) {
@@ -729,23 +771,27 @@ while ((int32_t)var_10h < 7) {
 }
 #+END_SRC
 
-# ---
+Here's the gist of the key verification algorithm:
 
-- =fcn_00400bb5= parses the key into a buffer (I renamed to =parse_key=)
-  - =charcode= function maps numerals to their numeric values ('0' becomes 0) and letters 'A' through 'Z' to 10-35
-  - buffer is written with 3 bytes per component
-    - I thought this was a decompiler mistake at first, but I checked the disassembly and it's legit.
-- =fcn_0040085e= enables features based on the parsed key (I renamed to =enable_features=)
-  - parsed buffer needs to start with 0xdeadbabe
-  - bytes 4 and 5 give a numerical year, 6 gives a numerical month, and 7 gives a numerical day.
-    - Sanity checks to ensure that day is between 1 and 31, that month is between 1 and 12, and that year is between 2016 and 2101.
-  - 7th bit of byte 8 enables feature A
-  - 1st bit of byte 9 enables feature B
-  - 2nd bit of byte 10 enables feature C
-  - 4th bit of byte 11 enables feature D
-  - 1st bit of byte 12 enables feature E
-  - One final check of the last 8 bytes against a checksum function
-checksum(0, parsed, 0x18)
+- =fcn_00400bb5= parses the key into a buffer (I renamed this to =parse_key=)
+  - Calls out to a =charcode= function which maps numerals to their numeric values
+    ('0' becomes 0) and letters 'A' through 'Z' to 10-35.
+  - The buffer is written with 3 bytes per component. I thought this was a
+    decompiler mistake at first, but I checked the disassembly and it really is
+    3 bytes per component. 24 bytes total.
+- =fcn_0040085e= does further verification and enables features based on the
+  parsed key (I renamed this to =enable_features=).
+  - The resultant parsed buffer needs to start with 0xdeadbabe.
+  - The 4th and 5th bytes give a numerical year, the 6th a numerical month, and
+    the 7th a numerical day.
+    - There's a sanity checks to ensure that the day is between 1 and 31, that
+      the month is between 1 and 12, and that the year is between 2016 and 2101.
+  - The 7th bit of byte 8 enables feature A
+  - The 1st bit of byte 9 enables feature B
+  - The 2nd bit of byte 10 enables feature C
+  - The 4th bit of byte 11 enables feature D
+  - The 1st bit of byte 12 enables feature E
+  - There's one final check of the last 8 bytes against a =checksum= function.
 
 #+BEGIN_SRC c
 #include <stdint.h>
@@ -778,9 +824,8 @@ uint64_t checksum(int64_t init, char *parsed, int64_t length)
 }
 #+END_SRC
 
-# ---
-
-From this, we can hack together a quick key verifier.
+I actually didn't realize that last part until I'd already hacked together a
+quick key verifier.
 
 #+BEGIN_SRC common-lisp
 (use-package :cl-utilities)
@@ -836,7 +881,7 @@ From this, we can hack together a quick key verifier.
 ;;  :FEATURE-B T :FEATURE-C T :FEATURE-D T :FEATURE-E T)
 #+END_SRC
 
-And verify our results.
+We can verify our results.
 
 #+BEGIN_SRC prog
 jakob@Epsilon ~ $ ./challenge74 "2Z7A7-EK270-TMHR4-BHC71-CEB52-HELL0-HELL0-EONP9"
@@ -861,26 +906,91 @@ Feature E: ON
 SN valid
 #+END_SRC
 
-# ---
+But, as I mentioned, I'd missed the checksum, so we'll need to deal with that in
+developing a keygen. What makes this so difficult is that the bytes of the
+checksum are incorporated in the checksum value. So, I thought this might be an
+opportunity to add something else to my toolbox: the [[https://en.wikipedia.org/wiki/Z3_Theorem_Prover][Z3 Theorem Prover]].
 
-Tried to brute force overnight, which brought me back to playing CTF, but it was
-sadly unfruitful.
+I'd never used it before, but it seems to show up in CTF writeups quite
+frequently. I did a bit of reading ([[https://jomo.tv/security/mrmcd-ctf-writeup-flag-checker][this]], [[https://ericpony.github.io/z3py-tutorial/guide-examples.htm][this]] and [[https://stackoverflow.com/questions/53726998/using-z3-where-constraint-depends-on-output-of-function][this]]) and put together this:
 
-# ---
+#+BEGIN_SRC python
+from z3 import *
 
-GDB's call functionality is godsend.
+s = Solver()
 
-(gdb) p (unsigned long long) $checksum(0, &{'\xff', '\xff', '\xff'}, 3)
-$14 = 18446742974197923840
+def checksum(init, key):
+    result = BitVecVal(~init, 64)
 
-# ---
+    for byte in key:
+        result ^= ZeroExt(56, byte)
+        for i in range(8):
+            result = (result >> 1 & 0x7fffffffffffffff) ^ (0x42f0e1eb0badbad0 * (result & 1))
 
-Z3 https://jomo.tv/security/mrmcd-ctf-writeup-flag-checker
-https://ericpony.github.io/z3py-tutorial/guide-examples.htm
-https://stackoverflow.com/questions/53726998/using-z3-where-constraint-depends-on-output-of-function
+    result = ~result
 
-Right shift was giving me a hard time (not prepending with zeroes) which you can
-see from the & 0x7fffffffffffffff.
+    return result
+
+def unpack(word):
+    result = BitVecVal(0, 64)
+    result |= ZeroExt(56, word[0])
+    result |= ZeroExt(56, word[1]) << 8
+    result |= ZeroExt(56, word[2]) << 16
+    result |= ZeroExt(56, word[3]) << 24
+    result |= ZeroExt(56, word[4]) << 32
+    result |= ZeroExt(56, word[5]) << 40
+    result |= ZeroExt(56, word[6]) << 48
+    result |= ZeroExt(56, word[7]) << 56
+    return result
+
+key = [BitVec("bv{}".format(i), 8) for i in range(24)]
+
+FEATURE_A = False
+FEATURE_B = False
+FEATURE_C = False
+FEATURE_D = False
+FEATURE_E = False
+
+s.add(key[0] == 222)
+s.add(key[1] == 173)
+s.add(key[2] == 186)
+s.add(key[3] == 190)
+s.add(key[4] == ((2019 & 0xff00) >> 8))
+s.add(key[5] == 2019 & 0x00ff)
+s.add(key[6] == 12)
+s.add(key[7] == 25)
+s.add(key[8] & 0b100000 == (1 if FEATURE_A else 0))
+s.add(key[9] & 0b000001 == (1 if FEATURE_B else 0))
+s.add(key[10] & 0b000010 == (1 if FEATURE_C else 0))
+s.add(key[11] & 0b001000 == (1 if FEATURE_D else 0))
+s.add(key[12] & 0b000001 == (1 if FEATURE_E else 0))
+s.add(key[15] == 153)
+s.add(key[16] == 95)
+s.add(key[17] == 15)
+s.add(key[18] == 153)
+s.add(key[19] == 95)
+s.add(key[20] == 15)
+
+s.add(unpack(key[16:]) == checksum(0, key))
+
+s.check()
+print(s.model())
+#+END_SRC
+
+Accurately translating the checksum function was a pain in the tuckus. The right
+shift was giving me a hard time since the Z3 right shift doesn't prepend with
+zeroes. The =& 0x7fffffffffffffff= is my attempt at dealing with that.
+
+As an aside, I just want to say that GDB's =call= functionality is godsend. It
+made verifying my translation so much easier.
+
+#+BEGIN_SRC prog
+(gdb) p (unsigned long long) $checksum(0, &{'\xff', '\xff', '\xff'}, 3)
+$14 = 18446742974197923840
+#+END_SRC
+
+So, I let this run overnight, which brought me back to when I was more active
+with CTF and would let my half-complete solutions run while I slept.
 
 #+BEGIN_SRC prog
 jakob@Epsilon ~ $ python solver.py 
@@ -910,17 +1020,41 @@ jakob@Epsilon ~ $ python solver.py
  bv0 = 222]
 #+END_SRC
 
+This was waiting for me when I got back from the gym the next morning.
+
 #+BEGIN_SRC common-lisp
-(string-join (mapcar #'ahash-component-inverse (mapcar #'triplet-to-number '((222 173 186) (190 0 27) (12 24 13) (170 108 208) (240 18 20) (153 95 15) (153 95 15) (216 196 130)))) "-")
+(string-join
+ (mapcar #'ahash-component-inverse
+         (mapcar #'triplet-to-number '((222 173 186)
+                                       (190 0 27)
+                                       (12 24 13)
+                                       (170 108 208)
+                                       (240 18 20)
+                                       (153 95 15)
+                                       (153 95 15)
+                                       (216 196 130))))
+ "-")
 #+END_SRC
 
 #+BEGIN_SRC prog
+CL-USER> (string-join
+ (mapcar #'ahash-component-inverse
+         (mapcar #'triplet-to-number '((222 173 186)
+                                       (190 0 27)
+                                       (12 24 13)
+                                       (170 108 208)
+                                       (240 18 20)
+                                       (153 95 15)
+                                       (153 95 15)
+                                       (216 196 130))))
+ "-")
+"2Z7A7-AHX11-S4EI0-6LR48-K37S0-HELL0-HELL0-KPO35"
 CL-USER> (key-attributes "2Z7A7-AHX11-S4EI0-6LR48-K37S0-HELL0-HELL0-KPO35")
 (:VALID NIL :EXPIRY-YEAR 27 :EXPIRY-MONTH 12 :EXPIRY-DAY 24 :FEATURE-A NIL
  :FEATURE-B NIL :FEATURE-C NIL :FEATURE-D NIL :FEATURE-E NIL)
 #+END_SRC
 
-OH MY GOD
+Oh no...
 
 #+BEGIN_SRC python
 ...
@@ -932,7 +1066,7 @@ That should've been =s.add(key[4] == ((2019 & 0xff00) >> 8))=...
 
 ;-;
 
-Let's try this again...
+Let's try this again.
 
 #+BEGIN_SRC prog
 jakob@Epsilon ~ $ python solver.py 
@@ -962,8 +1096,19 @@ jakob@Epsilon ~ $ python solver.py
  bv0 = 222]
 #+END_SRC
 
+This time it actually ran for a whole two days.
+
 #+BEGIN_SRC prog
-CL-USER> (mapcar #'hash-component-inverse (mapcar #'triplet-to-number '((222 173 186) (190 7 227) (12 25 140) (168 12 183) (184 39 124) (153 95 15) (153 95 15) (204 80 133))))
+CL-USER> (mapcar #'hash-component-inverse
+        (mapcar #'triplet-to-number
+                '((222 173 186)
+                  (190 7 227)
+                  (12 25 140)
+                  (168 12 183)
+                  (184 39 124)
+                  (153 95 15)
+                  (153 95 15)
+                  (204 80 133))))
 ("2Z7A7" "YFWU8" "CGSG5" "CF457" "K9EU4" "HELL0" "HELL0" "OH975")
 CL-USER> (key-attributes "2Z7A7-YFWU8-CGSG5-CF457-K9EU4-HELL0-HELL0-OH975")
 (:VALID T :EXPIRY-YEAR 2019 :EXPIRY-MONTH 12 :EXPIRY-DAY 25 :FEATURE-A NIL
@@ -983,14 +1128,23 @@ Feature E: OFF
 SN valid
 #+END_SRC
 
-# ---
+There we go. A working keygen! (Provided you're willing to wait).
 
-I have to say, r2ghidra is really fucking good. =pdg= takes a while, but if you
-rename some variables with =afvn= and run it again, it spits out the updated
-version instantly (probably doing some sort of caching/quick substitution).
+* An End-of-Year Reflection
 
-# ---
+This was fun, but I think in planning this out, I should have preferred depth
+over breadth, like getting through some of the challenges on [[http://reversing.kr/index.php][reversing.kr]]. The
+challenges I got the most out of were the ones I had to spend more than a day
+reversing. Another thing that made regret the choice of Dennis Yurichev's
+challenges is the significance of context in reverse engineering. Most of these
+challenges give little more than a disassembly. There are exceptions --
+challenge #33, for example, was one I was able to solve because the description
+said that it was a cryptographic function. But for the most part, I think being
+able to see the "big picture" would have been a more realistic way to practice
+my reverse engineering chops.
 
-# End-of-year reflection: Context is super important for making sense of assembly code.
-# Case in point: crypto challenges like #33
-# Idea to toy with: A monthly crackme, hints given out every week and solutions posted (also, the challenges won't be painfully abstract)
+One idea I've been toying with is putting out a crackme on a monthly basis.
+Infrequent enough that it wouldn't be overwhelming, and I'd be able to make it a
+sizeable challenge. I'd be able to give out hints every week, and post the
+solution at the end of the month. Actually, I may do this through the [[https://ctf.cs.umass.edu/][wargames]]
+site we're putting together at university. Stay tuned!