0

为什么长度>=60时angr不能解决问题？我只是得到一个死机。当我只检查 g[66] 时，答案是正确的。但是当使用长度超过 59 的 strcmp 时，我无法获得分叉状态。

解决.py

import angr
import claripy

p = angr.Project("a.out",auto_load_libs=True)

password_chars = [claripy.BVS("flag_%d" % i, 8) for i in range(70)]
password_ast = claripy.Concat(*password_chars)

simgr = p.factory.simulation_manager(p.factory.full_init_state(stdin=password_ast))
simgr.run()

print(simgr)

目标.c

#include <stdio.h>

int main(){
    char g[100];
    scanf("%s",g);
    if(strcmp(g,"vvvvvvvvvvvvvvvvvvvvvvvvvvvvvvvvvvvvvvvvvvvvvvvvvvvvvvvvvvvv")==0){  // 60 bytes
        printf("Correct!");
    }
    
    return 0;
}

输出

WARNING | 2022-02-15 00:51:30,367 | cle.loader | The main binary is a position-independent executable. It is being loaded with a base address of 0x400000.
WARNING | 2022-02-15 00:51:30,903 | angr.simos.simos | stdin is constrained to 70 bytes (has_end=True). If you are only providing the first 70 bytes instead of the entire stdin, please use stdin=SimFileStream(name='stdin', content=your_first_n_bytes, has_end=False).
WARNING | 2022-02-15 00:51:33,425 | angr.storage.memory_mixins.default_filler_mixin | The program is accessing memory or registers with an unspecified value. This could indicate unwanted behavior.
WARNING | 2022-02-15 00:51:33,425 | angr.storage.memory_mixins.default_filler_mixin | angr will cope with this by generating an unconstrained symbolic variable and continuing. You can resolve this by:
WARNING | 2022-02-15 00:51:33,425 | angr.storage.memory_mixins.default_filler_mixin | 1) setting a value to the initial state
WARNING | 2022-02-15 00:51:33,425 | angr.storage.memory_mixins.default_filler_mixin | 2) adding the state option ZERO_FILL_UNCONSTRAINED_{MEMORY,REGISTERS}, to make unknown regions hold null
WARNING | 2022-02-15 00:51:33,425 | angr.storage.memory_mixins.default_filler_mixin | 3) adding the state option SYMBOL_FILL_UNCONSTRAINED_{MEMORY,REGISTERS}, to suppress these messages.
WARNING | 2022-02-15 00:51:33,425 | angr.storage.memory_mixins.default_filler_mixin | Filling memory at 0x7fffffffffeff40 with 8 unconstrained bytes referenced from 0x5a22d0 (strcmp+0x0 in libc.so.6 (0xa22d0))
<SimulationManager with 1 deadended>

- - - - - 更新 - - - - -

我发现我可以添加“LAZY solve”选项，我将获得分叉状态。但它说它是Unsat ...？

import angr
import claripy

p = angr.Project("a.out",auto_load_libs=True)

password_chars = [claripy.BVS("flag_%d" % i, 8) for i in range(100)]
password_ast = claripy.Concat(*password_chars)

simgr = p.factory.simulation_manager(p.factory.full_init_state(stdin=password_ast,add_options={angr.options.LAZY_SOLVES}))
simgr.run()


In [21]: %run solve.py
WARNING | 2022-02-15 01:48:11,156 | cle.loader | The main binary is a position-independent executable. It is being loaded with a base address of 0x400000.
WARNING | 2022-02-15 01:48:11,676 | angr.simos.simos | stdin is constrained to 100 bytes (has_end=True). If you are only providing the first 100 bytes instead of the entire stdin, please use stdin=SimFileStream(name='stdin', content=your_first_n_bytes, has_end=False).
WARNING | 2022-02-15 01:48:13,289 | angr.storage.memory_mixins.default_filler_mixin | Filling memory at 0x7fffffffffeff40 with 8 unconstrained bytes referenced from 0x5a22d0 (strcmp+0x0 in libc.so.6 (0xa22d0))

In [22]: simgr.deadended[1].posix.dumps(0)
---------------------------------------------------------------------------
UnsatError                                Traceback (most recent call last)
4

1 回答 1

0

第一个“char g[100]”未初始化。这可能会导致错误的比较，并使其地址与字符串的地址相同。尝试像这样初始化它：

 char g[100] = { 0 };
于 2022-02-14T19:33:01.400 回答