# 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):

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 the actual value of `ingredients`.

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

$$
\begin{aligned}
\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{aligned}
$$

the calculation can be described as:

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

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:

    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!