Arybo: Manipulation, Canonicalization and Identification of Mixed Boolean-Arithmetic Symbolic Expressions

Adrien Guinet (1) , Ninon Eyrolles (2, 3, 4, 1) , Marion Videau (5, 1)

1 Quarkslab
2 Université Paris-Saclay
3 UVSQ - Université de Versailles Saint-Quentin-en-Yvelines
4 CNRS - Centre National de la Recherche Scientifique
5 CARAMBA - Cryptology, arithmetic : algebraic methods for better algorithms

This article presents arybo (available at https://github.com/quarkslab/arybo) a tool that gives a bit-level symbolic representation of expressions involving various types of operators on bit strings. Such a tool can be used to gain a better understanding of complex expressions, for example expressions that mix both arithmetic and boolean operators. It can also be useful for optimization purposes, such as proving bit hacks easily. We describe why we created this tool and the various related issues, such as the choice of the internal representation and the various possible optimizations. We also show how it can be used to identify some basic arithmetic or boolean functions, and present various usage examples.

Mots clés: boolean expressions; symbolic evaluation; expression simplification; expression identification; mixed boolean arithmetic; expression storage

Domaines: Cryptographie et sécurité [cs.CR]; Calcul formel [cs.SC]

Adrien Guinet, Ninon Eyrolles, Marion Videau. Arybo: Manipulation, Canonicalization and Identification of Mixed Boolean-Arithmetic Symbolic Expressions. GreHack 2016, Nov 2016, Grenoble, France. ⟨hal-01390528⟩