# Sonda

Là một chall RE từ The Game CTF tại HackUPC 2019 ([Tìm hiểu thêm](https://github.com/ViRb3/z3-python-ctf/tree/master/sonda))

```c
printf("Give me the magic number: ", argv, envp);
__isoc99_scanf("%d", &seed);
if ( seed % 17 || seed > 20 )
{
    puts("BAD...");
    result = 1;
}
```

Như vậy đầu tiên họ yêu cầu nhập 1 số ma thuật làm sao để không thỏa mãn 1 trong 2 điều kiện trên thì `seed % 17 = 0` và `seed <= 20`. Nên ta sẽ có số 17 và số 0.

```c
s = malloc(seed);
printf("Tell me more: ");
__isoc99_scanf("%s", s);
v4 = strlen(s);
if ( v4 <= seed )
{
    /* ... */
}
else
{
    puts("WTF is wrong with u?");
    free(s);
    result = 1;
}
```

Tiếp theo là nhập string s rồi kiểm tra kích thước của string đó nếu nó `<= seed` trên thì đúng. Bởi vậy không thể lấy giá trị 0 mà chỉ có thể lấy giá trị 17.

```c
srand(seed);
```

Nên bộ số ra ngẫu nhiên có seed =17 sẽ được giống nhau khi chạy nên ta có thể tìm thấy bộ đó.

```c
ptr = malloc(4LL * seed);
*ptr = 2 * seed + rand() % (5 * seed);
for ( i = 1; i < seed; ++i )
{
    v5 = ptr[i - 1];
    ptr[i] = v5 + rand() % 94 + 33;
}
```

* ptr được khởi tạo là một mảng động với 4 bytes int
* Các phần tử đều được dựa trên seed

```c
for ( j = 0; j < (int)seed; ++j )
      {
        v9 = 0;
        for ( k = 0; k <= j; ++k )
          v9 += s[k];
        if ( v9 != *((_DWORD *)ptr + j) )
        {
          puts("NOOB! Keep trying...");
          free(s);
          free(ptr);
          return 1;
        }
      }
```

Cái này kiểm tra lần lượt tường phần tử như sau:

* Tính tổng các phần tử trước nó và phần tử ở vị trị hiện tại đem so sánh với phần tử tại vị trí mà hệ thống đã thiết lập ở ptr.

Do đó ta giải quyết vấn đề này như sau: Điều tiên sẽ tìm các số ngẫu nhiên nhé: [(chạy bằng C)](https://www.onlinegdb.com/online_c_compiler)

{% code overflow="wrap" %}

```c
int seed = 17;
srand(seed);
printf("[");
for (int i = 0; i < seed; i++)
    printf("%d, ", rand());
    if(i == seed -1){
    printf("%d]", rand());
    }
// [1227918265, 3978157, 263514239, 1969574147, 1833982879, 488658959, 231688945, 1043863911, 1421669753, 1942003127, 1343955001, 461983965, 602354579, 726141576, 1746455982, 1641023978, 1153484208, 945487677]
```

{% endcode %}

Và phần sau sẽ sử dụng z3:

{% code overflow="wrap" %}

```python
from z3 import *

rands = [1227918265, 3978157, 263514239, 1969574147, 1833982879, 488658959, 231688945, 1043863911, 1421669753, 1942003127, 1343955001, 461983965, 602354579, 726141576, 1746455982, 1641023978, 1153484208, 945487677]

seed = 17

s = Solver()

flag  = [BitVec(f'flag_{i}', 8) for i in range(0,seed)]
ptr = [BitVec(f'ptr_{i}', 32) for i in range(0,seed)]

s.add(ptr[0] == 2 * seed + rands[0] % (5*seed))

for i in range(1, seed):
    v5 = ptr[i-1]
    s.add(ptr[i] == v5 + rands[i] % 94 + 33)

for j in range(0,seed):
    v9 = BitVecVal(0,32)
    for k in range(0, j+1):
        v9+= ZeroExt(24, flag[k])
    s.add(ptr[j] == v9)

if s.check() == sat:
    sol = []
    for i in range(seed):
        sol.append(s.model().eval(flag[i]).as_long())
    print(''.join([chr(int(c)) for c in sol]))
```

{% endcode %}


---

# Agent Instructions: Querying This Documentation

If you need additional information that is not directly available in this page, you can query the documentation dynamically by asking a question.

Perform an HTTP GET request on the current page URL with the `ask` query parameter:

```
GET https://viettaliii.gitbook.io/home/ctf/cheatsheet/python/z3py/vi-du-z3-su-dung-trong-ctf/sonda.md?ask=<question>
```

The question should be specific, self-contained, and written in natural language.
The response will contain a direct answer to the question and relevant excerpts and sources from the documentation.

Use this mechanism when the answer is not explicitly present in the current page, you need clarification or additional context, or you want to retrieve related documentation sections.