maisМоделирование и анализ информационных системModeling and Analysis of Information Systems1818-10152313-5417Yaroslavl State University10.18255/1818-1015-2023-2-140-159KBZXLJmais-1776Research ArticleAlgorithmsОб упрощении выражений со смешанной битовой и целочисленной арифметикойOn Simplifying Expressions with Mixed Boolean-Arithmetichttps://orcid.org/0000-0002-1491-524XКосолаповЮрий ВладимировичKosolapovYury V.itaim@mail.ruЮжный федеральный университетРоссияSouthern Federal UniversityRussian Federation202314062023302140159Copyright © Косолапов Ю.В., 20232023Косолапов Ю.В.Kosolapov Y.V.Данная работа распространяется под лицензией Creative Commons Attribution 4.0.This work is licensed under a Creative Commons Attribution 4.0 License.https://www.mais-journal.ru/jour/article/view/1776

Выражения со смешанной булевой и целочисленной арифметикой (далее — MBA-выражения, от англ. Mixed Boolean- Arithmetic) от $t$ целочисленных $n$-битных переменных часто находят применение при обфускации (запутывании) программного кода. Запутывание заключается в замене коротких выражений более длинными эквивалентными выражениями, на исследование которых, как представляется, аналитиком может быть затрачено больше времени. В работе показано, что для упрощения линейных MBA-выражений (сокращения количества слагаемых) может быть применена техника, аналогичная технике декодирования линейных кодов по информационным совокупностям. На основе этой техники в работе построены алгоритмы упрощения линейных MBA-выражений: алгоритм нахождения выражения с минимальным числом слагаемых и алгоритм сокращения числа слагаемых. На основе алгоритма сокращения числа слагаемых построен алгоритм, позволяющий оценить стойкость MBA-выражения к упрощению. В работе экспериментально оценена зависимость среднего числа слагаемых в линейном MBA-выражении, возвращаемом алгоритмами упрощения, от разрядности $n$, числа итераций декодирования и мощности набора булевых функций, по которому ищется линейная комбинация с минимальным числом ненулевых коэффициентов. Результаты экспериментов для всех рассмотренных $t$ и $n$ показывают, что если до обфускации линейное MBA-выражение содержало $r=1,2,3$ слагаемых, то разработанные алгоритмы упрощения с вероятностью, близкой к единице, позволяют по обфусцированному варианту этого выражения найти эквивалентное с числом слагаемых не более $r$. В этом заключается главное отличие техники декодирования по информационным совокупностям от известных техник упрощения линейных MBA-выражений, в которых целью является сокращение числа слагаемых до не более чем $2^t$. В работе также установлено, что для случайно сгенерированных линейных MBA-выражений с ростом $n$ среднее число слагаемых в возвращаемом выражении стремится к $2^t$ и не отличается от среднего числа слагаемых в линейном выражении, возвращаемом известными алгоритмами упрощения. Полученные результаты, в частности, позволяют определить $t$ и $n$, для которых количество слагаемых в упрощенном линейном MBA-выражении в среднем будет не менее заданного.

Mixed Boolean-Arithmetic expressions (MBA-expressions) with $t$ integer $n$-bit variables are often used for program obfuscations. Obfuscation consists of replacing short expressions with longer equivalent expressions that seem to take the analyst more time to explore. The paper shows that to simplify linear MBA-expressions (reduce the number of terms), a technique similar to the technique of decoding linear codes by information sets can be applied. Based on this technique, algorithms for simplifying linear MBA-expressions are constructed: an algorithm for finding an expression of minimum length and an algorithm for reducing the length of an expression. Based on the length reduction algorithm, an algorithm is constructed that allows to estimate the resistance of an MBA-expression to simplification. We experimentally estimate the dependence of the average number of terms in a linear MBA-expression returned by simplification algorithms on $n$, the number of decoding iterations, and the power of the set of Boolean functions, by which a linear combination with a minimum number of nonzero coefficients is sought. The results of the experiments for all considered $t$ and $n$ show that if before obfuscation the linear MBA-expression contained $r=1,2,3$ terms, then the developed simplification algorithms with a probability close to one allow using the obfuscated version of this expression find an equivalent one with no more than $r$ terms. This is the main difference between the information set decoding technique and the well-known techniques for simplifying linear MBA-expressions, where the goal is to reduce the number of terms to no more than $2^t$. We also found that for randomly generated linear MBA-expressions with increasing $n$, the average number of terms in the returned expression tends to $2^t$ and does not differ from the average number of terms in the linear expression returned by known simplification algorithms. The results obtained, in particular, make it possible to determine $t$ and $n$ for which the number of terms in the simplified linear MBA-expression on average will not be less than the given one.

обфускация программного кодаMBA-выраженияупрощение MBA-выраженийдекодирование по информационным совокупностямcode obfuscationMBA-expressionssimplification of MBA-expressionsdecoding by information setsReferencesB. Barak et al., “On the (im)possibility of obfuscating programs,” in Advances in Cryptology — CRYPTO 2001, 2001, vol. 2139, pp. 1–18.B. Barak et al., “On the (im)possibility of obfuscating programs,” in Advances in Cryptology — CRYPTO 2001, 2001, vol. 2139, pp. 1–18.Y. Zhou, A. Main, Y. X. Gu, and H. Johnson, “Information hiding in software with mixed boolean-arithmetic transforms,” in Information Security Applications. WISA 2007, 2007, vol. 4867, pp. 61–75.Y. Zhou, A. Main, Y. X. Gu, and H. Johnson, “Information hiding in software with mixed boolean-arithmetic transforms,” in Information Security Applications. WISA 2007, 2007, vol. 4867, pp. 61–75.S. Gulwani, O. Polozov, and R. Singh, “Program synthesis,” Foundations and Trends in Programming Languages, vol. 4, no. 1-2, pp. 1–119, 2017.S. Gulwani, O. Polozov, and R. Singh, “Program synthesis,” Foundations and Trends in Programming Languages, vol. 4, no. 1-2, pp. 1–119, 2017.B. Reichenwallner and P. Meerwald-Stadler, “Efficient Deobfuscation of Linear Mixed Boolean-Arithmetic Expressions,” in Proceedings of the 2022 ACM Workshop on Research on offensive and defensive techniques in the context of Man At The End (MATE) attacks, 2022, pp. 19–28.B. Reichenwallner and P. Meerwald-Stadler, “Efficient Deobfuscation of Linear Mixed Boolean-Arithmetic Expressions,” in Proceedings of the 2022 ACM Workshop on Research on offensive and defensive techniques in the context of Man At The End (MATE) attacks, 2022, pp. 19–28.L. Zobernig, “Mathematical Aspects of Program Obfuscation,” PhD thesis, The University of Auckland, 2020.L. Zobernig, “Mathematical Aspects of Program Obfuscation,” PhD thesis, The University of Auckland, 2020.P. Garba and M. Favaro, “Saturn-software deobfuscation framework based on LLVM,” in Proceedings of the 3rd ACM Workshop on Software Protection, 2019, pp. 27–38.P. Garba and M. Favaro, “Saturn-software deobfuscation framework based on LLVM,” in Proceedings of the 3rd ACM Workshop on Software Protection, 2019, pp. 27–38.N. Eyrolles, “Obfuscation with Mixed Boolean-Arithmetic Expressions: reconstruction, analysis and simplification tools,” PhD thesis, Universit'e Paris-Saclay, 2017.N. Eyrolles, “Obfuscation with Mixed Boolean-Arithmetic Expressions: reconstruction, analysis and simplification tools,” PhD thesis, Universit'e Paris-Saclay, 2017.D. Xu et al., “Boosting SMT solver performance on mixed-bitwise-arithmetic expressions,” in Proceedings of the 42nd ACM SIGPLAN International Conference on Programming Language Design and Implementation, 2021, pp. 651–664.D. Xu et al., “Boosting SMT solver performance on mixed-bitwise-arithmetic expressions,” in Proceedings of the 42nd ACM SIGPLAN International Conference on Programming Language Design and Implementation, 2021, pp. 651–664.B. Liu, J. Shen, J. Ming, Q. Zheng, J. Li, and D. Xu, “MBA-Blast: Unveiling and Simplifying Mixed Boolean-Arithmetic Obfuscation,” in Proceedings of the 30th USENIX Security Symposium, 2021, pp. 1701–1718.B. Liu, J. Shen, J. Ming, Q. Zheng, J. Li, and D. Xu, “MBA-Blast: Unveiling and Simplifying Mixed Boolean-Arithmetic Obfuscation,” in Proceedings of the 30th USENIX Security Symposium, 2021, pp. 1701–1718.E. Berlekamp, R. McEliece, and H. Van Tilborg, “On the inherent intractability of certain coding problems (corresp.),” IEEE Transactions on Information Theory, vol. 24, no. 3, pp. 384–386, 1978.E. Berlekamp, R. McEliece, and H. Van Tilborg, “On the inherent intractability of certain coding problems (corresp.),” IEEE Transactions on Information Theory, vol. 24, no. 3, pp. 384–386, 1978.E. Prange, “The use of information sets in decoding cyclic codes,” IRE Transactions on Information Theory, vol. 8, no. 5, pp. 5–9, 1962.E. Prange, “The use of information sets in decoding cyclic codes,” IRE Transactions on Information Theory, vol. 8, no. 5, pp. 5–9, 1962.C. Peters, “Information-set decoding for linear codes over $mathbbF_q$,” in Post-Quantum Cryptography. PQCrypto 2010, 2010, vol. 6061, pp. 81–94.C. Peters, “Information-set decoding for linear codes over $mathbbF_q$,” in Post-Quantum Cryptography. PQCrypto 2010, 2010, vol. 6061, pp. 81–94.V. Weger, N. Gassner, and J. Rosenthal, “A survey on code-based cryptography.” 2022.V. Weger, N. Gassner, and J. Rosenthal, “A survey on code-based cryptography.” 2022.

The authors declare that there are no conflicts of interest present.