## Challenge
> Look at that cute fox over there!!!> > http://www.talesshop.com/?page=product&query=fox> > Please Answer My Question!
Executing the program only outputs this rather useless message:
```Welcome To Kornewbie CTF, CTF Challengers!Before You Solve This Problem, Please Watch This Video.Video Link : https://www.youtube.com/watch?v=jofNR_WkoCEPlease Answer My Question, What Does Fox Say?```
## Binary analysis
The binary contains multiple code paths in the `main` function which areselected at random. However, only one of those code paths is relevant, becauseit's the only code path which checks for a flag *and* prints the`KorNewbie{%s}` string:
```c/* somewhere in main */buf[0] = 0;*(_DWORD *)&buf[1] = 0;*(_DWORD *)&buf[5] = 0;*(_DWORD *)&buf[9] = 0;*(_DWORD *)&buf[13] = 0;scanf("%s", buf);if(strlen(buf) == 16 && compute_hash(buf, 0x7C35D9A3) == 0xF92AC34) {	if(buf[3] == '_' && buf[7] == '_' && buf[12] == '_') {		if(buf[0] >= 'A'				&& buf[0] <= 'Z'				&& buf[1] >= 'A'				&& buf[1] <= 'Z'				&& buf[2] >= 'A'				&& buf[2] <= 'Z'				&& buf[4] >= 'A'				&& buf[4] <= 'Z'				&& buf[5] >= 'A'				&& buf[5] <= 'Z'				&& buf[6] >= 'A'				&& buf[6] <= 'Z'				&& buf[8] >= 'A'				&& buf[8] <= 'Z'				&& buf[9] >= 'A'				&& buf[9] <= 'Z'				&& buf[10] >= 'A'				&& buf[10] <= 'Z'				&& buf[11] >= 'A'				&& buf[11] <= 'Z'				&& buf[13] >= 'A'				&& buf[13] <= 'Z'				&& buf[14] >= 'A'				&& buf[14] <= 'Z'				&& buf[15] >= 'A'				&& buf[15] <= 'Z') {			printf("Good! Check The Flag!\n");			printf("KorNewbie{%s}\n", buf);		}	}}```
There is an input for a single word (`scanf`). Afterwards, the length ischecked (16 characters) and a hash is computed. If the hash matches theexpected hash, the structure of the string is checked:
- only uppercase letters- `_` at positions 3, 7, and 12
Therefore, the string we are looking for is supposed to have this structure:```AAA_AAA_AAAA_AAA```
The hash function itself looks like this:
```cint compute_hash(const char *str, int magic){	unsigned int i;	int hash = 0;
	for(i = 0; i < strlen(str); i++)		hash = magic ^ ((str[i] | 0x20) + __ROR4__(hash, 8));	return crt_check(1, hash);}```
(The `crt_check` function in the hash function just performs some runtimechecks and then returns the second argument, this function is not interestingfor us.)
This function computes a hash using the magic constant. Interestingly enough,this hash function was taken from a [real world malware sample](https://www.dailysecu.com/bbs/download.php?table=bbs_10&savefilename=bbs_10_2979_1.pdf&filename=%EC%83%88%EB%A1%9C%EC%9A%B4%20%EC%A4%91%EA%B5%AD%20%EC%82%AC%EC%9D%B4%EB%B2%84%20%EA%B3%B5%EA%B2%A9%20%EA%B7%B8%EB%A3%B9%20APT41%20%EC%84%B8%EB%B6%80%20%EB%82%B4%EC%9A%A9%20%EB%B3%B4%EA%B3%A0%EC%84%9C-%ED%8C%8C%EC%9D%B4%EC%96%B4%EC%95%84%EC%9D%B4%202019.pdf).Unfortunately the published analysis of that malware sample does not contain auseful analysis of the hash function itself.
## Basic Idea
The only way to solve this challenge is by breaking the hash function. A simplebrute force attack is way too slow and even with a dictionary the search spaceis still too big. The solution is to use SMT with a powerful SMT solver, whichdeals with all the complexity for us. We only have to encode the problem inSMT.
## Encode the problem in SMT
Encoding the problem in SMT is rather simple: just unroll the loop of the hashalgorithm and add the constraints on the input from the main function. We usethe theory of bit vectors to encode our 32bit variables and operations.
### Definitions
First define constants for the lower and upper limit of the input:
```common-lisp(declare-const lower (_ BitVec 32))(assert (= lower #x00000041))	; A(declare-const upper (_ BitVec 32))(assert (= upper #x0000005A))	; Z```
We also need the magic constant from the main function as well as the constantthat is or'd to the input:
```common-lisp(declare-const magic (_ BitVec 32))(assert (= magic #x7C35D9A3))
(declare-const cons (_ BitVec 32))(assert (= cons #x00000020))```
### Loop Unrolling: First Iteration
Now we need to translate the hash function itself. In SMT everything has to beunrolled, and variables from the original program have to be in SSA form. Thismeans we need one set of variables for every iteration of the hash function.
Let's start with the first iteration. The `hash` variable is initialized with`0`. We call this `out0`:
```common-lisp(declare-const out0 (_ BitVec 32))(assert (= out0 #x00000000))```
Now apply the constraints from the main function on the first character of theinput (only upper case letters):
```common-lisp(declare-const i0 (_ BitVec 32))(assert (and (bvule i0 upper) (bvuge i0 lower)))```
Then, we define a temporary variable `t0 = str[0] | 0x20`:
```common-lisp(declare-const t0 (_ BitVec 32))(assert (= t0 (bvor i0 cons)))```
This variable is XOR'd with the magic constant, which results in the `hash`value after the first iteration. Since the previous hash value is `0`, we canignore the ROT part here:
```common-lisp(declare-const out1 (_ BitVec 32))(assert (= out1 (bvxor t0 magic)))```
### Loop Unrolling: Second Iteration
Now we have to unroll the second iteration. Again, we start with theconstraints on the input:
```common-lisp(declare-const i1 (_ BitVec 32))(assert (and (bvule i1 upper) (bvuge i1 lower)))```
Then, we define the temporary variable `it1 = str[1] | 0x20`:
```common-lisp(declare-const it1 (_ BitVec 32))(assert (= it1 (bvor i1 cons)))```
This time we have to add the rotated old hash value:
```common-lisp(declare-const rot1 (_ BitVec 32))(assert (= rot1 ((_ rotate_right 8) out1)))(declare-const prexor1 (_ BitVec 32))(assert (= prexor1 (bvadd it1 rot1)))```
The XOR with the magic constants results in the `hash` value after the second iteration:
```common-lisp(declare-const out2 (_ BitVec 32))(assert (= out2 (bvxor prexor1 magic)))```
### Loop Unrolling: Third .. Sixteenth Iteration
Unrolling the remaining loop iterations works exactly in the same way. However,there is one special case with the checks for `_` characters. At thosepositions, the input is asserted to be `_` instead of the constraint for uppercase letters:
```common-lisp(declare-const i3 (_ BitVec 32))(assert (= i3 #x0000005f)) ; _```
### Check the Hash
After unrolling all loop iterations, the final hash value `out16` is checked bycomparing it to our expected hash:
```common-lisp(assert (= out16 #x0F92AC34))```
## Compute the Flag
A solution can now be computed by calling an SMT solver:```boolector -m -x fox.smt2```
The SMT solver now checks if there is a "satisfying assignment", which means ittries to find an input which produces the hash we're interested in. It then outputs the variable assignment, and we get this result:
```KorNewbie{RRV_NQN_UAAO_KLE}```
Unfortunately, we cannot submit this flag because the online system tells us it's "incorrect".
## Guessing the Flag
So … we computed a valid flag, but we can't submit it because the system tellsus it's invalid. This is where the real fun starts. We now have to *guess* theflag.
We can choose letters and e.g. specify that the word `FOX` has to appear.Unfortunately we can still get lots of "incorrect" flags, even if we forcewords. After a few hours of playing this "guessing game", I guessed that theflag might start with `THE_FOX_SAYS_`, since the program asks us `What Does FoxSay?`.
Encoding such a constraint is rather simple, just force the input to specific values:
```common-lisp; guess the first few words(assert (and (= i0 #x00000054) (= i1 #x00000048) (= i2 #x00000045))) ; THE(assert (and (= i4 #x00000046) (= i5 #x0000004F) (= i6 #x00000058))) ; FOX(assert (and (= i8 #x00000053) (= i9 #x00000041) (= i10 #x00000059) (= i11 #x00000053))) ; SAYS```
Now, with *this* guess we finally get our flag that can be submitted:
```KorNewbie{THE_FOX_SAYS_SUA}```
[Final SMT file](https://www.sigflag.at/assets/posts/foxyfox/fox.smt2)
## Unique Solution
Challenges without unique solutions suck. After we already guessed thesolution, the challenge was "fixed" with the following change:
```cref[0] = 0;ref[1] = 0x1C;ref[2] = 0x11;ref[3] = 0xB;ref[4] = 0x12;ref[5] = 0x1B;ref[6] = 0xC;ref[7] = 0xB;ref[8] = 7;ref[9] = 0x15;ref[10] = 0xD;ref[11] = 7;ref[12] = 0xB;ref[13] = 7;ref[14] = 1;ref[15] = 0x15;
if(...) { /* this is the long if from before */	ok = 1;	for(i = 0; i < strlen(buf); i++) {		if((buf[i] ^ buf[0]) != ref[i])			ok = 0;	}	if(ok == 1) {		printf("Good! Check The Flag!\n");		printf("KorNewbie{%s}\n", buf);	}}```
This change is supposed to make the solution unique.
In SMT, this contstraint looks like this:
```common-lisp(assert (= (bvxor i0 i0) #x00000000))(assert (= (bvxor i1 i0) #x0000001C))(assert (= (bvxor i2 i0) #x00000011))(assert (= (bvxor i3 i0) #x0000000B))(assert (= (bvxor i4 i0) #x00000012))(assert (= (bvxor i5 i0) #x0000001B))(assert (= (bvxor i6 i0) #x0000000C))(assert (= (bvxor i7 i0) #x0000000B))(assert (= (bvxor i8 i0) #x00000007))(assert (= (bvxor i9 i0) #x00000015))(assert (= (bvxor i10 i0) #x0000000D))(assert (= (bvxor i11 i0) #x00000007))(assert (= (bvxor i12 i0) #x0000000B))(assert (= (bvxor i13 i0) #x00000007))(assert (= (bvxor i14 i0) #x00000001))(assert (= (bvxor i15 i0) #x00000015))```
If we ask the SMT solver for a model, we directly get the "correct" flag.
To convince ourselves that the solution is now really unique, we can check ifthere is another solution by "blacklisting" the previous solution:
```common-lisp; blacklist 'THE_FOX_SAYS_SUA'(assert (not (and	(= i0 #x00000054)	(= i1 #x00000048)	(= i2 #x00000045)	(= i3 #x0000005f)	(= i4 #x00000046)	(= i5 #x0000004f)	(= i6 #x00000058)	(= i7 #x0000005f)	(= i8 #x00000053)	(= i9 #x00000041)	(= i10 #x00000059)	(= i11 #x00000053)	(= i12 #x0000005f)	(= i13 #x00000053)	(= i14 #x00000055)	(= i15 #x00000041))))```
Now the SMT solver tells us `unsat`, which means there is indeed only one solution.
## Useful Links
- [boolector](https://boolector.github.io/): efficient SMT solver- [smtlib2](http://smtlib.cs.uiowa.edu/): description of the smtlib2 language