论文:ZHENHUA DUAN and LIANG ZHAO, “Differential Testing of Certificate Validation in SSL/TLS Implementations: An RFC-guided Approach”.

问题背景-前置知识

数字证书是现代互联网中个体间相互信任的基石,是网络安全中的一个非常重要组成部分,如果没有数字证书,那么也没有了各式各样的电商平台以及方便的电子支付服务。数字证书有很多格式版本,主要有X.509v3(1997)、X509v4(1997)、X.509v1(1988)等。比较常用的版本是x.509V3。

为什么需要数字证书

防止伪造公钥,即确认公钥确实是特定某人的公钥。试想这样一种场景:

Bob有公钥和私钥,他将公钥分发给两个朋友:Alice,Eve。Bob决定给Alice写信,他写完后先用Hash函数,生成信件的摘要(digest),然后Bob用私钥,对这个摘要加密,生成”数字签名”(signature),这个签名,附在信件下面,一起发给Alice。Eve想欺骗Alice,他访问了Alice的电脑,用自己的公钥换走了Bob的公钥。此时,Alice实际拥有的是Eve的公钥,但是还以为这是Bob的公钥。因此,Eve就可以冒充Bob,用自己的私钥做成”数字签名”,写信给Alice。

Alice想到了一个办法,要求Bob去CA,为公钥做认证。证书中心用自己的私钥,对Bob的公钥和一些相关信息一起加密,生成”数字证书”(Digital Certificate)。这样避免了上述问题的发生。

X.509数字证书数据格式

使用https协议的网站都可以查看证书,chrome为例,F12切security可以查看证书:

黄色图标为关键信息,有如下内容:

  • 版本:识别用于该证书的 X.509 标准的版本,这可以影响证书中所能指定的信息。迄今为止,已定义的版本有三个。知乎为例:X.509v3
  • 序列号:发放证书的实体有责任为证书指定序列号,以使其区别于该实体发放的其它证书,如果某一证书被撤消,其序列号将放到证书撤消清单 (CRL) 中。知乎为例:0e3cc14994b3e174a63454d9906466d7
  • 签名算法:用于识别 CA 签写证书时所用的算法。知乎为例:sha256RSA

  • 颁发者:颁发证书的实体的 X.500 名称,它通常为一个 CA。递归上溯知道root CA可以得到证书链。知乎为例:CN = GeoTrust RSA CA 2018。

  • 有效期:每个证书均只能在一个有限的时间段内有效。知乎为例:‎2017‎年‎12‎月‎25‎日 8:00:00-‎2020‎年‎12‎月‎24‎日 20:00:00
  • 使用者主体名:证书可以识别其公钥的实体名。此名称使用 X.500 标准,因此在Internet中应是唯一的。知乎为例:CN = *.zhihu.com OU = IT O = 智者四海(北京)技术有限公司 L = 北京市 C = CN
  • 主体公钥信息:这是被命名实体的公钥,同时包括指定该密钥所属公钥密码系统的算法标识符及所有相关的密钥参数。

https通信中使用这两种格式的整数文件,cer/crt使用二进制存储,pem使用ascii码。

Internet X.509 PKI 数字证书在RFC5280中详细描述。下面是RFC5280用ASN.1语言(一种形式化语言 https://www.jianshu.com/p/44e6a9e1fbe2语法格式介绍 )定义的证书格式。

“`ASN.1
Certificate ::= SEQUENCE {
tbsCertificate TBSCertificate, –证书主体–
signatureAlgorithm AlgorithmIdentifier, –签名算法–
signatureValue BIT STRING –证书签名值–}

TBSCertificate ::= SEQUENCE {
version [0] EXPLICIT Version DEFAULT v1,–证书版本号–
serialNumber CertificateSerialNumber,–证书序列号–
signature AlgorithmIdentifier,–签名算法–
issuer Name,–发行者名称–
validity Validity,–有效期–
subject Name,–证书主体–
subjectPublicKeyInfo SubjectPublicKeyInfo,–证书公钥–
issuerUniqueID [1] IMPLICIT UniqueIdentifier OPTIONAL,
— If present, version MUST be v2 or v3
subjectUniqueID [2] IMPLICIT UniqueIdentifier OPTIONAL,
— If present, version MUST be v2 or v3
extensions [3] EXPLICIT Extensions OPTIONAL
— If present, version MUST be v3
}

Version ::= INTEGER { v1(0), v2(1), v3(2) }

CertificateSerialNumber ::= INTEGER –序列号声明–

Validity ::= SEQUENCE {–起止日期声明–
notBefore Time,
notAfter Time }

Time ::= CHOICE {–时间声明–
utcTime UTCTime,
generalTime GeneralizedTime }

UniqueIdentifier ::= BIT STRING

SubjectPublicKeyInfo ::= SEQUENCE {–公钥信息声明–
algorithm AlgorithmIdentifier,
subjectPublicKey BIT STRING }

Extensions ::= SEQUENCE SIZE (1..MAX) OF Extension

Extension ::= SEQUENCE {–扩展信息–
extnID OBJECT IDENTIFIER,
critical BOOLEAN DEFAULT FALSE,
extnValue OCTET STRING
— contains the DER encoding of an ASN.1 value
— corresponding to the extension type identified
— by extnID
}

<pre><code class=""><br /><br /><br />### 符号执行工具KLEE的使用

KLEE是一个符号执行工具,它会为探索到的路径生成相应的测试用例(这篇文章中即是生成的证书),这也是这篇文章使用它的原因,这有助于使用测试用例复现问题定位bug。KLEE通过插入函数调用(klee_make_symbolic)对内存进行符号化。并且跟踪符号内存的使用,并收集使用这些符号内存的约束。使用符号内存的其他内存,该内存也将会被符号化。当遇到一个使用符号化内存的分支时,KLEE会将执行状态一分为二,看看分支的哪一边可以找到一个可以满足符号约束的解。

#### KLEE的安装

“`sh
docker pull klee/klee:2.0 docker run –rm -ti –ulimit=’stack=-1:-1′ klee/klee:2.0

(这里需要换源安装一下vim)

使用KLEE进行第一个测试

在这个程序中有五中错误,模零、除零、数组越界、空指针、free后指针未置零,根据a的不同值共有六条路径。

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

void kleeTest(int a){
    int arr[10];
    int d[10];

    for (int i = 0; i < 10; i++){
        arr[i] = i;
    }

    if (a == '1'){ // mod zero
        for (int i = 0; i < 10; i++){
            int num = i;
            d[i] = arr[i] % num;
        }
    }
    else if(a == '2'){  // divide zero
        for (int i = 0; i <= 10; i++){
            int num = i ;
            d[i] = arr[i] / num;
        }
    }
    else if (a == '3'){  // pointer out of bound
        for(int i = 0; i<= 11; i++){
            arr[i] = i;
        }
    }
    else if (a == '4'){  // null pointer
        int *a = NULL;
        int b = *a + 1;
    }
    else if(a == '5'){  // leak memory
        free(arr);
    }
}

int main(){
    int n;
    klee_make_symbolic(&n, sizeof(n), "n");
    kleeTest(n);
    return 0;
}
$ clang -I ../../include -emit-llvm -c -g mytest.c
$ klee mytest.bc

执行之后,可以看到klee生成了6个测试用例:

klee@debe62de6d36:~/test$ cat ./klee-last/
assembly.ll          run.istats           test000001.kquery    test000002.ktest     test000003.kquery    test000005.div.err   test000006.kquery    warnings.txt
info                 run.stats            test000001.ktest     test000002.ptr.err   test000003.ktest     test000005.kquery    test000006.ktest     
messages.txt         test000001.div.err   test000002.kquery    test000003.free.err  test000004.ktest     test000005.ktest     test000006.ptr.err 

以及每个测试用例相应发生的错误信息。

前人相关研究

SSL/TLS实现中的证书验证是不一定安全的,需要进行软件测试。问题的关键在于如何足够高效的生成测试用例-即大量的数字证书。

1、由于数字证书的复杂性以及语义限制,应用Fuzzing产生的测试用例十分低效,因为太多的用例根本不符合数字证书的结构。
2、NEZHA和SymCerts方法使用符号执行提取出路径约束,以发现不符合X.509标准的情况,但是这都依赖于程序必须是开源的。
3、Frankencert和Mucert采用遗传算法来生成测试用例,它依赖于一开始的一个种子测试用例,随后迭代的变异产生新的相似测试用例。它们的缺点在于种子测试用例难以选择以及变异算子设计的巧妙性,尽管它们的适应度均是以代码覆盖率为目标,但是实际情况并不好,同时这种方法无法指出确切问题的所在,只能使用生成的错误用例进行人工分析。
4、 Korat采用一种方法:使用前提条件来生成测试用例,然后使用后置条件作为测试预期输出来检查程序的正确性。 TestEra生成Java程序作为违反标准的反例。 Pandita等,提出了一种从API文档的自然语言文本中推断形式规范的新颖方法。肖,提出了一种名为Text2Policy的方法来自动从自然语言软件文档中提取访问控制策略,并从自然语言的需求文档中提取资源访问信息。
5、受上述基于规范的方法的启发,RFCcert利用动态符号执行和组合技术生成基于RFC标准的的证书,克服了传统的缺点。 使用该方法,与通过FrankencertMucert等遗传方法生成的变异证书相比,由RFCcert生成的证书更具有针对性。 实验结果表明,RFCcertmRFCcertSSL/TLS实现中显着改善了证书验证的测试。 此外,RFCcert可以扩展到其他的基于RFC的测试。

RFCcert方法概述

方法整体流程如下图所示,它首先从RFC文档中提取出规则,将规则形式化为变量,再依据这些产生出一个c语言程序,进而由klee符号执行工具产生测试用例,把这些测试用例组装为证书,去测试程序。

从RFC文档中提取规则

根据RFC2119定义的RFC语言标准,对文档RFC5280和RFC6818进行分析提取。

对于ASN.1语言比较好理解,对于自然语言(下面称NL),RFC2119定义了一些特定单词:

The modal key words include:
(1) absolute requirements or prohibitions of specifications: MUST, REQUIRED, SHALL, MUST
NOT, and SHALL NOT;
(2) requirements or prohibitions with flexibility: SHOULD, RECOMMENDED, SHOULD NOT,
and NOT RECOMMENDED; and
(3) truly optional items: MAY and OPTIONAL.

算法1是一个简单的程序,将有规则意义的句子(NL),语言块(ASN.1)从文档中提取出来。下图示,第一行定义了NL中句子的划分符,第二行定义了ASN中语言块的划分符,第三行定义了关键单词,第四行初步处理RFC文档。下面循环按照section和title将包含关键单词的句子和语言块提出来保存到ruleSet文本文件。

从一个RFC文档更新规则

RFC6818作为RFC5280的更新文档,Updates to the Internet X.509 Public Key Infrastructure Certificate and Certificate Revocation List (CRL) Profile。依据RFC文档的规范,必须是“… paragraph says: ….”,然后替代为“This paragraph is replaced with:…”,依据这个规则,算法2对规则进行更新。

第三行到第十行把新旧规则用矩阵表示,第十一行到二十行遍历矩阵,更新规则。

生产者消费者规则

CA在颁发证书时应遵循的规则称为生产者规则,而证书在验证过程中必须遵循的规则是消费者规则。存在既是生产者规则又是消费者规则的规则,这些规则称为共享规则。 SSL / TLS实现中的证书验证应符合所有与消费者相关的规则。因此,在RFCcert方法中,要考虑消费者规则和共享规则。算法3将更新后的规则分为生产者规则,消费者规则和共享规则。

进一步划分为breakable和unbreakable

将规则表达为变量

一方面,很难根据这些规则直接自动生成证书,另一方面,手动获取组合规则很容易出错。为了克服这个问题,RFCcert在第二步执行DSE,以自动执行证书生成过程。为此,规则需要表示为变量。

根据约束条件,将这些规则转换为变量。该转换由算法5完成,该算法包括三个步骤。第一步,收集构成规则主干的关键单词。第二步利用关键单词简化规则。第三步生成NL和ASN.1规则的组合约束。

Example 3. “In addition, applications conforming to this profile SHOULD recognize the ‘authority’
and ‘subject key identifier’ and ‘policy mappings’ extensions.”
Example 4. “This field MUST contain the same algorithm identifier as the ‘signature’ field in the
sequence ‘tbsCertificate’.”

这两个例子对应生成的变量为:

Example 3. authorityKey- Identifier_present_subjectKeyIdentifier_present_policyMappings_present__applications_ SHOULDrecognize
Example 4. tbsCertSignature_present__signatureAlgorithm_MUSTsame and explicitText_More than200chars__certUsers_SHOULDhandle

使用正则表达式对算法1到算法5重写

….略,这里算法6-算法10是使用正则表达式的与上述算法功能相同的描述。

由变量生成c语言程序

将unbreakable变量用>0,breakable变量用<0,使用klee进行符号执行生成测试用例。(我想这里的变量名应该都是很长的,最后程序产生每个路径对应一个测试用例,测试用例是各个(变量),也就是句子。)

根据测试用例生成证书

算法12依据测试用例组装生成证书,

第一行定义了基础信息,例如版本号等。第三行第四行从测试用例中提取出条件和相应的值,例如变量tbsCertSignature_ present__signature Algorithm_MUSTsame,可以提取出&lt;tbsCertSignature, present and signatureAlgorithm, MUSTsame>。第五行到第七行给基础信息赋值,第十一行到第十三行依据测试用例给相应信息赋值,第十四行到十六行将breakable信息进行相反修改。

RFCcert的变异

使用RFCcert生成的证书来查找由违反RFC触发的bug。 RFCcert和突变方法是互补的,因为它们从不同方面寻找差异。 RFCcert擅长查找违反RFC的bug,而变异方法可能会发现并非由违反RFC的bug。 变异方法依赖于变异算子和种子证书来发现bug。 因此,RFCcert能够为突变方法(例如Mucert)提供有用的种子证书。

使用RFCcert证书作为输入,传统的变异方法仅产生变异的证书,而没有解释潜在差异。为了提供RFCcert的相似功能,即提供差异,通过变异跟踪器来检测变异方法。在下图中,输入的是RFCcert证书,以及证书违反了哪些规则的信息。变异过程采用开源变异方法,并使用变异跟踪器对它们进行检测。

论文中的实验

1、RFCcert与Mucert的对比

2、RFCcert与NEZHA的对比

3、Mutated RFCcert 与 Mucert+RFCcert 的对比

总结与思考

从RFC文档中提取规则以及如何根据符号执行生成的测试用例组装出证书测试用例是这篇论文的重点,也是RFCcert的难点。从自然语言中抽象出约束与限制条件,这与上一篇论文“通过自动化文档分析发现支付聚合服务中的逻辑漏洞”类似。

这种方法需要大量的文档分析前期工作,所以最好具有可扩展性和前瞻性,这篇论文中使用正则表达式的算法6-10是一个很好的例子,理论上可以修改后用于其他基于RFC文档的测试工作。