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

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