rps-casino
6 minutes to read
We are given the Python source code of the server:
#!/usr/local/bin/python
import os
from Crypto.Util.number import bytes_to_long
def LFSR():
state = bytes_to_long(os.urandom(8))
while 1:
yield state & 0xf
for i in range(4):
bit = (state ^ (state >> 1) ^ (state >> 3) ^ (state >> 4)) & 1
state = (state >> 1) | (bit << 63)
rng = LFSR()
n = 56
print(f"Let's play rock-paper-scissors! We'll give you {n} free games")
print("but after that you'll have to beat me 50 times in a row to win. Good luck!")
rps = ["rock", "paper", "scissors", "rock"]
nums = []
for i in range(n):
choice = next(rng) % 3
inp = input("Choose rock, paper, or scissors: ")
if inp not in rps:
print("Invalid choice")
exit(0)
if inp == rps[choice]:
print("Tie!")
elif rps.index(inp, 1) - 1 == choice:
print("You win!")
else:
print("You lose!")
for i in range(50):
choice = next(rng) % 3
inp = input("Choose rock, paper, or scissors: ")
if inp not in rps:
print("Invalid choice")
break
if rps.index(inp, 1) - 1 != choice:
print("Better luck next time!")
break
else:
print("You win!")
else:
print(open("flag.txt").read())
Source code analysis
The server implements a Rock-Paper-Scissors game using a Linear Feedback Shift Register (LFSR) as a Pseudo-Random Number Generator (PRNG). We are given 56 free rounds and then we need to win 50 times in a row to get the flag.
Therefore, we will need to recover the original state of the LFSR from the first 56 rounds, in order to successfully generate future rounds and win the game.
LFSR
The LFSR implementation is this one:
def LFSR():
state = bytes_to_long(os.urandom(8))
while 1:
yield state & 0xf
for i in range(4):
bit = (state ^ (state >> 1) ^ (state >> 3) ^ (state >> 4)) & 1
state = (state >> 1) | (bit << 63)
The state is composed of 64 bits (8 bytes). We can express this as binary variables $[x_{63}, \dots, x_0]$ in $\mathbb{F}_2$. In this field, XOR is the addition operation.
On each round of the LFSR, 4 internal rounds are processed in a for loop. Here, the new bit $x_{63} = x_0 + x_1 + x_3 + x_4$ and then the rest of bits take the value of the bit at its left: $x_i = x_{i + 1}$ for $0 \leqslant i < 63$. This operation can be expressed in matrix form:
$$ \begin{pmatrix} 0 & \dots & 0 & 1 & 1 & 0 & 1 & 1 \\ 1 & & & & & & & \\ & \ddots & & & & & & \\ & & 1 & & & & & \\ & & & 1 & & & & \\ & & & & 1 & & & \\ & & & & & 1 & & \\ & & & & & & 1 & \\ & & & & & & & 1 \end{pmatrix} $$
With this matrix $M$, we can perform one internal iteration:
$$ M \cdot \begin{pmatrix} x_{63} \\ x_{62} \\ x_{61} \\ \vdots \\ x_2 \\ x_1 \\ x_0 \end{pmatrix} = \begin{pmatrix} x_0 + x_1 + x_3 + x_4 \\ x_{63} \\ x_{62} \\ \vdots \\ x_3 \\ x_2 \\ x_1 \end{pmatrix} $$
As a result, an LFSR round is the result of 4 internal rounds, which translates into using $M^4$:
$$ M^4 \cdot \begin{pmatrix} x_{63} \\ x_{62} \\ x_{61} \\ \vdots \\ x_2 \\ x_1 \\ x_0 \end{pmatrix} = \begin{pmatrix} x_0 + x_1 + x_3 + x_4 \\ x_1 + x_2 + x_4 + x_5 \\ x_2 + x_3 + x_5 + x_6 \\ x_3 + x_4 + x_6 + x_7 \\ x_{60} \\ x_{59} \\ \vdots \\ x_6 \\ x_5 \\ x_4 \end{pmatrix} $$
The LFSR round returns the 4 bits at the right (that is, positions $x_3$ through $x_0$ of the state). However, the Rock-Paper-Scissors game reduces $\mod{3}$ in order to make a choice:
for i in range(n):
choice = next(rng) % 3
This is a problem if we want to solve this challenge using Linear Algebra, because we need to change variables from $\mathbb{F}_2$ to $\mathbb{Z}/16\mathbb{Z}$ (which is not a problem) and then to $\mathbb{Z}/3\mathbb{Z}$ (which is a problem).
The issue is that all LFSR computations are done in $\mathbb{F}_2$. While the output is a 4-bit number ($\mathbb{Z}/16\mathbb{Z}$), we can still consider individual bits and continue working in $\mathbb{F}_2$. Nevertheless, the server is reducing the 4-bit number $\mod{3}$. Therefore, no matter how we define the variables that any algebraic approach will fail.
z3 to the rescue
After wasting a lot of time trying to understand why SageMath was unable to solve this problem, I tried using z3, which is an SMT solver that does not rely on Linear Algebra.
The idea of using z3 is that we can define the original state as a bit-vector of length 64 and perform LFSR symbolic computations with z3. After that, we add some constraints of the expected LFSR outputs $\mod{3}$ and we pray for a solution.
Implementation
Implementing a solution in z3 is quite simple because we can reuse most of the original code. However, we need to be careful with the use of some operations. For instance, we need to change >> by LShR to force a logical shift instead of an arithmetic shift:
def z3_LFSR(state):
while 1:
yield state & 0xf
for _ in range(4):
bit = (state ^ LShR(state, 1) ^ LShR(state, 3) ^ LShR(state, 4)) & 1
state = LShR(state, 1) | (bit << 63)
Then, we just need to take the values from the server and add the constraints:
state = BitVec('s', 64)
lfsr = z3_LFSR(state)
s = Solver()
for r in range(56):
res = play()
sym = next(lfsr) % 3
s.add(sym == res)
Just to clarify, play is a helper function:
io = get_process()
def play(choice: bytes = b'rock') -> int:
io.sendlineafter(b'Choose rock, paper, or scissors: ', choice)
res = io.recvline()
if b'Tie' in res:
return 0
elif b'lose' in res:
return 1
elif b'win' in res:
return 2
At this point, we can see if the solver has found a solution and, if so, take the original state:
if s.check() == sat:
model = s.model()
_state = int(model[state].as_long())
else:
exit(1)
Finally, we redo the 56 initial rounds and play the next 50 rounds knowing which choice the server is going to make, so we can win the game:
for _ in range(56):
next(lfsr)
for _ in range(50):
play([b'rock', b'paper', b'scissors'][(next(lfsr) + 1) % 3])
Flag
If we run the script, we will capture the flag:
$ python3 solve.py mc.ax 31234
[+] Opening connection to mc.ax on port 31234: Done
[+] dice{wow_u_must_be_extremely_lucky_91ff5a34}
[*] Closed connection to mc.ax port 31234
The full script can be found in here: solve.py.