To-Read-List

SOSP'21

• Session 13: Scheduling

• Session 17: Storage

• Session 18: Verification

Kernel Concurrency Testing

Input Generation

SOSP'21 - HEALER

Key Idea ：考虑系统调用之间的 influence relation ，即一个 syscall 的执行是否会影响后续 syscall 的执行行为，并利用 influence relation 实现 guided fuzzing 。

HEALER 为每个系统调用序列 $C$ 构建一个 $n \times n$ 的布尔矩阵，$R_{ij} = 1$ 表示 $C_i$ 是否执行会改变 $C_j$ 的 execution trace 。

HEALER 从两方面“学习”出 influence relation 矩阵：

• static learning ：若 $C_i$ 的返回值类型和 $C_j$ 的参数类型是 compatible 的，则令 $R_{ij} = 1$ 。

• dynamic learning ：首先在 coverage 不变的前提下尽可能将系统调用序列最小化，然后对每个 $C_i$ ，观察在跳过 $C_i$ 的情况下 $C_{i + 1}$ 的 coverage 是否变化。只考虑直接后继的原因是避免将间接影响纳入 influence relation 中。

在 fuzzing 过程的前期，influence relation 还未包含足够的信息，不具有指导意义，因此会更多地随机选择 syscall ，此概率随迭代次数的增加而逐渐减小。

---

Ideas from Other Related Works

Model Checking

punctuated search (EuroSys19_DSLabs) ：首先搜索满足某些谓词约束的状态，然后以这些中间状态为起点重新开始搜索，以期扩大搜索深度。使用谓词约束也可以让 model checker 针对特定类别的错误。

runtime snapshot (NSDI09_CrystalBall) ：在实际运行系统的同时保存快照发送给 model checker 。

consequence prediction (NSDI09_CrystalBall) ：对局部状态空间进行搜索和记忆，如果外部事件没有影响到区域内部，则无需重新搜索。

prefix-based search (NSDI07_MaceMC) ：先执行一长段路径，然后再开始 model checking 。

exhausted search with biased random walks (NSDI07_MaceMC) ：为实践中更可能发生的事件设置更高的优先级，反直觉，但事先的 exhausted search 已使其逼近 corner case 。

state hashing (ASE00_JPF, OSDI02_CMC)

down-scaling (OSDI02_CMC) ：限制被测系统的规模，例如限制网络中的路由节点的数量。这可能更容易发现那些由少数进程之间的复杂交互导致地方错误，但是会遗漏那些仅在大规模系统中才会出现的错误。

state abstraction (OSDI02_CMC) ：消除用户认为对检查属性没有帮助的信息。在计算状态的哈希签名时忽略对应的内存位置即可。这可能会产生漏报，但不会产生误报。

compare-and-check (OSDI04_FiSC) ：为被测系统建模一个抽象的正确系统，验证相同输入下二者的状态一致性。

recover state with calculation (OSDI06_EXPLODE) ：EXPLODE 使用计算而不是复制来恢复状态，它将被测系统到达状态 $S$ 的选择序列作为 $S$ 的检查点，并从干净的初始状态开始 replay 选择序列以恢复状态 $S$ 。此方法假设被测系统是 deterministic 的，并且会破坏系统的时间戳属性。

PCT 专注于概率性地查找特定深度 $d$ 的错误。此外，PCT 的设计旨在为深度较小的错误提供更好的保证。

irrelevant component elimination ：Bandera / program slicing 或 chopped symbolic execution 。

Fuzz Testing

Model-Based Testing Survey

ASE'07 - A Survey on Model-based Testing Approaches - A Systematic Review