好久没灌水了,发贴冒个泡~
最近在科研搬砖的过程中发现了一个有意思的东西 —— 编译器对于除法与求模运算的优化
用图1说明这个优化的事
求模运算的优化分为两步:1.求商;2.被除数 - 除数 * 商 = 余数。求商的过程是编译优化的结果
0xCCCCCCCD这个Magic Number怎么算出来的可以参考《算法心得:高效算法的秘密》的第10章,见图2
图1
图2
吊诡的事情就是,我用Z3尝试解这个优化后的求商运算的最大值,并发现Z3解不出(在实验室服务器上挂了快二十分钟没跑出来
贴个我的求解脚本说明问题
from z3 import *
import time
#esi -> 被除数
# mov esi, DWORD PTR _c$[esp+16]
# mov eax, -858993459 ; cccccccdH
# mul esi
# add esp, 8
# shr edx, 2
#edx -> 商
# lea ecx, DWORD PTR [edx+edx*4]
# sub esi, ecx
#esi -> 余数
eax = BitVec("b", 32)
esi = BitVec("a", 32)
ecx = BitVec("c", 32)
edx = BitVec("d", 32)
edx = Extract(63, 32, ZeroExt(32, esi) * ZeroExt(32, BitVecVal(0xCCCCCCCD, 32)))
eax = esi * BitVecVal(0xCCCCCCCD, 32)
edx = LShR(edx, 2)
ecx = edx * BitVecVal(5, 32)
esi = esi - ecx
print(edx)
print(esi)
r = BitVec("r", 32)
s = Optimize()
s.add(r == esi)
s.maximize(r)
s.check()
print(s.model().eval(r))
有意思的来了,结合编译优化,我们可以构造一种成本低廉的不透明谓词
上个示例
#include <stdio.h>
unsigned int m;
int main()
{
unsigned int j = m;
if (j % 7 > 10)
{
printf("Bogus.");
}
else
{
printf("Always here~");
}
return 0;
}
import angr
import claripy
import time
def print_constraint(state):
print(state.inspect.added_constraints)
proj = angr.Project(r"C:\Users\chengrui\source\repos\ConsoleApplication4\Release\ConsoleApplication4.exe", auto_load_libs = False)
state = proj.factory.entry_state(addr = 0x00401040)
state.inspect.b("constraints", when = angr.BP_AFTER, action = print_constraint)
a = claripy.BVS("a", 32)
state.mem[0x404378].int = a #符号化全局变量m
sm = proj.factory.simgr(state)
sm.explore(find = 0x0040106A) #寻找有无能够到达Bogus分支的输入
print(len(sm.found))
求解脚本输出的约束如下:
(<Bool a_0_32 - ((LShR(LShR(a_0_32 - 0x24924925 * (0#32 .. a_0_32)[63:32], 0x1) + 0x24924925 * (0#32 .. a_0_32)[63:32], 0x2) << 0x3) - LShR(LShR(a_0_32 - 0x24924925 * (0#32 .. a_0_32)[63:32], 0x1) + 0x24924925 * (0#32 .. a_0_32)[63:32], 0x2)) <= 0xa>,)
(<Bool a_0_32 - ((LShR(LShR(a_0_32 - 0x24924925 * (0#32 .. a_0_32)[63:32], 0x1) + 0x24924925 * (0#32 .. a_0_32)[63:32], 0x2) << 0x3) - LShR(LShR(a_0_32 - 0x24924925 * (0#32 .. a_0_32)[63:32], 0x1) + 0x24924925 * (0#32 .. a_0_32)[63:32], 0x2)) > 0xa>,)
没在笔记本上跑多久,不过联系第一个Z3求最大值求不出,我估计Z3要求解这个也挺困难的
最后想问问有没有系统研究过MaxSAT的老哥,可以指点下这种无法求解且又结构简单的表达式有构造方法吗?
[培训]《安卓高级研修班(网课)》月薪三万计划
最后于 2021-4-7 13:18
被天水姜伯约编辑
,原因: