[ca] Una expressió Mixta Booleana-Aritmètica (MBA) està formada per operadors aritmètics sobre enters i operadors bit a bit. Les expressions MBA es poden aprofitar per ofuscar el flux de dades del codi aplicant iterativament regles de reescriptura i identitats de funcions que compliquen (ofusquen) l'expressió inicial, al mateix temps que es preserva el seu comportament semàntic. Aquesta possibilitat està motivada pel fet que la combinació d'operadors d'aquests dos camps diferents no interactuen gaire bé: no tenim regles (distributivitat, factorització...) o una teoria general per tractar amb aquests operadors barrejats. En aquest projecte, explorem enfocaments ortogonals a les tècniques actuals per tractar la simplificació d'expressions MBA, les quals es basen en l'ús combinat d'execució simbòlica i síntesi de programes. La idea principal és aconseguir extreure informació subjacent a l'estructura matemàtica d'aquestes expressions. Així, podem fer servir aquesta informació, siga per si mateixa o en combinació amb altres tècniques, per facilitar la tasca de simplificar expressions MBA. Posem èmfasi en l'estudi d'alguns articles acadèmics recents que desenvolupen aquestes idees, majoritàriament dirigits a proporcionar una representació normalitzada (d'un subconjunt) d'expressions MBA lineals com a combinacions lineals respecte a un conjunt arbitrari d'operadors mínims i expressions que conformen una base d'un espai vectorial ad hoc on habiten aquestes expressions MBA lineals. Analitzem les contribucions, defectes i limitacions de les investigacions recents en aquest sentit, i en proporcionem aplicacions pràctiques. En particular, aprofitem una transformació que redueix l'alternança d'operadors aritmètics i bit a bit d'una expressió MBA tot preservant-ne el comportament semàntic en el context de la desofuscació de codi basada en la síntesi de programes. Aquesta transformació s'utilitza després per ajudar en el problema de verificar la correcció semàntica d'una expressió candidata sintetitzada, millorant així la solidesa d'aquesta tècnica.

[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.