rps-casino
6 minutos de lectura
Se nos proporciona el código fuente en Python del servidor:
#!/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())
Análisis del código fuente
El servidor implementa un juego de Piedra-Papel-Tijera utilizando un Linear Feedback Shift Register (LFSR) como un generador de números pseudo-aleatorios (PRNG). Nos dan 56 rondas gratuitas y luego necesitamos ganar 50 veces seguidas para obtener la flag.
Por lo tanto, necesitaremos recuperar el estado original del LFSR a partir de las primeras 56 rondas, para generar con éxito futuras rondas y ganar el juego.
LFSR
La implementación del LFSR es esta:
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)
El estado está compuesto por 64 bits (8 bytes). Podemos expresar esto como variables binarias $[x_{63}, \dots, x_0]$ en $\mathbb{F}_2$. En este campo, Xor es la operación de adición.
En cada ronda del LFSR, se procesan 4 rondas internas en un bucle for
. Aquí, se calcula el nuevo bit $x_{63} = x_0 + x_1 + x_3 + x_4$ y luego el resto de bits toma el valor de su izquierda: $x_i = x_{i + 1}$ para $0 \leqslant i < 63$. Esta operación se puede expresar en forma de matriz:
$$ \begin{pmatrix} 0 & \dots & 0 & 1 & 1 & 0 & 1 & 1 \\ 1 & & & & & & & \\ & \ddots & & & & & & \\ & & 1 & & & & & \\ & & & 1 & & & & \\ & & & & 1 & & & \\ & & & & & 1 & & \\ & & & & & & 1 & \\ & & & & & & & 1 \end{pmatrix} $$
Con esta matriz $M$, podemos realizar una iteración interna:
$$ 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} $$
Como resultado, una ronda del LFSR es el resultado de 4 rondas internas, que se traduce en usar $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} $$
La ronda del LFSR devuelve los 4 bits a la derecha (esto es, las posiciones $x_3$ hasta la $x_0$ del estado). Sin embargo, para el juego Piedra-Papel-Tijera se reduce $\mod{3}$ para tomar una decisión:
for i in range(n):
choice = next(rng) % 3
Este es un problema si queremos resolver este reto usando álgebra lineal, porque necesitamos cambiar las variables de $\mathbb{F}_2$ a $\mathbb{Z}/16\mathbb{Z}$ (que no es un problema) y luego a $\mathbb{Z}/3\mathbb{Z}$ (que sí es un problema).
El problema es que todos los cálculos del LFSR se realizan en $\mathbb{F}_2$. Aunque que la salida es un número de 4 bits ($\mathbb{Z}/16\mathbb{Z}$), todavía podemos considerar bits individuales y seguir trabajando en $\mathbb{F}_2$. Sin embargo, el servidor está reduciendo el número de 4 bits en $\mod{3}$. Por lo tanto, no importa cómo definamos las variables que cualquier enfoque algebraico fallará.
z3
al rescate
Después de perder mucho tiempo tratando de entender por qué SageMath no pudo resolver este problema, intenté usar z3
, que es un solucionador SMT que no depende del Álgebra Lineal.
La idea de usar z3
es que podemos definir el estado original como un vector de bits de longitud 64 y realizar cálculos simbólicos del LFSR con z3
. Después de eso, agregamos algunas restricciones con las salidas del LFSR esperadas en $\mod{3}$ y rezamos por una solución.
Implementación
Implementar una solución en z3
es bastante simple porque podemos reutilizar la mayor parte del código original. Sin embargo, debemos tener cuidado con el uso de algunas operaciones. Por ejemplo, necesitamos cambiar >>
por LShR
para forzar un desplazamiento lógico en lugar de uno aritmético:
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)
Luego, solo necesitamos tomar los valores del servidor y agregar las restricciones:
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)
Solo para aclarar, play
es una función auxiliar:
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
En este punto, podemos ver si el solucionador ha encontrado una solución y, de ser así, tomar el estado original:
if s.check() == sat:
model = s.model()
_state = int(model[state].as_long())
else:
exit(1)
Finalmente, rehacemos las 56 rondas iniciales y jugamos las siguientes 50 rondas sabiendo qué opción elegirá el servidor, para que podamos ganar el juego:
for _ in range(56):
next(lfsr)
for _ in range(50):
play([b'rock', b'paper', b'scissors'][(next(lfsr) + 1) % 3])
Flag
Si ejecutamos el script, capturaremos la 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
El script completo se puede encontrar aquí: solve.py
.