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

International audienceThis 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