Skip to Main content Skip to Navigation
Conference papers

Formal Verification of a Program Obfuscation Based on Mixed Boolean-Arithmetic Expressions

Sandrine Blazy 1 Rémi Hutin 1
1 CELTIQUE - Software certification with semantic analysis
Inria Rennes – Bretagne Atlantique , IRISA-D4 - LANGAGE ET GÉNIE LOGICIEL
Abstract : The insertion of expressions mixing arithmetic operators and bitwise boolean operators is a widespread protection of sensitive data in source programs. This recent advanced ob-fuscation technique is one of the less studied among program obfuscations even if it is commonly found in binary code. In this paper, we formally verify in Coq this data obfuscation. It operates over a generic notion of mixed boolean-arithmetic expressions and on properties of bitwise operators operating over machine integers. Our obfuscation performs two kinds of program transformations: rewriting of expressions and insertion of modular inverses. To facilitate its proof of cor-rectness, we define boolean semantic tables, a data structure inspired from truth tables. Our obfuscation is integrated into the CompCert formally verified compiler where it operates over Clight programs. The automatic extraction of our program obfuscator into OCaml yields a program with competitive results.
Complete list of metadata

Cited literature [17 references]  Display  Hide  Download
Contributor : Sandrine Blazy <>
Submitted on : Wednesday, January 9, 2019 - 12:01:32 PM
Last modification on : Saturday, July 11, 2020 - 3:14:59 AM



Sandrine Blazy, Rémi Hutin. Formal Verification of a Program Obfuscation Based on Mixed Boolean-Arithmetic Expressions. CPP 2019 - 8th ACM SIGPLAN International Conference on Certified Programs and Proofs, Jan 2019, Cascais, Portugal. pp.196-208, ⟨10.1145/3293880.3294103⟩. ⟨hal-01955773⟩



Record views


Files downloads