Tags: rng crypto lll lwe babai lattice z3 

Rating: 5.0

# Aero CTF 2020 - Magic II (Crypto, 496pts)

Good and difficult crypto challenge. Should be an entry exercise for getting into Lattice-based cryptoanalysis and Symbolic Execution.

## challenge details

We got Python script (excerpted):

```python
def create_potion(ingredients: List[int], amounts: List[int]) -> int:
magic_constant = 1046961993706256953070441
effect = sum(starmap(mul, zip(ingredients, amounts)))
side_effect = getrandbits(13) ^ getrandbits(37)
return (effect + side_effect) % magic_constant

def main():
from secret import FLAG
security_level = 64
ingredients_count = 12
random = Random.create(security_level)
potions_count = int.from_bytes(FLAG, 'big') ^ random.randint(512)
print(f'There are {potions_count} famous potions in the world. We are trying to create something new!')
ingredients = [random.randint(security_level) for _ in range(ingredients_count)]
while True:
amounts = [getrandbits(41) for _ in range(len(ingredients))]
effect = create_potion(ingredients, amounts)
print(f'A potion with {amounts} amounts of ingregients has {effect} value of effect.')
choice = input('Would you like to create another potion? (y/n): ')
if not choice.lower().startswith('y'):
break
return
```

and its output for 100 rounds:

```
There are 6649072325173565167790166618241744001772629470276152191212306811403978598551946952005874796389850254324206273014469019894959347241157412707755498754629152 famous potions in the world. We are trying to create something new!
A potion with [432963764937, 1734018663110, 341889949567, 1898982667391, 2077151719276, 1407002783602, 1284167537027, 1834426568578, 285492081118, 2058066808411, 682725745551, 212794466530] amounts of ingregients has 675829748828112222653599 value of effect.
Would you like to create another potion? (y/n): y
A potion with [1520127565791, 1613928435234, 1481625614519, 513222175065, 1825760063135, 849601240471, 2028256612679, 884310262235, 240010057040, 992839358285, 923505774812, 383090205845] amounts of ingregients has 19282755083699178123269 value of effect.
Would you like to create another potion? (y/n): y
(...194 lines omitted)
A potion with [353615797819, 779510410363, 634337418618, 112328801072, 1308573457212, 1018471322967, 2191760622378, 1641311358023, 126717015375, 790498704391, 2029952294067, 1080095433537] amounts of ingregients has 64147717148582160182619 value of effect.
Would you like to create another potion? (y/n): n
```

## Recovering ingredients by solving CVP

`Random` is the original RNG implementation of this challenge. We should analyse it later, but at first we should guess what the `ingredients` is.

The calculation of creating potion above can be treated as manipulation of matrix. If we define

$$
\begin{align}
\boldsymbol{A} =&\;\texttt{amounts[]}\\
\boldsymbol{s} =&\;\texttt{ingredients}\\
n =&\;\texttt{ingredients_count}\\
\boldsymbol{e} =&\;\texttt{side_effect[]}\\
\boldsymbol{b} =&\;\texttt{effect[]}\\
q =&\;\texttt{magic_constant}
\end{align}
$$

the calculation can be described as:

$$
\begin{align}
\boldsymbol{A}\boldsymbol{s}+\boldsymbol{e}=\boldsymbol{b}\bmod
q
\end{align}
$$

And we know $\boldsymbol{A}$, $\boldsymbol{b}$, and $q$... well, that is what exactly [LWE cryptosystem](http://cryptowiki.net/index.php?title=LWE-based_cryptographic_protocols#LWE-based_cryptosystems) is!

Using a [lattice](https://ctf-wiki.github.io/ctf-wiki/crypto/asymmetric/lattice/overview/) for attacking LWE is very common. In this case, there are too many bits in $q$ and the error $\boldsymbol{e}$ is relatively small. It is very likely to break this cipher by lattice attack.

Solving LWE is reducted into [CVP](https://ctf-wiki.github.io/ctf-wiki/crypto/asymmetric/lattice/cvp/) in the lattice theory. First break the equation into rows:

\[
\begin{cases}
\boldsymbol{a}_{1}\boldsymbol{s}+e_{1}=b_{1}\bmod q\\
\boldsymbol{a}_{2}\boldsymbol{s}+e_{2}=b_{2}\bmod q\\
\vdots\\
\boldsymbol{a}_{m}\boldsymbol{s}+e_{m}=b_{m}\bmod q
\end{cases}
\]

and erase the modulo by introducing coefficient $k_1, \dots, k_n\in\mathbb{Z}$:

$$
\begin{cases}
\boldsymbol{a}_{1}\boldsymbol{s}+k_{1}q=b_{1}-e_{1}\\
\boldsymbol{a}_{2}\boldsymbol{s}+k_{2}q=b_{2}-e_{2}\\
\vdots\\
\boldsymbol{a}_{m}\boldsymbol{s}+k_{m}q=b_{m}-e_{m}
\end{cases}
$$

This can be translated into matrix operation:

$$
\left[\begin{array}{cccccccc}
a_{11} & a_{12} & \cdots & a_{1n} & q & 0 & \cdots & 0\\
a_{21} & \ddots & & \vdots & 0 & q & & \vdots\\
\vdots & & \ddots & \vdots & \vdots & & \ddots & \vdots\\
a_{m1} & \cdots & \cdots & a_{mn} & 0 & \cdots & \cdots & q
\end{array}\right]\left[\begin{array}{c}
s_{1}\\
\vdots\\
s_{n}\\
k_{1}\\
\vdots\\
k_{m}
\end{array}\right]=\boldsymbol{b}-\boldsymbol{e}
$$

and also can be written as following:

$$
s_{1}\left[\begin{array}{c}
a_{11}\\
a_{21}\\
\vdots\\
a_{m1}
\end{array}\right]+\cdots+s_{n}\left[\begin{array}{c}
a_{1n}\\
a_{2}\\
\vdots\\
a_{mn}
\end{array}\right]+k_{1}\left[\begin{array}{c}
q\\
0\\
\vdots\\
0
\end{array}\right]+k_{2}\left[\begin{array}{c}
0\\
q\\
\vdots\\
0
\end{array}\right]+\cdots+k_{m}\left[\begin{array}{c}
0\\
0\\
\vdots\\
q
\end{array}\right]=\boldsymbol{b}-\boldsymbol{e}
$$

This is considered as a lattice, with $n+m$ base vectors and targetting $\boldsymbol{b}$ with a (relatively) small error $\boldsymbol{e}$. In the other words, we should adjust parameters $s_1, \dots, s_n, k_1, \dots, k_m$ and find the closest vector into $\boldsymbol{b}$.

This is called CVP (Closest Vector Problem) in the lattice theory. It is known that this is NP-hard, but, by using LLL and [Babai's nearest plane algorithm](https://ctf-wiki.github.io/ctf-wiki/crypto/asymmetric/lattice/cvp/#babais-nearest-plane-algorithm), a good approximate solution can be found in the polynomial time (w/o knowing actual parameters $s_1, \dots, s_n, k_1, \dots, k_m$). This is enough for this case.

We did implement solver with SageMath:

{%gist hakatashi/2266a5df35cc79de50b86d2419b33a6f %}

Note that SageMath implements [closest_vector()](http://doc.sagemath.org/html/en/reference/modules/sage/modules/free_module_integer.html#sage.modules.free_module_integer.FreeModule_submodule_with_basis_integer.closest_vector) but it is a definitive solution and (thus) very very slow.

And we recovered `ingredients` as:

```
[15947635162630781022, 13358685451704549741, 16125368066162772035, 15826229117247968913, 2646399917048428358, 4885066420149917790, 5030034390407155536, 14428761327704365060, 12909357566263158604, 8293230205600583029, 14383462958218167109, 15636563551321853965]
```

## Recover the Initial State of RNG by Z3

Now we know the last $64\times12$ bits of RNG output. Let's move into RNG.

The generation of bits can be seen here in the given code:

```python
def _getbit(self) -> int:
buffer = 2 * self._state | self._state >> (self._size - 1) | self._state << (self._size + 1)
self._state = reduce(ior, ((buffer >> i & 7 in [1, 2, 3, 4]) << i for i in range(self._size)))
return self._state & 1
```

The state parameter is 64bits unsigned integer. This code is a bit tricky, but actually this is just getting `i-1..i+1`-th bits of previous state for each `i`-th bits and checking if it is 1, 2, 3, or 4.

Solving the puzzle by hand is an option, but this check can be translated into a simple logical expression, `(state[i-1] | state[i]) ^ state[i+1]` (Write your own truth table!). It is very likely that this can be automatically analyzed by SAT-solver. Let's try with Z3Py!

{%gist hakatashi/c7826a6b6ff64e97a934d2485099af45 %}

Execute and wait for a few minites... and yes, SAT!

```
$ python2 solve.py
Solving...
('SAT', [state__13 = True,
state__2 = True,
state__46 = True,
state__42 = True,
state__49 = False,
state__50 = False,
state__54 = False,
state__63 = True,
state__25 = False,
state__39 = False,
state__30 = True,
state__19 = True,
state__47 = True,
state__41 = False,
state__38 = False,
state__20 = False,
state__23 = True,
state__52 = False,
state__11 = True,
state__18 = False,
state__21 = True,
state__55 = False,
state__62 = False,
state__1 = True,
state__40 = True,
state__51 = False,
state__0 = False,
state__3 = False,
state__14 = False,
state__57 = True,
state__28 = False,
state__9 = True,
state__45 = False,
state__22 = False,
state__44 = True,
state__35 = True,
state__5 = False,
state__6 = True,
state__27 = True,
state__32 = False,
state__60 = False,
state__61 = True,
state__53 = True,
state__4 = False,
state__16 = False,
state__29 = False,
state__34 = False,
state__37 = False,
state__7 = True,
state__15 = False,
state__26 = True,
state__12 = True,
state__43 = False,
state__10 = True,
state__59 = False,
state__17 = True,
state__56 = False,
state__48 = True,
state__31 = True,
state__36 = False,
state__8 = True,
state__58 = True,
state__24 = True,
state__33 = False])
```

This is the initial state (=seed) of the RNG. We can recover the following 512bits of outputs by simply modifying the original code, resulting:

```
6649072325173565167790166607303544343236044285056890707110072554988785350596422550050892070579043919783725646730179370397111189029461357122780521673335594
```

Now xor it with the given number (`potions_count`) and successfully get flag:

`Aero{b3_c4r3ful_n0t_4ll_p0t10ns_4r3_g00d_f0r_h34lth}`

Great!

Original writeup (https://hackmd.io/@hakatashi/B1OM7HFVI).