Cyber Skyline has launched a new lottery system, but there is a flaw hidden within. Can you uncover the issues and hit the jackpot?
Q1 (5 pts) - Where can you find the backend source code for the API? Enter the path.
/source
Q2 (5 pts) - What programming language is the backend API written in?
Java
Q3 (5 pts) - What PRNG implementation is the application using? Enter the full import path, like xxx.xxx.xxx.
java.util.Random
Q4 (5 pts) - What is the algorithm used to generate the pseudo random numbers? Enter the three letter acronym.
LCG
Q5 (10 pts) - What is the minimum number of ticket purchases needed to reliably recover the internal seed?
2
Q6 (10 pts) - How many individual bits (not values) must be brute forced when reconstructing the internal seed? Enter the integer value.
16
Q7 (10 pts) - What is the value of the multiplier in this algorithm’s implementation? Enter as an integer.
25214903917
Q8 (10 pts) - What is the value of the mask in this algorithm’s implementation? Enter as an integer.
281474976710655
Q9 (10 pts) - What is the value of the increment in this algorithm’s implementation? Enter as an integer.
11
Q10 (20 pts) - What is the flag shown on the site after redeeming a ticket that matches the winning numbers?
SKY-DMEX-8392
I started by opening the page in another tab.
The site exposed the algorithm at /source.

The answers to Q1 and Q2 were both available there.
The API source was under /source, and it was clearly written in Java.

For Q3, I reviewed what a PRNG was so I could identify the concept correctly.

I then checked the source files.
Ticket.java showed the answer directly.

Q4 — I searched for the algorithm behind java.util.Random.

Q5 — I reviewed how Java’s random number generator stores and updates its internal seed.

It uses a 48-bit integer, based on this code:
public static int[] drawNumbers(String sessionId) {
int[] numbers = new int[6]; // ← creates space for 6 numbers
Random rand = getRandom(sessionId);
for (int I = 0; I < 6; I++) { // ← runs 6 times
numbers[I] = rand.nextInt(100);
}
return numbers;
}
Every time a ticket is purchased, 6 outputs are generated.
If two tickets are purchased, then 12 outputs are generated, which makes brute-forcing the seed easier. That is why 2 tickets is the minimum answer.
A Java integer is 32 bits, so 48 - 32 = 16, meaning 16 bits still need to be brute-forced.
Q6 — I reviewed the LCG values used by Java’s random implementation.
That gave me the values for Q7 through Q9.

I used AI to verify the final reconstruction step once I had identified the seed behavior and generation logic.
It had me run a curl command to keep the session cookie active.
curl -c jar.txt -b jar.txt \
-X POST \
-H "Content-Type: application/json" \
https://000dddd903ab3d293a15db76698cd30f-jackpot.web.cityinthe.cloud/buy \
-d '{"numbers":null}'
It gave me these two scripts
The first script purchase a few tickets and saves the uids and ticket number
import requests
from z3 import BitVec, BitVecVal, Solver, LShR, URem, sat
BASE = "https://000dddd903ab3d293a15db76698cd30f-jackpot.web.cityinthe.cloud"
A = 25214903917
C = 11
MASK = (1 << 48) - 1
sess = requests.Session()
def buy_auto():
r = sess.post(
BASE + "/buy",
json={"numbers": None},
timeout=10,
)
r.raise_for_status()
j = r.json()["ticket"]
return j["numbers"], int(j["u`uid`"])
def step_expr(seed):
return (seed * BitVecVal(A, 64) + BitVecVal(C, 64)) & BitVecVal(MASK, 64)
def recover_seed(observed):
"""
observed = [
([n1,n2,n3,n4,n5,n6], u`uid`1),
([m1,m2,m3,m4,m5,m6], u`uid`2),
...
]
"""
s0 = BitVec("s0", 64)
solver = Solver()
mask_bv = BitVecVal(MASK, 64)
solver.add((s0 & ~mask_bv) == 0) # ensure only 48 bits are used
cur = s0
for nums, u`uid`_val in observed:
# 6 calls to nextInt(100)
for n in nums:
cur = step_expr(cur)
bits31 = LShR(cur, 17) # next(31)
solver.add(URem(bits31, 100) == n)
# 1 call to nextInt() for UUID
cur = step_expr(cur)
out32 = LShR(cur, 16) # next(32)
solver.add(out32 == u`uid`_val)
if solver.check() != sat:
raise RuntimeError("No satisfying seed found. Collect one more auto ticket.")
model = solver.model()
return model[s0].as_long()
def step(seed):
return (seed * A + C) & MASK
def next32(seed):
seed = step(seed)
return seed, seed >> 16
def next31(seed):
seed = step(seed)
return seed, seed >> 17
def next_int_100(seed):
# good enough here; rejection case is negligible
seed, bits = next31(seed)
return seed, bits % 100
def advance_past_observed(seed, observed):
cur = seed
for nums, u`uid`_val in observed:
for _ in nums:
cur, _ = next_int_100(cur)
cur, _ = next32(cur)
return cur
def predict_next_redeem_winning_numbers(seed_after_observed):
cur = seed_after_observed
# Buying a manual ticket consumes one nextInt() for its UUID
cur, future_u`uid` = next32(cur)
winning = []
for _ in range(6):
cur, v = next_int_100(cur)
winning.append(v)
return future_u`uid`, winning
def main():
observed = []
for I in range(3):
nums, u`uid`_val = buy_auto()
observed.append((nums, u`uid`_val))
print(f"[+] auto ticket {I+1}: numbers={nums}, u`uid`={u`uid`_val}")
seed0 = recover_seed(observed)
print(f"[+] recovered initial state: {seed0}")
cur = advance_past_observed(seed0, observed)
future_u`uid`, winning = predict_next_redeem_winning_numbers(cur)
print(f"[+] predicted manual-ticket UUID step consumed output: {future_u`uid`}")
print(f"[+] predicted next redeem winning numbers: {winning}")
if __name__ == "__main__":
main()
It solves for the next winning numbers

The next script is the same but added on the solver
import requests
from z3 import BitVec, BitVecVal, Solver, LShR, URem, sat
BASE = "https://000dddd903ab3d293a15db76698cd30f-jackpot.web.cityinthe.cloud"
A = 25214903917
C = 11
MASK = (1 << 48) - 1
sess = requests.Session()
def buy_auto():
r = sess.post(BASE + "/buy", json={"numbers": None}, timeout=10)
r.raise_for_status()
j = r.json()["ticket"]
return j["numbers"], int(j["u`uid`"])
def buy_manual(nums):
r = sess.post(BASE + "/buy", json={"numbers": nums}, timeout=10)
r.raise_for_status()
return r.json()["ticket"]
def redeem(u`uid`_val):
r = sess.post(BASE + "/redeem", json={"u`uid`": str(u`uid`_val)}, timeout=10)
r.raise_for_status()
return r.json()
def step_expr(seed):
return (seed * BitVecVal(A, 64) + BitVecVal(C, 64)) & BitVecVal(MASK, 64)
def recover_seed(observed):
s0 = BitVec("s0", 64)
solver = Solver()
mask_bv = BitVecVal(MASK, 64)
solver.add((s0 & ~mask_bv) == 0)
cur = s0
for nums, u`uid`_val in observed:
for n in nums:
cur = step_expr(cur)
bits31 = LShR(cur, 17)
solver.add(URem(bits31, 100) == n)
cur = step_expr(cur)
out32 = LShR(cur, 16)
solver.add(out32 == u`uid`_val)
if solver.check() != sat:
raise RuntimeError("No satisfying seed found. Try collecting 1 more auto ticket.")
return solver.model()[s0].as_long()
def step(seed):
return (seed * A + C) & MASK
def next32(seed):
seed = step(seed)
return seed, seed >> 16
def next31(seed):
seed = step(seed)
return seed, seed >> 17
def next_int_100(seed):
seed, bits = next31(seed)
return seed, bits % 100
def advance_past_observed(seed, observed):
cur = seed
for nums, _u`uid` in observed:
for _ in nums:
cur, _ = next_int_100(cur)
cur, _ = next32(cur)
return cur
def predict_next_redeem_numbers(seed_after_observed):
cur = seed_after_observed
# buying the manual ticket consumes one nextInt() for UUID
cur, manual_u`uid`_output = next32(cur)
winning = []
for _ in range(6):
cur, v = next_int_100(cur)
winning.append(v)
return manual_u`uid`_output, winning
def main():
observed = []
for I in range(3):
nums, u`uid`_val = buy_auto()
observed.append((nums, u`uid`_val))
print(f"[+] auto ticket {I+1}: numbers={nums}, u`uid`={u`uid`_val}")
seed0 = recover_seed(observed)
print(f"[+] recovered initial state: {seed0}")
cur = advance_past_observed(seed0, observed)
predicted_u`uid`_output, winning = predict_next_redeem_numbers(cur)
print(f"[+] predicted next winning numbers: {winning}")
jackpot_ticket = buy_manual(winning)
print(f"[+] bought predicted ticket: {jackpot_ticket}")
result = redeem(jackpot_ticket["u`uid`"])
print("[+] redeem response:")
print(result)
if result.get("result") == "JACKPOT!!!" and "flag" in result:
print("\nFLAG:", result["flag"])
else:
print("\n[-] No flag returned.")
print(" winning from server:", result.get("winning"))
if __name__ == "__main__":
main()
It automatically solved and got the flag
