首页
论坛
课程
招聘
[原创]有意思的除法优化及成本低廉的不透明谓词构造
2021-4-7 13:07 1357

[原创]有意思的除法优化及成本低廉的不透明谓词构造

2021-4-7 13:07
1357

好久没灌水了,发贴冒个泡~


最近在科研搬砖的过程中发现了一个有意思的东西 —— 编译器对于除法与求模运算的优化


用图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的老哥,可以指点下这种无法求解且又结构简单的表达式有构造方法吗?


[注意] 招人!base上海,课程运营、市场多个坑位等你投递!

最后于 2021-4-7 13:18 被天水姜伯约编辑 ,原因:
收藏
点赞0
打赏
分享
最新回复 (1)
雪    币: 5274
活跃值: 活跃值 (1112)
能力值: ( LV3,RANK:35 )
在线值:
发帖
回帖
粉丝
alphc 活跃值 2021-4-7 18:07
2
1

有意思,mark了

最后于 2021-4-7 18:08 被alphc编辑 ,原因:
游客
登录 | 注册 方可回帖
返回