插入符号变量进而利用约束器计算全局变量
题目源码
#include <stdio.h>
char u=0;
int main(void)
{
int i, bits[2]={0,0};
for (i=0; i<8; i++) {
bits[(u&(1<<i))!=0]++;
}
if (bits[0]==bits[1]) {
printf("you win!");
}
else {
printf("you lose!");
}
return 0;
}
题目很简单,需要得到一个特殊的u值使得条件成立输出you win就行了,利用angr state的memory方法的store函数就可以把符号变量插入到全局变量中,然后老样子利用explore约束求到最终解。
注意点
- 如果要使用
state.memory.store
,则要在初始化的时候加上add_options={angr.options.SYMBOLIC_WRITE_ADDRESSES}
(而在使用sm.found[0]的found.memory.store则不用添加选项) state.posix.dumps(1)
获得状态的标准输出- Verify the find/avoid addresses you used. When
len(sm.found) == 0
, that means yoursm.explore()
couldn't find a path.
EXP:
import angr
import claripy
def main():
p = angr.Project('./issue', load_options={"auto_load_libs": False})
# By default, all symbolic write indices are concretized.
state = p.factory.entry_state(add_options={angr.options.SYMBOLIC_WRITE_ADDRESSES})
u = claripy.BVS("u", 8)
state.memory.store(0x804a021, u)
sm = p.factory.simulation_manager(state)
def correct(state):
try:
return b'win' in state.posix.dumps(1)
except:
return False
def wrong(state):
try:
return b'lose' in state.posix.dumps(1)
except:
return False
sm.explore(find=correct, avoid=wrong)
# Alternatively, you can hardcode the addresses.
# sm.explore(find=0x80484e3, avoid=0x80484f5)
return sm.found[0].solver.eval(u)
def test():
assert '240' in str(main())
if __name__ == '__main__':
print(repr(main()))
Comments | NOTHING