[en] A Mixed Boolean-Arithmetic (MBA) expression is composed of integer arithmetic operators and bitwise operators. MBA expressions can be leveraged to obfuscate the data-flow of code by iteratively applying rewrite rules and function identities that complicate (obfuscate) the initial expression while preserving its semantic behavior. This possibility is motivated by the fact that the combination of operators from these different fields do not interact well together: we have no rules (distributivity, factorization...) or general theory to deal with this mixing of operators. In this project, we study and explore approaches to MBA simplification which are orthogonal to current techniques relying on a combination of symbolic execution and program synthesis. The main idea is to be able to extract some information from the underlying mathematical structure of such expressions. Then, this information can be used either alone or in combination with other techniques to aid in the task of MBA simplification. The focus is set upon recent research literature that develops such ideas, mainly addressing the problem of providing a normalized representation of (a subset of) linear MBA expressions as linear combinations with respect to an arbitrary set of minimal operators and expressions that form a basis of an ad hoc vector space where such linear MBA expressions live. We analyze the contributions, flaws and limitations of recent research in this regard, and provide practical applications. In particular, we leverage a semantics preserving transformation which reduces the alternation of arithmetic and bitwise operators of an MBA expression in the context of program synthesis based code deobfuscation. This transformation is then used to aid in the problem of verifying the semantic correctness of a synthesized candidate expression, thus improving the soundness of such technique.

[es] Una expresión Mixta Booleana-Aritmética (MBA) está formada por operadores aritméticos sobre enteros y operadores bit a bit. Las expresiones MBA se pueden aprovechar para ofuscar el flujo de datos del código aplicando iterativamente reglas de reescritura e identidades de funciones que complican (ofuscan) la expresión inicial, al tiempo que se preserva su comportamiento semántico. Esta posibilidad está motivada por el hecho de que la combinación de operadores de estos dos campos diferentes no interactúan muy bien: carecemos de reglas (distributividad, factorización...) o una teoría general para tratar con estos operadores mezclados. En este proyecto, exploramos enfoques ortogonales a las técnicas actuales para tratar la simplificación de expresiones MBA, que se basan en el uso combinado de ejecución simbólica y síntesis de programas. La idea principal es conseguir extraer información subyacente a la estructura matemática de estas expresiones. Así, podemos utilizar esta información, sea por sí misma o en combinación con otras técnicas, para facilitar la tarea de simplificar expresiones MBA. Ponemos énfasis en el estudio de algunos artículos académicos recientes que desarrollan estas ideas, mayoritariamente dirigidos a proporcionar una representación normalizada (de un subconjunto) de expresiones MBA lineales como combinaciones lineales respecto a un conjunto arbitrario de operadores mínimos y expresiones que conforman una base de un espacio vectorial ad hoc donde habitan estas expresiones MBA lineales. Analizamos las contribuciones, defectos y limitaciones de las investigaciones recientes en este sentido, y proporcionamos aplicaciones prácticas. En particular, aprovechamos una transformación que reduce la alternancia de operadores aritméticos y bit a bit de una expresión MBA preservando su comportamiento semántico en el contexto de la desofuscación de código basada en la síntesis de programas. Esta transformación se utiliza luego para ayudar al problema de verificar la corrección semántica de una expresión candidata sintetizada, mejorando así la solidez de esta técnica.