MIT IEEE URTC 2024. GSET 2024. Repository for the "MBASED: Practical Simplifications of Mixed Boolean-Arithmetic Obfuscation". A Binary Ninja decompiler plugin taking ideas from compiler construction to simplify obfuscated boolean expressions.
After performing simplifications and transformations on boolean expressions, we need a way to verify the correctness of two boolean expressions (simplified and unsimplified forms) to be equivalent. This is actually quite a tricky problem since comparing two boolean formulae without the NOT symbol is apparently in co-NP. Two ideas are the following.
We restrict the size of N and argue that in practice, N is not unreasonably large and brute force two truth tables and compare them (potentially requires exponential time).
We leverage z3 to tackle boolean matching. A blog post on this is here.
Boolean matching is a difficult problem which may slow down our analysis process but may be necessary to ensure the correctness of certain transformations. One idea is to enable this feature via a debug flag and turn it off if the reverse engineer does not want to guarantee correctness. We can potentially argue for a combination of these techniques.
bliutech
commented
2 months ago
After performing simplifications and transformations on boolean expressions, we need a way to verify the correctness of two boolean expressions (simplified and unsimplified forms) to be equivalent. This is actually quite a tricky problem since comparing two boolean formulae without the NOT symbol is apparently in co-NP. Two ideas are the following.
Nand argue that in practice,Nis not unreasonably large and brute force two truth tables and compare them (potentially requires exponential time).Boolean matching is a difficult problem which may slow down our analysis process but may be necessary to ensure the correctness of certain transformations. One idea is to enable this feature via a debug flag and turn it off if the reverse engineer does not want to guarantee correctness. We can potentially argue for a combination of these techniques.
Action items
To be added later.
Resources
To be added later.