插入符号变量进而利用约束器计算全局变量

题目源码

二进制文件
https://github.com/fangdada/learning-angr/blob/master/%E6%8F%92%E5%85%A5%E7%AC%A6%E5%8F%B7%E5%8F%98%E9%87%8F/issue

#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 your sm.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()))