G.O.S.S.I.P 阅读推荐 2023-05-10

又到了 G.O.S.S.I.P和朋友 专栏时间（这个栏目以后一定会越来越红火！），今天介绍这篇在IEEE S&P 2023发表的论文 Finding Specification Blind Spots via Fuzz Testing 来自加拿大滑铁卢大学徐萌研究组的博士生纪儒，她是在G.O.S.S.I.P实习期间，通过公众号了解到了徐老师，然后成功申请，旋即博士生的第一个研究工作就拿到了IEEE S&P的录用，让我们对她和徐萌老师表示热烈祝贺！接下来我们就来看看这篇论文~

背景

形式化验证通过数学方法给系统提供高效的正确性保障。通常应用形式化验证的场景包括 1) 错误会导致严重的损失和无法挽回的后果（e.g. 航空领域）。2) 传统的系统更新模式在该系统下不可行（e.g. 智能合约）。

在一个系统上使用形式化验证可以被大体分为两个步骤 1）为目标系统开发一组完整的specification（下文简称spec）。2）验证implementation（下文简称code）是否和spec相符。

近些年出现了许多基于2）的工作，例如优化的SMT/SAT solver，新的prover框架，SMT/SAT的安全性分析等等。但是一个可能被忽略的重要问题是，在一个完美的验证链下，程序最多只能和spec一样正确，也就是说spec中的一个blind spot可以轻松破坏对验证链的工作。

Motivation Example

下面给出本文的一个motivation example。

在这个例子中，add1函数的功能是在一个list中循环遍历并给里面的每一个元素加一。右侧的spec的功能是规定并验证在add1函数执行结束后，list里面的每一个元素跟进入add1之前相比已经被加一。

这里的spec是有缺陷的，你能看出来问题吗？

揭晓答案是spec没有specify list的长度，所以即使code在加一操作结尾pop出一个元素，这个code仍然可以通过验证。

我们修复的方法也很简单，在spec中加一个ensures限制进入函数前后list的长度保持一致。

方法

看了上面这个例子之后，可能很容易会想到只要用类似的mutation方法，就可以找到更多的blind spot了，但是实际应用起来其实需要考虑更多的问题。我们先看一个枚举的case study。

Enumerative code mutant generation

我们在Diem Payment Network (DPN)上使用枚举的方法进行mutation testing。DPN使用Meta开发的智能合约语言Move编写的支付系统。Move语言自带形式化验证工具Move Prover。

首先第一步我们收集所有可以mutate的location。为了保证每一次生成的mutant都是有效的mutant，mutation作用于compiler中的typing步骤之前。在这里我们的upper bound 设置为3，也就是最高我们允许三个location合并组成的mutant。

通过这个例子我们也可以看出enumerative generation的问题，mutant的数量是exponential的。如果把n定义为可能做mutation的location数目，在不考虑每一个location可能会有多种mutation target的情况下，mutant的数量已经是2^n（其中n≥number of instructions）。在这个例子中DPN codebase里面的location数目为404。通过这个问题我们引出了下一个case study:

Evolutionary code mutant generation

我们在AWS的轻量TLS实现库s2n-tls上实现了我们的第二个case study。s2n-tls使用Software Analysis Workbench script(SAW script)进行形式化验证。值得注意的一点是s2n-tls中的mutation location有6772个。

我们从coverage-based fuzzing中汲取灵感。通常的fuzzing程序中，我们不断向目标程序输入unexpected input，并期望能够trigger出程序中的unsafe behaviour。在这个case中，unexpected input是被mutate过的code，unsafe behaviour是mutant通过验证，我们的目标是尽快找到一个可以通过验证的mutant。

在evolutionary mutant generation中，具体实现步骤如下：

Pre-collection - 首先我们收集所有可能的mutation location，放入random mutant的集合里面。

Initialization - 初始化seed pool — 第一个seed设置为没有任何mutation的原始code，并且同时赋予一个较高分数，目的是给整个程序一个初始动量推动。

Each round - 在每一轮中，我们的mutant由两部分构成 — 1) seed pool里面分数最高的seed 2) 从random mutants中选择的一个random mutant。我们把这个mutant交给验证工具并且收集结果。如果验证失败，我们收集error信息。如果验证成功，我们记录下这个mutant，并且交给下一个部分的内容判断这个blind spot是intentional or mistaken。

Fitness evaluation - 一个mutant在两个条件之下被定义为fit: （相对于seed而言）1)mutant减少了验证的error数 2) mutant触发了之前没有出现过的error。

Seed Registration - 在每一次verification结束之后，通过上述evaluation方法判断一个seed是否fit，一个fit的mutant会被加入seed pool。

Seed Scheduling - 如果基于一个seed产生了fit的mutant，那么给这个seed加分，反之扣分。

Intention or Mistaken?

方法介绍至此，可能会造成一种找到通过verification的mutant是最终目的的错觉，然而事实并非如此，一个简单的例子：

spec规定一个排序函数，但排序函数的具体使用方法并不做具体要求（比如quick sort和merge sort都可以），这时候如果我们的mutation从一种排序方法跳转到另一种排序方法，并且mutant通过了验证，这其实是一个开发者故意留下（intentional）的blind spot。

从这个思路出发，我们把mutant通过验证的情况总共归结为三类，如下图所示：

绿色：mutant通过验证，mutant通过test，(spec与code之间产生的)gap在test中被明显允许 —> 此发现的blind spot是by design。

黄色：mutant通过验证，mutant通过test，gap没有在test中被定义 —> 我们无法确定这个gap的意图，需要手动验证确认。

蓝色：mutant通过验证，mutant没有通过test —>这个gap是一个mistake。

结果

在DPN中我们确认了13个case，在s2n-tls中确认了21个case。所有确认的case提供了修复/报告。详细内容参见paper。

通用性与展望

FAST被实现在两个case study中。但是本文更想提供FAST作为一种architecture，可以被运用到更多的形式化验证的系统中。在其他系统中使用FAST需要两个条件：1) 验证系统是完全自动化的（Coq等交互式验证系统不可用）2）FAST可以改动一些code representation（比如LLVM IR）。

我们希望FAST的结果能吸引到更多对于形式化验证系统的spec质量的关注。

论文：https://cs.uwaterloo.ca/~m285xu/assets/publication/fast-paper.pdf

原文始发于微信公众号（安全研究GoSSIP）：G.O.S.S.I.P 阅读推荐 2023-05-10