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