**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).