# 0x00. 一切开始之前

MIT 6.858 是面向高年级本科生与研究生开设的一门关于计算机系统安全（secure computer security）的课程，内容包括威胁模型（threat models）、危害安全的攻击（attacks that compromise security）、实现安全的技术（techniques for achieving security）

• Lab1：缓冲区溢出（buffer overflow）
• Lab2：权限分离与服务侧沙箱（privilege separation and server-side sandboxing）
• Lab3：符号执行（symbolic execution）
• Lab4：浏览器安全（browser security）
• Lab5：安全的文件系统（secure file system）

## PRE. 环境搭建 && 说明

### Method I.（推荐）使用 MIT 提供的 VM 镜像

MIT 提供了一个 course VM image ，其中有着一个 Ubuntu 21.10 的系统，登录的用户名为 student，密码为 6858，下载解压后根据自身的本地环境进行对应的操作：

• 使用 KVM 运行：直接运行 ./6.858-x86_64-v22.sh 即可
• 使用 VMware运行：新建虚拟机→稍后安装操作系统→选择系统 Linux > Debian 9.x 64-bit →移除原有虚拟磁盘→添加新的虚拟磁盘→选择 6.858-x86_64-v22.vmdk 即可

zookd 有两种版本：

• zookd-exstack：栈具有可执行权限
• zookd-nxstack：栈不具有可执行权限

### Method III.使用 docker 搭建实验环境

Dockerfile，注意替换上自己的公钥，如果没有从外部连接容器的需求的话这一步可以跳过

# 0x01. Lab1: Buffer overflows

## Part 1: Finding buffer overflows

Exercise 1. Study the web server’s C code (in zookd.c and http.c), and find one example of code that allows an attacker to overwrite the return address of a function. Hint: look for buffers allocated on the stack. Write down a description of the vulnerability in the file answers.txt. For your vulnerability, describe the buffer which may overflow, how you would structure the input to the web server (i.e., the HTTP request) to overflow the buffer and overwrite the return address, and the call stack that will trigger the buffer overflow (i.e., the chain of function calls starting from process_client).

It is worth taking your time on this exercise and familiarizing yourself with the code, because your next job is to exploit the vulnerability you identified. In fact, you may want to go back and forth between this exercise and later exercises, as you work out the details and document them. That is, if you find a buffer overflow that you think can be exploited, you can use later exercises to figure out if it indeed can be exploited. It will be helpful to draw a stack diagram like the figures in Smashing the Stack in the 21st Century.

#### process_client()：处理单次 HTTP request

process_client() 的逻辑也比较简单，主要是调用 http_request_line() 获取请求头第一行，之后给到 env_deserialize() 解析环境变量，之后调用 http_request_headers() 解析剩下的 header，最后调用 http_serve() 处理

• 这里我们注意到 value 是一个位于函数栈上的字符数组，长度仅为 512，而该 HTTP server 所允许的单行最大长度为 8192 字符，这意味着我们可以很轻易地通过传入一个较长的键值对参数来完成栈溢出

• 这里我们注意到 envvar 也是一个位于函数栈上的长度仅为 512的字符数组，因此在这里也可以发生栈溢出

Exercise 2. Write an exploit that uses a buffer overflow to crash the web server (or one of the processes it creates). You do not need to inject code at this point. Verify that your exploit crashes the server by checking the last few lines of dmesg | tail, using gdb, or observing that the web server crashes (i.e., it will print Child process 9999 terminated incorrectly, receiving signal 11)

Provide the code for the exploit in a file called exploit-2.py.

The vulnerability you found in Exercise 1 may be too hard to exploit. Feel free to find and exploit a different vulnerability.

MIT 其实还贴心地提供了一个 exploit-template.py 文件，让笔者这种不怎么会用 socket 写裸 HTTP 请求的菜鸡可以参考（笑），他真的👴哭死

## Part 2: Code injection

Exercise 3 (warm-up). Modify shellcode.S to unlink /home/student/grades.txt. Your assembly code can either invoke the SYS_unlink system call, or call the unlink() library function.

Exercise 4. Starting from one of your exploits from Exercise 2, construct an exploit that hijacks the control flow of the web server and unlinks /home/student/grades.txt. Save this exploit in a file called exploit-4.py.

Verify that your exploit works; you will need to re-create /home/student/grades.txt after each successful exploit run.

Suggestion: first focus on obtaining control of the program counter. Sketch out the stack layout that you expect the program to have at the point when you overflow the buffer, and use gdb to verify that your overflow data ends up where you expect it to. Step through the execution of the function to the return instruction to make sure you can control what address the program returns to. The next, stepi, and x commands in gdb should prove helpful.

Once you can reliably hijack the control flow of the program, find a suitable address that will contain the code you want to execute, and focus on placing the correct code at that address—e.g. a derivative of the provided shell code.

## Part 3: Return-to-libc attacks

Exercise 5. Starting from your exploit in Exercises 2 and 4, construct an exploit that unlinks /home/student/grades.txt when run on the binaries that have a non-executable stack. Name this new exploit exploit-5.py.

In this attack you are going to take control of the server over the network without injecting any code into the server. You should use a return-to-libc attack where you redirect control flow to code that already existed before your attack. The outline of the attack is to perform a buffer overflow that:

1. causes the argument to the chosen libc function to be on stack
2. then causes accidentally to run so that argument ends up in %rdi
3. and then causes accidentally to return to the chosen libc function

It will be helpful to draw a stack diagram like the figures in Smashing the Stack in the 21st Century at (1) the point that the buffer overflows and (2) at the point that accidentally runs.

Challenge! (optional) The accidentally function is a bit artificial. For extra credit, figure out how to perform the return-to-libc attack without relying on that function (delete it and find another way to make your exploit work). Provide your attack in exploit-challenge.py. Also, briefly explain the attack and provide ROP gadgets you use in answers.txt.

You will need to find another chunk of code to reuse that gives you control over %rdi. You can read through the disassembly (e.g. using objdump) to look for useful ROP gadgets.

Because of the nature of x86/x86-64, you can use another technique to find sequences of instructions that don’t even appear in the disassembly! Instructions are variable-length (from 1 to 15 bytes), and by causing a misaligned parse (by jumping into the middle of an intended instruction), you can cause a sequence of machine code to be misinterpreted. For example, the instruction sequence pop %r15; ret corresponds to the machine code 41 5F C3. But instead of executing from the start of this instruction stream, if you jump 1 byte in, the machine code 5F C3 corresponds to the assembly pop %rdi; ret.

Automated tools such as ROPgadget.py can assist you in searching for ROP gadgets, even finding gadgets that arise from misaligned parses. The 6.858 VM already has ROPgadget installed.

You may find it useful to search for ROP gadgets not just in the zookd binary but in other libraries that zookd loads at runtime. To see these libraries, and the addresses at which they are loaded, you can run ( ulimit -s unlimited && setarch -R ldd zookd-nxstack ). The ulimit and setarch commands set up the same environment used by clean-env.sh, so that ldd prints the same addresses that will be used at runtime.

## Part 4: Fixing buffer overflows and other bugs

Exercise 6. Look through the source code and try to find more vulnerabilities that can allow an attacker to compromise the security of the web server. Describe the attacks you have found in answers.txt, along with an explanation of the limitations of the attack, what an attacker can accomplish, why it works, and how you might go about fixing or preventing it. You should ignore bugs in zoobar‘s code. They will be addressed in future labs.

One approach for finding vulnerabilities is to trace the flow of inputs controlled by the attacker through the server code. At each point that the attacker’s input is used, consider all the possible values the attacker might have provided at that point, and what the attacker can achieve in that manner.

You should find at least two vulnerabilities for this exercise.

Exercise 6 里说 You should find at least two vulnerabilities for this exercise. ，笔者已经找足两个，满足了题目要求，就不继续找更多的了（笑）👴选择直接摆大烂

Exercise 7. For each buffer overflow vulnerability you have exploited in Exercises 2, 4, and 5, fix the web server’s code to prevent the vulnerability in the first place. Do not rely on compile-time or runtime mechanisms such as stack canaries, removing -fno-stack-protector, baggy bounds checking, etc.

Make sure that your code actually stops your exploits from working. Use make check-fixed to run your exploits against your modified source code (as opposed to the staff reference binaries from bin.tar.gz). These checks should report FAIL (i.e., exploit no longer works). If they report PASS, this means the exploit still works, and you did not correctly fix the vulnerability.

Note that your submission should not make changes to the Makefile and other grading scripts. We will use our unmodified version during grading.

You should also make sure your code still passes all tests using make check, which uses the unmodified lab binaries.

# 0x02.Lab 2: Privilege separation and server-side sandboxing（uncompleted）

## Introduction

• 一个按用户名欢迎访客的 profile
• 一个记录最后几位访客的 profile
• 一个为每位访客提供 zoobar 的 profile（限制为每分钟1位）

## Prelude: What’s a zoobar?

zoobar 的一个重要特性是允许在用户之间传递凭证（credits），这由 transfer.py 实现，我们可以启动 zoobar 感受一下：

configure_base() 中有着一个调用 apt-get 的逻辑，由于 Ubuntu 21.10 已经 EOL 了，所以这一步是必然会失败的

👴真的麻了，这实验™是 MIT 今年春季学期发布的，用个 20.04 这样的 LTS 不好🐎，用个就只剩几个🈷寿命的 21.10 就离谱

MIT 估计是不会修这个问题了，而下一次的实验手册得等到 2023 年的春季学期才能上线，那这里笔者只能自行尝试解决这个问题了: (

# 0x03.Lab 3: Symbolic execution

## Introduction

EXE paper 中描述了一个用于 C 程序的符号执行系统，为了简单化，该 lab 将通过修改 Python 对象与重载特定方法来为 Python 程序建立一个符号/混合执行系统，类似于 EXE，我们将使用一个 SMT （ Satisfiability Modulo Theories，可满足性模理论）求解器来检查可满足的约束，这意味着我们的求解器可以检查同时包含传统布尔可满足性表达式与涉及其他“理论”的约束如整型、位向量、字符串等

## Using an SMT solver

Exercise 1. Implement a correct function to compute the unsigned average of a and b using only 32-bit arithmetic, by modifying the u_avg = ... line in int-avg.py.

For the purposes of this exercise, you are not allowed to change the bit-widths of your operands. This is meant to represent the real world, where you cannot just add one more bit to your CPU’s register width.

You may find it helpful to search online for correct ways to perform fixed-width integer arithmetic. The book Hacker’s Delight by Henry S. Warren is a particularly good source of such tricks.

Check your averaging function by re-running ./int-avg.py or make check. If your implementation is correct, int-avg.py should produce the message Answer for unsigned avg: unsat.

• (a / 2) + (b / 2) + ((a % 2) + (b % 2)) / 2

• (a & b) + ((a ^ b) >> 1)

Challenge! (optional) For extra credit, figure out how to compute the average of two 32-bit signed values. Modify the s_avg = ... line in int-avg.py, and run ./int-avg.py or make check to check your answer. Keep in mind the direction of rounding: 3/2=1 and -3/2=-1, so so the average of 1 and 2 should be 1, and the average of -2 and -1 should be -1.

As you explore signed arithmetic, you may find it useful to know that Z3 has two different modulo-like operators. The first is signed modulo, which you get by using a % b in the Python Z3 API. Here, the sign of the result follows the sign of the divisor (i.e., b). For example, -5 % 2 = 1. The second is signed remainder, which you get by using z3.SRem(a, b). Here, the sign of the result follows the sign of the dividend (i.e., a). With the same example inputs, z3.SRem(-5, 2) = -1.

• tmp = (a & b) + ((a ^ b) >> 1)
• res = tmp + ((tmp >> 31) & (a ^ b))

## Interlude: what are symbolic and concolic execution?

• 由于程序包含基于输入的中间值（例如输入两个整型并计算平均值，并存放在一些变量中），我们需要记住输入与这些中间值间的关系，通常这通过允许变量或内存位置有 具体的 （concrete，例如 114514 这样的实际值） 或 符号的 （symbolic，例如我们在上一小节构建的符号变量） 值
• 我们需要根据输入来确定要执行的控制流分支，这归结于在程序每次发生分支时构建符号约束，在程序选择一些特定分支时描述布尔条件（以程序原有输入的形式）；由于我们持续保存中间值与程序原有输入的间隙，我们并不需要通过原有输入来计算约束，这些约束就像我们在前文中用来寻找整型中漏洞的约束；确定控制流约束非常重要，因为若程序初始时进入了特定分支路径，我们想要知道如何让他走到另一条路径来寻找是否存在漏洞，在 EXE 的论文中使用了一个 C-to-C 的翻译器来在所有的分支上插入他们的代码
• 对于每一条上述分支，我们需要决定是否有一个输入能够让程序在一条分支上执行另一条路径（更准确地说，我们考虑整个控制流路径而非单个路径），这帮助我们在程序中寻找可以让我们通过调整输入来影响的控制流条件，所有的符号执行系统都基于 SMT 求解器来完成这些工作
• 我们需要确定我们在测试中寻找的是什么，这是我们从程序中确保 不变量 （invariant）来考虑的最佳方法，而符号执行寻找改变这些常量的输入（👴也没咋读明白，可以看实验手册原句）；我们可以寻找的事物之一是程序崩溃（crashes，即不变量是 我们的程序不应当崩溃 ），在 C 程序中这非常有意义，因为 crashes 通常指示了代表漏洞的内存损坏，在 Python 这样更高级的语言中在设计上并不存在内存损坏，但我们仍然可以寻找如 Python 代码级的代码注入攻击（例如 eval() ）或是特定于某种应用的影响安全的不变量
• 最终，对于给出程序中所有可能执行的控制流路径，我们需要决定该尝试哪条路径，因为路径数量会随着程序规模的增大而快速增长，我们不可能尝试所有的路径，因此符号执行系统通常包含确定哪一条路径更有希望发现破坏不变量的某种 调度器 （scheduler）或 搜索策略 （search strategy），一个简单的搜索策略例子便是尝试未执行过的路径，这代表着更高的代码覆盖率与未被发现的漏洞的存在的可能性

• 若我们的 concolic system 知道应用的行为，我们可以像符号执行那样运行（除了我们还会同时传播每个值的 concrete 部分）；例如，假设我们有两个 concolic 整型变量 aabb，其有着具体值 56 ，并对应符号表达式 ab，此时若应用创建了一个变量 cc = aa + bb，其会同时有着具体值 11 及符号表达式 a + b；类似地，若应用在 cc == 12 的分支上执行，程序可以像分支为假一样执行，并记录对应的符号分支条件 a + b != 12
• 若我们的 concolic system 不知道应用的当前行为，应用将只会得到具体的值；例如若应用将 cc 写入文件中，或者是传递到外部库中，代码仍可以使用具体值 11 如同应用正常运行那样继续执行

## Concolic execution for integers

• 抽象语法树（The AST）：与此前我们在 int-avg.py 中使用 Z3 表达式来表示符号值所不同的是，本 Lab 构建了其自己的抽象语法树（abstract syntax tree）来表达符号表达式，一个 AST 节点可以是一个简单的变量（ sym_strsym_int 对象）、一个常量（const_intconst_strconst_bool 对象）、或是一些将其他 AST 节点作为参数的函数或操作符（例如 sym_eq(a, b) 表示布尔表达式 a==b，其中 ab 都是 AST 节点，或是 sym_plus(a, b) 表示整型表达式 a + b

每个 AST 节点 n 都可以使用 z3expr(n) 转化为 Z3 表达式，这由调用 n._z3expr 完成，即每个 AST 节点都实现了返回对应 Z3 表达式的 _z3expr 方法

我们使用自己的 AST 层而非使用 Z3 的符号表示的原因是因为我们需要实现一些 Z3 表示难以完成的操作，此外我们需要分出一个独立的进程来调用 Z3 的求解器，以在 Z3 求解器耗时过长时杀死进程——将约束归为不可解（这种情况下我们可能失去这些路径，但至少我们会让程序探索其他路径）；使用我们自己的 AST 能让我们将 Z3 状态完全独立在 fork 出的进程里

• 混合封装（The concolic wrappers）：为了拦截 python-level 的操作并进行混合执行，我们将常规的 intstr 对象替换成了混合的子类：concolic_int 继承自 intconcolic_str 继承自 str，每一个混合封装都同时存储一个具体值（self.__v ）与一个符号表达式（与 AST 节点，在 self.__sym），当应用在计算混合值表达式（例如 a+1 中的 aconcolic_int），我们需要拦截该操作并返回一个同时包含具体值与符号表达式的的混合值

为了实现这样的拦截操作，我们重载了 concolic_intconcolic_str 类中的一些方法，例如 concolic_int.__add__ 在上面的例子 a + 1 中会被调用并返回一个新的混合值表示结果

原则上我们应该也要有一个 concolic_bool 作为 bool 的子类，不幸的是在 Python 中 bool 不能被继承（参见这里这里），于是我们创建了函数 concolic_bool 作为代替，当我们创建一个混合布尔值时，程序会按其值进行分支，故 concolic_bool 也会为当前路径条件添加一个约束（布尔值的符号表达式与具体值相等的约束），并返回一个具体的布尔值

• 具体输入（The concrete inputs）：在混合执行下被测试的程序输入都存储在 concrete_values 字典中，在该字典中存储了程序输入的字符串名字，并将每个名字映射到对应的输入值（整型变量的值为python整型，字符串变量为python字符串）

concrete_value 被设为全局变量的原因是应用通过调用 fuzzy.mk_str(name)fuzzy.mk_int(name) 来创建一个混合字符串或混合整型，其返回一个混合值，其中的符号部分为一个新的 AST 节点对应到一个名为 name 的变量，但具体值被在 concrete_values 中查找，若字典中没有与之关联的变量，系统将其设为默认的初始值（整型为0，字符串为空串）

混合执行框架在一个 InputQueue 对象中维持一个待尝试的不同输入的队列，框架首先会添加一个初始输入（空字典 {}），之后执行代码，若应用进入了分支，混合执行系统将唤醒 Z3 来带来 新的输入以测试代码中的其他分支，将这些输入放到输入队列中，并保持迭代直到没有输入可以尝试

• 可满足性模理论求解器（The SMT solver）： fork_and_check(c) 函数会检查约束 c （一个 AST 节点）是否为可满足的表达式，并返回一对值：可满足性状态 ok 及示例模型（分配给变量的值），若约束可以被满足则 okz3.sat ，若约束不可被满足则 okz3.unsatz3.unknown；该函数内部会 fork 一个独立的进程来运行 Z3 求解器，若耗时超过 z3_timeout 则杀死进程并返回 z3.unknown

• 当前路径条件（The current path condition）：当应用执行并基于混合值决定控制流时（参见上面关于 concolic_bool 的讨论），表示该分支的约束会被添加到 cur_path_constr 列表中，为了生成能够沿着一条分支从一个点进行不同选择的输入，所需的约束为路径上该点之前的约束集合，加上该点的反向约束；为了帮助调试与启发式搜索，触发了分支的代码行的信息会被存放在 cur_path_constr_callers 列表中

### 混合执行框架代码浅析 - Part 1

#### V. 混合变量

Exercise 2. Finish the implementation of concolic_int by adding support for integer multiply and divide operations. You will need to overload additional methods in the concolic_int class (see the documentation for operator functions in Python 3), add AST nodes for multiply and divide operations, and implement _z3expr appropriately for those AST nodes.

Look for the comments Exercise 2: your code here in symex/fuzzy.py to find places where we think you might need to write code to solve this exercise.

Run ./check-concolic-int.py or make check to check that your changes to concolic_int work correctly.

• 首先判断运算对象是否为 concolic_int ，若是则将自身具体值加上对象具体值，否则直接加上该对象，结果存放到 res
• 创建一个新的 concolic_int 实例作为返回值，res 作为其具体值部分，创建两个 ast 实例并利用 sym_plus() 计算结果作为新 concolic_int 的符号值部分

Exercise 3. An important component of concolic execution is concolic_exec_input() in symex/fuzzy.py. We have given you the implementation. You will use it to build a complete concolic execution system. To understand how to use concolic_exec_input(), you should create an input such that you pass the first check in symex/check-symex-int.py. Don’t modify symex/check-symex-int.py directly, but instead modify symex_exercises.py. Run ./check-symex-int.py or make check to check your solution.

### 混合执行框架代码浅析 - Part 2

#### VI.具体值字典 - ConcreteValues

symex/fuzzy.py 中有一个全局变量 current_concrete_values，实际上就是我们前面所说的全局具体值字典，我们可以使用ConctreteValues.mk_global() 使该对象变为全局引用，即我们每次使用只需要创建一个ConctreteValues 对象即可：

#### VII. concolic_exec_input() - 输入执行

• 初始化两个全局空列表 cur_path_constr当前路径的条件约束）与 cur_path_constr_callers（当前路径的信息）
• 调用 concrete_values.mk_global() 使其成为一个全局字典
• 调用传入的函数指针来获得一个值 v，若参数 verbose > 1 则打印两个列表的内容
• 最后的返回值为 (v, cur_path_constr, cur_path_constr_callers)

concolic_bool() 实际上在 concolic_intconcolic_str 的运算符重载中进行调用，这也是为什么每次执行 concolic_exec_input() 都要重新将路径约束与信息列表清空的缘故，这里以 concolic_int 中的 __cmp__ 运算符为例：

Exercise 4. Another major component in concolic execution is finding a concrete input for a constraint. Complete the implementation of concolic_find_input in symex/fuzzy.py and make sure you pass the second test case of symex/check-symex-int.py. For this exercise, you will have to invoke Z3, along the lines of (ok, model) = fork_and_check(constr) (see the comments in the code). Run ./check-symex-int.py or make check to check your solution.

• 创建子进程调用 fork_and_check_worker() 进行约束求解，父子进程通过管道通信
• 父进程等待子进程的 SIGALRM 信号，若 z3_timeout 秒后未收到，杀死子进程
• 从管道接收结果并返回，若超时（子进程被杀，管道关闭）则返回 (z3.unknown, None)

• 新建一个 Z3 求解器将转化为字符串的约束表达式传入，调用 Solver.check() 求解
• 若求解成功，调用 Solver.model() 获得求解结果
• 判断结果中变量类型并转换为整型/字符串，对于字符串做额外处理，将结果放到一个 字符串→结果 映射的字典中并返回

Z3 这玩意用起来确实方便，不愧是微软大爹

Exercise 5. A final major component in concolic execution is exploring different branches of execution. Complete the implementation of concolic_force_branch in symex/fuzzy.py and make sure you pass the final test case of symex/check-symex-int.py. Run ./check-symex-int.py or make check to check your solution.

Exercise 6. Now implement concolic execution of a function in concolic_execs() in symex/fuzzy.py. The goal is to eventually cause every every branch of functo be executed. Read the comment for a proposed plan of attack for implementing that loop. The functions in the exercises 3-5 should be quite useful.

Run ./check-symex-int.py or make check to check that your concolic_execs() works correctly.

Beware that our check for this exercise is not complete. You may well find that later on something does not work, and you will have to revisit your code for this exercise.

• checked 为已经检查过的约束，outs 为最后求解所得结果，inputs 为待测试输入队列（输入为具体值字典）
• 由一个大循环持续调用concolic_exec_input() 计算约束
• 将新的约束解添加到结果中

• concolic_exec_input(testfunc, concrete_values, verbose = 0)：将 concrete_values 参数设为全局字典，之后执行给定的函数 testfunc，返回执行的结果值、分支条件列表、分支调用信息列表
• concolic_find_input(constraint, ok_names, verbose=0)：使用 Z3 求解给定约束，返回 ok_names 列表中变量的值
• concolic_force_branch(b, branch_conds, branch_callers, verbose = 1)：对给定约束条件 branch_conds 与分支 b，返回走向该分支另一路径的约束

• 迭代 concolic_exec_input() 所返回的分支集合
• 使用 concolic_force_branch() 来构建一个分支的另一路径约束
• 若约束已经在 check 集合中，将其跳过，否则加入集合中
• 使用 concolic_find_input() 以构建一个基于另一路径约束的新的测试输入
• Z3 可能不会为每个变量分配值（例如变量可能与约束无关），我们需要从上次使用的字典继承到 concolic_find_input() 返回的新字典中，将新的字典添加到 input 队列中

## Concolic execution for strings and Zoobar

Exercise 7. Finish the implementation of concolic execution for strings and byte-arrays in symex/fuzzy.py. We left out support for two operations on concolic_str and concolic_bytes objects. The first is computing the length of a string, and the second is checking whether a particular string a appears in string b (i.e., a is contained in b, the underlying implementation of Python’s “a in b” construct).

Look for the comment Exercise 7: your code here to find where you should implement the code for this exercise. We have already implemented the sym_contains and sym_length AST nodes for you, which should come in handy for this exercise.

Run ./check-concolic-str.py and ./check-symex-str.py (or just run make check) to check that your answer to this exercise works correctly.

Exercise 8. Figure out how to handle the SQL database so that the concolic engine can create constraints against the data returned by the database. To help you do this, we’ve written an empty wrapper around the sqlalchemy get method, in symex/symsql.py. Implement this wrapper so that concolic execution can try all possible records in a database. Examine ./check-symex-sql.py to see how we are thinking of performing database lookups on concolic values.

You will likely need to consult the reference for the SQLalchemy query object to understand what the behavior of get should be and what your replacement implementation should be doing.

Run ./check-symex-sql.py (or just run make check) to check that your answer to this exercise works correctly.

test_f() 中会调用 test1_setup() 进行数据库 "test1" 的创建，并创建一个混合字符串 s，将其作为参数给到数据库的 get 函数：

Lab 已经实现了的一个不变量便是 eval injection——即对 eval() 的参数进行注入，在 symex/symeval.py 中 Lab 给出了对这种情况的检查思路：若传给 eval() 的字符串可以包含 ;badstuff(); ，说明我们发现了一个 eval injection 漏洞——由此我们可以让混合执行系统去尝试构建能包含该子串的字符串

• 若没有新用户被注册，则所有用户的 Zoobar balances 之和应当在每次请求间保持一致
• 若用户 u 没有向 Zoobar 进行请求，u 的 Zoobar balance 不应当缩小

Exercise 9. Add invariant checks to check-symex-zoobar.py to implement the above two rules (total balance preservation and no zoobar theft). Look for the comment Exercise 9: your code here to see where you should write this code. When you detect a zoobar balance mismatch, call the report_balance_mismatch() function. When you detect zoobar theft, call report_zoobar_theft().

Recall that our check for exercises 3-6, where you implemented the core of the concolic execution system, was not complete. If you are having trouble with this exercise, it may be that you did not implement exercises 3-6 correctly, so you may need to go back and fix it.

To check whether your solution works correctly, you need to re-run ./check-symex-zoobar.py and see whether the output contains the messages WARNING: Balance mismatch detected and WARNING: Zoobar theft detected. Alternatively, you can run make check, which will do this for you (run check-symex-zoobar.py and look for these magic strings).

test_stuff() 开头便对应创建了两个数据库，因此我们可以从其定义入手：

zoobar/zoodb.py 中定义了 Person 数据库，其中 balance（也就是 zoobars 字段）的初始值为 10，同时主键为 username

Exercise 10. Fix the two bugs you found in Exercise 9, by copying whatever .py files you need to modify from the zoobar directory to zoobar-fixed and changing them there.

Recall that our check for exercises 3-6, where you implemented the core of the concolic execution system, was not complete. If you are having trouble with this exercise, it may be that you did not implement exercises 3-6 correctly, so you may need to go back and fix it.

To check whether your solution works correctly, you need to run ./check-symex-zoobar-fixed.sh and see whether the output still contains the messages Exception: eval injection, WARNING: Balance mismatch detected and WARNING: Zoobar theft detected. Alternatively, you can run make check, which will do this for you.

• 由一个外层大循环不断迭代
• 从输入队列中取出具体值字典
• 调用 concolic_exec_input() 执行目标函数，获取到返回值、分支条件列表、分支调用方列表
• 将得到的新的返回值添加至 outs 集合
• 内层小循环遍历分支条件列表
• 调用 concolic_force_branch() 获取将当前分支条件逆转后的约束条件
• 若该约束不在 checked （已验证约束集合）中，添加，并调用 concolic_find_input() 进行约束求解
• 约束可解，将结果添加到下一次作为输入的具体值字典中

• 未对负数的 transfer 进行过滤，导致一个用户可以盗取另一用户的 balance
• 未对 self-transfer 的情况做合适处理，导致最后总的 balance 不一致

• 缺失了对 transfer 数量为负的检查
• 重复赋值导致对 self-transfer 的情况计算错误

# 0x04.Lab 4: Browser security（uncompleted）

## Introduction

• Part 1：跨站脚本攻击（cross-site scripting attack，XSS）
• Part 2：侧信道与钓鱼攻击（side channel and phishing attack）
• Part 3：一个简单的蠕虫（a profile worm）

## Part 1: a cross-site scripting (XSS) attack

Cookies are HTTP’s main mechanism for tracking users across requests. If an attacker can get ahold of another user’s cookie, they can completely impersonate that other user. For this exercise, your goal is simply to print the cookie of the currently logged-in user when they access the “Users” page.

2. Save a copy of zoobar/templates/users.html (you’ll need to restore this original version later). Add a <script> tag to users.html that prints the logged-in user’s cookie using alert()

Your script might not work immediately if you made a Javascript programming error. Fortunately, Chrome has fantastic debugging tools accessible in the Inspector: the JavaScript console, the DOM inspector, and the Network monitor. The JavaScript console lets you see which exceptions are being thrown and why. The DOM Inspector lets you peek at the structure of the page and the properties and methods of each node it contains. The Network monitor allows you to inspect the requests going between your browser and the website. By clicking on one of the requests, you can see what cookie your browser is sending, and compare it to what your script prints.

3. Put the contents of your script in a file named answer-1.js. Your file should only contain javascript (don’t include <script> tags).

【EXPR.0x01】MIT 6.858 课程实验报告
http://blog.arttnba3.cn/2022/12/25/EXPR-0X01-MIT_6_858/

arttnba3

2022年12月25日