Abstract interpretation-based formal description of data obfuscation

This paper presents an abstract interpretation-based formal description of data obfuscation, which makes it possible to formally analyze and certify not only the correctness but also the potency of data obfuscating transformations. First, a semantic data obfuscating transformation is given, which is expressed as an abstract interpretation of program semantics with a variable obfuscation function and a corresponding variable deobfuscation function. Then, the syntactic data obfuscating transformation is systematically derived by composition of source-to-semantics, semantics-to-data obfuscating transformed semantics and semantics-to-source abstractions applied to fix-point trace semantics.