标题: MISC系列(59)--用Arybo进行混合布尔运算分析

创建: 2025-08-12 17:22
更新: 2025-08-27 17:05
链接: https://scz.617.cn/misc/202508121722.txt

--------------------------------------------------------------------------

目录:

    ☆ 背景介绍
    ☆ 环境搭建
        1) 安装
        2) 测试
    ☆ Tutorials
        1) Symbloc evaluation of a complex function
        2) Dirac function
            2.2) 等价简化形式
            2.3) 不合要求的等价简化形式
            2.4) 快速识别Dirac函数
    ☆ 若干MBA分析示例
        1) ~(a + b)
        3) a & b
        4) a ^ b
    ☆ SiMBA/GAMBA (推荐)
    ☆ 其他讨论
        1) claripy.simplify
    ☆ 参考资源

--------------------------------------------------------------------------

☆ 背景介绍

MBA(Mixed Boolean Arithmetic)是一种将布尔运算和算术运算混合的技术，常用于
代码混淆。

参[1]，Arybo是一个Python库，可用于混合布尔运算分析，常用于逆向工程、反代码
混淆。但是，Arybo并非专门用于MBA化简，单就此目的而言，另有两个现成项目用于
化简MBA，参[4]，一个是SiMBA，另一个是GAMBA，推荐后者。

本文翻译Arybo入门教程，简介SiMBA、GAMBA的用法。

☆ 环境搭建

1) 安装

建议在Python3虚拟环境中安装，最简安装方案

pip3 install arybo

后期测试时遭遇异常

AttributeError: module 'numpy' has no attribute 'int'

升级networkx模块解决之

pip3 install --upgrade networkx

2) 测试

$ iarybo 8
...
These variables have been set for you:

  mba = MBA(8)
  x, y, a, b, c, d = 8-bit vars
...

意思是已经初始化过若干符号变量，可在提示符中直接使用

In [1]: x | 0x7f
Out[1]:
Vec([
1,
1,
1,
1,
1,
1,
1,
x7
])

位向量中x0对应LSB，x7对应MSB。意思是符号变量x按位或0x7f，结果只有最高位x7
可控。

☆ Tutorials

1) Symbloc evaluation of a complex function

--------------------------------------------------------------------------
def f ( x ) :
    v0  = (x & 0xff) * 0xe5 + 0xf7
    v0  = v0 & 0xff
    v3  = (((((v0 * 0x26) + 0x55 ) & 0xfe) + (v0 * 0xed) + 0xd6) & 0xff)
    v4  = ((((((-(v3 * 0x2)) + 0xff) & 0xfe) + v3) * 0x03) + 0x4d)
    v5  = (((((v4 * 0x56) + 0x24) & 0x46) * 0x4b) + (v4 * 0xe7) + 0x76)
    v7  = ((((v5 * 0x3a) + 0xaf) & 0xf4) + (v5 * 0x63) + 0x2e)
    v6  = v7 & 0x94
    v8  = ((((v6 + v6 + (-(v7 & 0xff))) * 0x67) + 0xd))
    res = ((v8 * 0x2d) + (((v8 * 0xae) | 0x22) * 0xe5) + 0xc2) & 0xff
    return (0xed * (res - 0xf7)) & 0xff

print( f(255) )
--------------------------------------------------------------------------

假设有个函数f(x)，接受8位整数作参数，经过一系列眼花缭乱的MBA运算，返回另一
个8位整数。f(x)实际做了一个简单异或运算，(x^0x5c)。

下面用Arybo研究f(x)

--------------------------------------------------------------------------
import arybo.lib

def f ( x ) :
    v0  = (x & 0xff) * 0xe5 + 0xf7
    v0  = v0 & 0xff
    v3  = (((((v0 * 0x26) + 0x55 ) & 0xfe) + (v0 * 0xed) + 0xd6) & 0xff)
    v4  = ((((((-(v3 * 0x2)) + 0xff) & 0xfe) + v3) * 0x03) + 0x4d)
    v5  = (((((v4 * 0x56) + 0x24) & 0x46) * 0x4b) + (v4 * 0xe7) + 0x76)
    v7  = ((((v5 * 0x3a) + 0xaf) & 0xf4) + (v5 * 0x63) + 0x2e)
    v6  = v7 & 0x94
    v8  = ((((v6 + v6 + (-(v7 & 0xff))) * 0x67) + 0xd))
    res = ((v8 * 0x2d) + (((v8 * 0xae) | 0x22) * 0xe5) + 0xc2) & 0xff
    return (0xed * (res - 0xf7)) & 0xff

mba = arybo.lib.MBA(8)
x   = mba.var('x')
ret = f(x)
print( ret )
--------------------------------------------------------------------------

执行上述代码，得到

--------------------------------------------------------------------------
Vec([
x0,
x1,
(x2 + 1),
(x3 + 1),
(x4 + 1),
x5,
(x6 + 1),
x7
])
--------------------------------------------------------------------------

位向量中x0对应LSB，x7对应MSB。人工识别出，f(x)等价于(x^0x5c)。

可用Arybo找出0x5c这个常量

--------------------------------------------------------------------------
app = ret.vectorial_decomp([x])
print( hex(app.cst().get_int_be()) )
--------------------------------------------------------------------------

执行上述代码，得到

0x5c

此处有些反直觉，得用get_int_be()，不要用get_int_le()。

检验f(x)等价于(x^0x5c)

--------------------------------------------------------------------------
all(f(x) == (x^0x5c) for x in range(0x100))
--------------------------------------------------------------------------

应该返回True。

2) Dirac function

Dirac函数在其定义域上只有一个特定值处的函数值非常见值，定义域其余位置的函
数值均为常见值。这种函数很有趣，逆向工程师在尝试暴力破解时，可能会在一段时
间后误以为它总是返回常见值，这可能导致逆向工程师生成错误的代码，或者减缓TA
对代码逻辑的理解进程。

--------------------------------------------------------------------------
def f ( y ) :
    t   = ((y + 1) & (~y))
    c   = ((t | 0x7afafa697afafa69) & 0x80a061440a061440) + \
          ((~t & 0x10401050504) | 0x1010104)
    return c

print( hex(f(0)) )
print( hex(f(100)) )
print( hex(f(0xfffffffffffffffe)) )
print( hex(f(0xffffffffffffffff)) )
--------------------------------------------------------------------------

上面这个f(y)是一个Dirac函数，在其定义域上函数值只有一个偏离，其余均为常见
值0xa061440b071544。无法用all()来检查f(y)，其定义域是64位整数，可接受时间
内无法穷举。

可用Arybo证明Dirac函数在其定义域上并非常量，进而找出使函数值偏离的自变量值。

--------------------------------------------------------------------------
import arybo.lib

def f ( y ) :
    t   = ((y + 1) & (~y))
    c   = ((t | 0x7afafa697afafa69) & 0x80a061440a061440) + \
          ((~t & 0x10401050504) | 0x1010104)
    return c

mba = arybo.lib.MBA(64)
x   = mba.var('x')
ret = f(x)
print( ret )
--------------------------------------------------------------------------

执行上述代码，得到

--------------------------------------------------------------------------
Vec([
0,
0,
1,
...
0,
((x0 * x1 * ... * x62) + (x0 * x1 * ... * x63))
])
--------------------------------------------------------------------------

上述位向量的MSB是变化的，其余位则是常量，这表明Dirac函数在其定义域上并非常
量。

用Arybo进一步研究f(y)。绝大多数时候，f(y)的MSB是0，用Arybo找出使MSB为1的自
变量:

--------------------------------------------------------------------------
solutions   = arybo.lib.boolean_expr_solve(ret[63], x, 1)
print( len(solutions) )
print( hex(solutions[0].get_int_be()) )
--------------------------------------------------------------------------

执行上述代码，得到

1
0x7fffffffffffffff

只有一个x使得MSB为1，此x为0x7fffffffffffffff

--------------------------------------------------------------------------
print( hex(f(5)) )
print( hex(f(0x7ffffffffffffffe)) )
print( hex(f(0x7fffffffffffffff)) )
--------------------------------------------------------------------------

执行上述代码，得到

0xa061440b071544    // 常见值
0xa061440b071544    // 常见值
0x80a061440b071544  // 偏离值

2.2) 等价简化形式

--------------------------------------------------------------------------
import arybo.lib

def f ( y ) :
    y  -= 0x7fffffffffffffff
    s   = ~((y | -y) >> 63) & 1
    return (s << 63) ^ 0xa061440b071544

mba = arybo.lib.MBA(64)
x   = mba.var('x')
ret = f(x)
print( ret )
--------------------------------------------------------------------------

2.3) 不合要求的等价简化形式

--------------------------------------------------------------------------
import arybo.lib

def f ( y ) :
    return (int(y == 0x7fffffffffffffff) << 63) ^ 0xa061440b071544

mba = arybo.lib.MBA(64)
x   = mba.var('x')
ret = f(x)
--------------------------------------------------------------------------

这是人类最易理解的等价简化形式，但此实现不合要求，无法对f(y)传递符号变量，
"ret = f(x)"会抛异常。

2.4) 快速识别Dirac函数

--------------------------------------------------------------------------
import arybo.lib

def f ( y ) :
    return y ^ y ^ 0xa061440b071544

mba = arybo.lib.MBA(64)
x   = mba.var('x')
ret = f(x)
print( ret )
--------------------------------------------------------------------------

若f()始终返回常量，ret的位向量中将全是常量，没有变量，反之则是Dirac函数；
无需分析app。

--------------------------------------------------------------------------
app = ret.vectorial_decomp([x])
print( app )
--------------------------------------------------------------------------

若非要看看app，会注意到App NL、AffApp matrix全零。

☆ 若干MBA分析示例

1) ~(a + b)

尝试用Arybo化简下面的e变量

--------------------------------------------------------------------------
import arybo.lib

#
# 4位的代表性足够了
#
mba = arybo.lib.MBA(4)
a   = mba.var('a')
b   = mba.var('b')
e   = ~(~(a ^ b) - 4294967294 * (b | a) + 1)
print( e )
app = e.vectorial_decomp([a,b])
print( app )
--------------------------------------------------------------------------

执行上述代码，得到

--------------------------------------------------------------------------
Vec([
(a0 + b0 + 1),
((a0 * b0) + a1 + b1 + 1),
((a1 * b1) + (a0 * a1 * b0) + (a0 * b0 * b1) + a2 + b2 + 1),
((a2 * b2) + (a1 * a2 * b1) + (a1 * b1 * b2) + (a0 * a1 * a2 * b0) + (a0 * a1 * b0 * b2) + (a0 * a2 * b0 * b1) + (a0 * b0 * b1 * b2) + a3 + b3 + 1)
])

App NL = Vec([
0,
(_0 * _4),
((_1 * _5) + (_0 * _1 * _4) + (_0 * _4 * _5)),
((_2 * _6) + (_1 * _2 * _5) + (_1 * _5 * _6) + (_0 * _1 * _2 * _4) + (_0 * _1 * _4 * _6) + (_0 * _2 * _4 * _5) + (_0 * _4 * _5 * _6))
])

AffApp matrix = Mat([
[1, 0, 0, 0, 1, 0, 0, 0]
[0, 1, 0, 0, 0, 1, 0, 0]
[0, 0, 1, 0, 0, 0, 1, 0]
[0, 0, 0, 1, 0, 0, 0, 1]
])

AffApp cst = Vec([
1,
1,
1,
1
])
--------------------------------------------------------------------------

打印e，不太容易直接看出结果，除非特别熟悉某些知识。尝试分析app，逼近结果。

最终结果的数学形式是:

(非线性部分) ^ (仿射变换矩阵 * 输入) ^ (常量部分)
(App NL) ^ ((AffApp matrix) * [a, b]^T) ^ (AffApp cst)

T表示转置，将拼接后的行向量转置成列向量，否则无法进行"矩阵 * 向量"的运算。

"AffApp matrix"是两个拼接的单位矩阵(I)。在GF(2)域的矩阵乘法中

[I | I] * [a, b]^T = (a ^ b)

于是有

(仿射变换矩阵 * 输入)=(a ^ b)

"AffApp cst"全1，一个全1的位向量在异或运算中的作用就是按位取反(NOT)，这意
味着最终结果形如:

~((App NL) ^ (a ^ b))

"App NL"中_0至_3对应a0至a3，_4到_7对应b0至b3。假设有"二进制硬件加法器"的经
验，肉眼可识别出"App NL"对应二进制加法进位链。

前置知识，在GF(2)域中加法(+)等价于异或(^)，乘法(*)等价于按位与(&)，且有乘
法对加法的分配率。在GF(2)域中，逐位相加时有如下运算模式:

--------------------------------------------------------------------------
#
# (a + b)加法和，记住这个模式
#
s       = (a ^ b ^ c_in)
        = (a + b + c_in)
#
# (a + b)进位链，记住这个模式
#
c_out   = (a & b) ^ (a & c_in) ^ (b & c_in)
        = (a * b) + (a * c_in) + (b * c_in)
--------------------------------------------------------------------------

NL[i]对应第(i-1)位加法产生的进位输出，i从0计。

NL[0]保持0

c0_in = 0

NL[1]对应第0位加法产生的进位输出

c1_in = c0_out
      = (a0 * b0) ^ (a0 & c0_in) ^ (b0 & c0_in)
      = (a0 * b0)
      = (_0 * _4)

NL[2]对应第1位加法产生的进位输出

c2_in = c1_out
      = (a1 & b1) ^ (a1 & c1_in) ^ (b1 & c1_in)
      = (_1 * _5) ^ (_1 & (_0 * _4)) ^ (_5 & (_0 * _4))
      = (_1 * _5) + (_1 * _0 * _4) + (_5 * _0 * _4)

同理，可识别出

c3_in = NL[3]

现在我们知道最终结果形如:

~((进位链) ^ (a ^ b)) = ~(a + b)

可不详细分析NL，不妨假设"~((App NL) ^ (a ^ b))"对应"~(a + b)"，因为在GF(2)
域中加法等价于异或，然后用Arybo直接检查二者是否恒等，相当于试一下。

$ iarybo 4

在提示符中输入

~(~(a ^ b) - 4294967294 * (a | b) + 1) == ~(a + b)

应该返回True。

3) a & b

--------------------------------------------------------------------------
import arybo.lib

mba = arybo.lib.MBA(4)
a   = mba.var('a')
b   = mba.var('b')
e0  = ((~a) | b) - (~a)
e1  = ((~a) | b) + (a + 1)

print( e0 )
app = e0.vectorial_decomp([a,b])
print( app )

print( e1 )
app = e1.vectorial_decomp([a,b])
print( app )

print( e0 == e1 )
--------------------------------------------------------------------------

执行上述代码，注意到e0、e1完全同构，输出完全一样

--------------------------------------------------------------------------
Vec([
(a0 * b0),
(a1 * b1),
(a2 * b2),
(a3 * b3)
])

App NL = Vec([
(_0 * _4),
(_1 * _5),
(_2 * _6),
(_3 * _7)
])

AffApp matrix = Mat([
[0, 0, 0, 0, 0, 0, 0, 0]
[0, 0, 0, 0, 0, 0, 0, 0]
[0, 0, 0, 0, 0, 0, 0, 0]
[0, 0, 0, 0, 0, 0, 0, 0]
])

AffApp cst = Vec([
0,
0,
0,
0
])
--------------------------------------------------------------------------

上例线性部分、常量部分全零，只与非线性部分相关。不看非线性部分，直接看e0、
e1的输出，也能看出结果等于(a & b)。在GF(2)域中乘法(*)等价于按位与(&)。

对于(a & b)及(a ^ b)，无论它们的MBA变形多复杂，用Arybo输出MBA表达式，将一
眼看穿。若最终结果涉及整数域的加法，分析时将比较复杂。

4) a ^ b

--------------------------------------------------------------------------
import arybo.lib

mba = arybo.lib.MBA(4)
a   = mba.var('a')
b   = mba.var('b')
e   = (a + b) - 2 * (a & b)

print( e )
app = e.vectorial_decomp([a,b])
print( app )
--------------------------------------------------------------------------

执行上述代码，得到

--------------------------------------------------------------------------
Vec([
(a0 + b0),
(a1 + b1),
(a2 + b2),
(a3 + b3)
])

App NL = Vec([
0,
0,
0,
0
])

AffApp matrix = Mat([
[1, 0, 0, 0, 1, 0, 0, 0]
[0, 1, 0, 0, 0, 1, 0, 0]
[0, 0, 1, 0, 0, 0, 1, 0]
[0, 0, 0, 1, 0, 0, 0, 1]
])

AffApp cst = Vec([
0,
0,
0,
0
])
--------------------------------------------------------------------------

在GF(2)域中加法(+)等价于异或(^)。直接看e的输出，就能看出结果等于(a ^ b)。
也可从app来分析，在GF(2)域的矩阵乘法中，"[I | I] * [a, b]^T"就是(a ^ b)。

☆ SiMBA/GAMBA (推荐)

参[4]，有两个现成项目用于化简MBA，一个是SiMBA，另一个是GAMBA，推荐后者。

问AI，"Linear MBA"与"General MBA"有什么区别，二者定义是什么？

cd /home/scz/src/ollvm

git clone ssh://git@github.com/DenuvoSoftwareSolutions/SiMBA.git SiMBA
git clone ssh://git@github.com/DenuvoSoftwareSolutions/GAMBA.git GAMBA

du -h SiMBA
rm -rf SiMBA/.git SiMBA/data SiMBA/slides/video.mp4

du -h GAMBA

SiMBA带有一堆我们不关心的内容(可删)，相当占空间，而GAMBA要小得多。

--------------------------------------------------------------------------
$ python3 /home/scz/src/ollvm/SiMBA/src/simplify.py "~(~(a ^ b) + 2 * (b | a) + 1)"
18446744073709551615+18446744073709551615*a+18446744073709551615*b

$ python3 /home/scz/src/ollvm/GAMBA/src/simplify.py "~(~(a ^ b) + 2 * (b | a) + 1)"
-1-a-b

$ python3 /home/scz/src/ollvm/GAMBA/src/simplify_general.py "~(~(a ^ b) + 2 * (b | a) + 1)"
~a-b
--------------------------------------------------------------------------

"~(~(a ^ b) + 2 * (b | a) + 1)"不属于"Linear MBA"，SiMBA有-l参数检查是否是
"Linear MBA"。已知其等价于"~(a + b)"，SiMBA化简结果非预期。推荐GAMBA的
simplify_general.py。

--------------------------------------------------------------------------
python3 /home/scz/src/ollvm/SiMBA/src/simplify.py \
"a + b + (a | ~b) + (a ^ b) - (a & ~b) + 1" \
"2 * (a | b) - (a ^ b)" \
"((~a) | b) - (~a)" \
"((~a) | b) + (a + 1)" \
"(a + b) - 2 * (a & b)"
--------------------------------------------------------------------------
python3 /home/scz/src/ollvm/GAMBA/src/simplify.py \
"a + b + (a | ~b) + (a ^ b) - (a & ~b) + 1" \
"2 * (a | b) - (a ^ b)" \
"((~a) | b) - (~a)" \
"((~a) | b) + (a + 1)" \
"(a + b) - 2 * (a & b)"
--------------------------------------------------------------------------
python3 /home/scz/src/ollvm/GAMBA/src/simplify_general.py \
"a + b + (a | ~b) + (a ^ b) - (a & ~b) + 1" \
"2 * (a | b) - (a ^ b)" \
"((~a) | b) - (~a)" \
"((~a) | b) + (a + 1)" \
"(a + b) - 2 * (a & b)"
--------------------------------------------------------------------------

对比上述三条命令的输出，均为

--------------------------------------------------------------------------
a+b
a+b
a&b
a&b
a^b
--------------------------------------------------------------------------

化简MBA时缺省是64位整数，可用-b指定位数

$ python3 /home/scz/src/ollvm/GAMBA/src/simplify_general.py -b 32 "~(~(a ^ b) - 4294967294 * (b | a) + 1)"
~a-b

用GAMBA化简MBA比Arybo快捷得多，之前太傻。

GAMBA可变相验证两个MBA是否等价:

$ python3 /home/scz/src/ollvm/GAMBA/src/simplify_general.py -b 32 "~(~(a ^ b) - 4294967294 * (b | a) + 1) - (~(a + b))"
0

输出0时表示两个MBA等价。

☆ 其他讨论

1) claripy.simplify

Angr的claripy.simplify()可进行某种程度的表达式化简，但它只做通用代数和逻辑
化简，不是专为MBA反混淆设计的。

--------------------------------------------------------------------------
import claripy

x       = claripy.BVS( 'x', 32 )
y       = claripy.BVS( 'y', 32 )

e1      = (x + 10) * 2 - 20
e2      = (y ^ y) | (x & 0xffffffff)
e3      = claripy.And( True, x > 10 )

e1_s    = claripy.simplify( e1 )
solver  = claripy.Solver()
solver.add( e1_s != (x * 2) )
#
# 是否存在一个解能满足这个约束？若satisfiable为False，意味着找不到x使得它
# 们不相等，表明它们在语义上是等价的
#
assert not solver.satisfiable()

e2_s    = claripy.simplify( e2 )
assert e2_s.structurally_match( x )

e3_s    = claripy.simplify( e3 )
solver  = claripy.Solver()
solver.add( e3_s != (x > 10) )
assert not solver.satisfiable()

print( e1 )
print( e1_s )

print( e2 )
print( e2_s )

print( e3 )
print( e3_s )
--------------------------------------------------------------------------

执行上述代码，得到

--------------------------------------------------------------------------
<BV32 (x_0_32 + 0xa) * 0x2 - 0x14>
<BV32 0x2 * x_0_32>

<BV32 x_0_32>
<BV32 x_0_32>

<Bool x_0_32 > 0xa>
<Bool !(x_0_32[31:4] == 0x0) || !(x_0_32[3:0] <= 10)>
--------------------------------------------------------------------------

e1、e2得到化简；e3_s相比e3，不但未化简，反而更复杂了。e3_s这种形式对SAT求
解器来说，是一种非常高效的优化，但从人类可读性来看，并非化简。此例直观演示
了claripy.simplify()不是专为MBA反混淆设计的。

检查e2_s时，用到structurally_match()，这是刻意为之，想演示其用法。该函数不
关心表达式的数学意义，仅递归比较抽象语法树(AST)，不理解数学定律，比如乘法
交换律，该函数判定(x + y)不等价于(y + x)。structurally_match()无法检查两个
表达式是否语义等价，非常僵化，并不适用于化简检查的场景。故用satisfiable()
间接检查语义等价。

--------------------------------------------------------------------------
import claripy

a       = claripy.BVS( 'a', 32 )
b       = claripy.BVS( 'b', 32 )

e       = ~(~(a ^ b) - 4294967294 * (b | a) + 1)
e_s     = claripy.simplify( e )

print( e )
print( e_s )
--------------------------------------------------------------------------

执行上述代码，得到

--------------------------------------------------------------------------
<BV32 ~(~(a_0_32 ^ b_1_32) - 0xfffffffe * (b_1_32 | a_0_32) + 0x1)>
<BV32 ~(0x1 + ~(a_0_32 ^ b_1_32) + 0x2 * (b_1_32 | a_0_32))>
--------------------------------------------------------------------------

上例直观表明，claripy.simplify()不是专为MBA反混淆设计的，e_s并不能提供预期
化简效果。

☆ 参考资源

[1] Arybo
    https://github.com/quarkslab/arybo
    (Manipulation, canonicalization and identification of mixed boolean-arithmetic symbolic expressions)

    https://pythonhosted.org/arybo/

    Installation
    https://pythonhosted.org/arybo/setup.html

    Tutorials
    https://pythonhosted.org/arybo/tutorial.html

[4] SiMBA (Efficient Deobfuscation of Linear Mixed Boolean-Arithmetic Expressions)
    https://github.com/DenuvoSoftwareSolutions/SiMBA

    GAMBA (Simplification of General Mixed Boolean-Arithmetic Expressions)
    https://github.com/DenuvoSoftwareSolutions/GAMBA