◆何 旭 任晓静

安全规范模块验证方法的研究

◆何 旭 任晓静

(达州职业技术学院 四川 635001)

针对大多数软件组件验证其安全性是非常重要的，本文对验证软件本身安全性进行了简单介绍。分析了软件隔离在操作系统内核的虚拟内存保护机制内和不接受不受信任输入的加密身份验证，分析了静态分析与功能正确性验证的功能规范说明的程序建模及数据抽象。提出了功能规范端到端、模块化、编译程序来进行功能正确性验证的保护机制，探索了模块安全与功能正确保护机制验证的方法。得出了内核、加密和编译器可以通过编译功能进行正确性验证的途径。

组件；安全性；保护机制；功能规范；验证

0 引言

一个计算机系统是由各种硬件与软件组件构成的，这些组件可能存在漏洞，因此具有强制性保护机制的可信内核是确保一个组件的恶意漏洞不能传播到其他组件的有效措施[1]。但是一个可信的内核自身可能会非常庞大，它包括：实现虚拟内存保护、网络协议、加密协议、编译器等。

计算机系统是由组件、软硬件的进程以及封装层等模块化方式构建的，在这些层（或其中一个组件）中分析人员可能不想知道很多关于下一个组件的内部结构，例如网络协议人员不想成为编译优化人员而想成为加密专家。

信任由不同组件建立起来的系统是至关重要的，一个庞大的系统不可避免地存在漏洞，从而黑客就能够入侵到该系统。当然也可以考虑到下列情形进行验证。

（1）通过对所有这些组件进行端对端、模块化、推理验证，从而可以确认具有实质性的信任，这样可以大幅提高系统的安全性。

（2）验证必须在不同领域进行，程序逻辑或程序细化可以证明实现具体程序抽象算法的正确性，应用程序推理可以用来验证能够实现目标的抽象算法。

（3）高阶纯函数编程规范是功能规范验证模块化程序常用的有效方法。

1 静态分析与功能正确性验证

一些研究方法使用静态分析工具检查程序的安全性。有些具有安全属性的程序的分析工具每一次执行都是安全的则认为具有可靠性，否则认为是不可靠的。这样的工具在软件工程过程中是非常有用，可以减少错误数量并提高可靠性特别是可靠性工具应用于计算机安全方面，例如，Java类检测工具可以保证不信任的代码即使在缺少硬件存贮保护的情况下也是可靠的，这种可靠的静态分析工具是一种形式化验证方法。

通过静态分析操作系统内核、加密库以及字节码验证等机制，将客户端程序彼此分离，并保护系统代码免受客户端程序的影响。因此这些保护机制不仅要保证安全性而且还必须是正确可靠。操作系统内核或加密库没有缓冲溢出也是不够的，还必须计算正确。因此形式化的机器检查其功能正确性验证的重要程序必须是实现保护机制的系统代码。

2 功能规范说明

程序的功能规范说明表示程序的可观察行为，数学关系和功能程序是两种不同功能的研究方法，考虑如下C程序。

int min(int a[], int n){

int i,min;

min=a[0];

for(i=0;i

if(a[i]

return min;

}

该C程序使用了三种不同的功能规格说明，排列{α,σ}表示变量α以当前内容为序列σ的一组排列。

Specific A：

∀ σ: list(ℤ)

precondition: {|σ|=n>0 ⋀ array α σ}

postcondition: {∀ j. 0≤i

Specific B:

∀ σ: list(ℤ)

precondition: {|σ|=n>0 ⋀ array α σ}

postcondition: {∃ i. 0≤i

⋀∀ j. 0≤j

Specific C:

LET

function fold(f:α→β→β)(b:β)(al:list(α)):β=

match al with nil⟹b|a::ar⟹f a(fold f b ar) end

function min(i:ℤ)(j:ℤ):ℤ=

if i

function hd(d: α)(al:list(α)): α=

match al with nil⟹d|a::ar⟹a end

IN

∀ σ:list(ℤ).

precondition: {|σ|=n>0 ⋀ array α σ}

postcondition: {ret=fold min(hd 0 σ) σ}

规格说明A和B表示输入和输出之间的数学关系，但是相对更严格，A只是确保返回值是数组的所有元素而不一定是唯一元素。但是这也不能表示B一定比A严格，可能A正是客户端所需要的。规范说明C表示程序正好计算出该函数，满足C的任何程序也将满足A和B，也就是说C至少与A或B一样严格。实际上任何以这种范式编写的规范说明一定具有最强的后置条件，这是因为使用的函数语言具有确定性和全面性，因而不会出错且计算结果是唯一的。

A可能会被认为正是客户端需要的而B和C却过多，规范C看起来冗长。研究表明，用函数语言编写规范说明也是非常有效的，常采用三级方法进行验证描述。

domain-specific proof pure functional program refinement proof imperative program compiler-correctness proof machine-language program

该验证采用了常用的模块化方式使其验证更加有效，精细化验证可以用在编程中，体现一些语言（如C、Java或汇编语言）之间的关系以及实现其给定的函数。在该验证中，关于数学算法方面的内容通常是不必要的，所有内容都可以在程序属性的高级验证中验证。

对功能规范的端到端、模块化、编译程序等都可以全面验证保护机制的功能正确性。例如使用功能性算法证明三层验证的细化层，OpenSSL SHA-256和HMAC用C语言实现并用证明其正确性[2]。通过离散逻辑证明显示其获会话期密钥计算入侵者无法区分的HMAC与伪随机函数PRF的正确性[3]，该验证通过推算其概率分布达到计算正确性的目的。

3 程序建模及数据抽象

对于SHA-256与HMAC来讲，只要给定一个输入，那么其输出是唯一的，因此也就容易用C程序实现纯语言描述。但对于任何大型软件系统或其中的一个模块，从输入到输出不仅仅是一个简单的函数或功能描述，一个模块具有内部状态以及在外部状态下运行的接口操作（方法）。在函数语言中，可以将其表示为表征类型的从属记录、“当前内部状态”类型的值以及一系列表征类型或其它输入的函数，并生成表达类型或其它输出。

数据抽象的本质是抽象数据类型ADT的私有表示形式可以通过关联量进行建模。不仅私有变量的类型必须被量化约束，而且表征不变量也是一样。

countr.h

struct countr;

struct countr * make(void);

void int(struct countr *p);

int get(struct countr *p);

counte.c

#include ”countr.h”;

struct countr {int x3; int x2;}

struct countr *make(void) {

struct countr *p = (struct counter *)malloc(sizeof(*p));

p->x3=0; p->x2=0;

return p;

}

void int (struct countr *p) {

p->x3+=3; p->x2+=2;

}

int get (struct countr *p) {

return p->x3 – p->x2;

}

上面示例表示了具有私有变量的类型与被量化约束的关系，且模块接口的规范说明部分是不受限制的。

为了显示编译产生SHA/HMAC语言程序的正确性，研究中引用两个更加独立的模块化来证明。

Leroy关于CompCert的C编译器的证明是正确的，其使用了C语言的形式化语义理论[6]。另外，Appel用可验证的C程序逻辑证明了Leroy表达的SHA和HMAC[7]。这两种证明之间没有太多重叠，然而在其规范接口上做了许多研究工作，主要集中在内存模型和操作语义的Coq表示上[8]。同样，CertiKOS研究了关于上下文细化与CompCert编译器正确性证明的端到端连接问题。

SHA-2（安全散列算法）是一种使用迭代块压缩的算法，在256位模式下512位块与256位散列混合产生一个新256位散列，这样的块可以链接在一起且奇数长度的字符串由填充及长度后缀来处理。

Bellare基于迭代块压缩（如SHA）提出了用于对称密钥加密认证的HMAC算法并证明了其加密安全性，特别对于缺少会话密钥的多项式时间使入侵者无法将随机函数与HMAC区分开，HMAC是一种PRF（伪随机函数）。

通过机器检查证明，OpenSSL的SHA+HMAC加密是安全的，是一种基于PRF的加密。

Appel用C程序证明OpenSSL SHA-256并验证FIPS 180；Beringer用C证明OpenSSL HMAC并验证FIPS 198。

4 结论

用模块化自动检查的方法验证重要系统安全组件功能的正确性是非常实用的，文中研究使用了三种重要的模块化验证原则：（1）使用功能规范编写成一个功能性程序，将特定领域的推理与低级程序语言验证分离出来；（2）使用低级编程语言（如C语言或汇编语言）的操作语义将程序验证与编译器验证（或机器体系结构验证）分开；（3）为了验证模块化程序，使用高阶逻辑描述，通过对谓词量化来进行抽象。最后，为了最大限度地减少规范接口上的语义歧义，都像通用高阶逻辑证明一样，所有的验证都可以在一个通用框架内完成并可以嵌入工具。

[1]邓良，曾庆凯.一种在不可信操作系统内核中高效保护应用程序的方法.软件学报，2016.

[2]Lennart Beringer, Adam Petcher, Katherine Q. Ye, and Andrew W.Appel. Verified correctness and security of OpenSSL HMAC. In 24th USENIX Security Symposium, pages 207–221. USENIX Assocation，2015.

[3]何旭，任晓静.约束伪随机函数的构造及应用研究.网络安全技术与应用，2017.

[4]Ronghui Gu, J´er´emie Koenig, Tahina Ramananandro, Zhong Shao, Xiongnan (Newman) Wu, Shu-Chun Weng, Haozhong Zhang, and Yu Guo. Deep specifications and certified abstraction layers. In 42nd ACM Symposium on Principles of Programming Languages (POPL’15), pages 595–608. ACM Press, January 2015.

[5]Gerwin Klein, June Andronick, Kevin Elphinstone, Toby Murray, Thomas Sewell, Rafal Kolanski, and Gernot Heiser. Comprehensive formal verification of an OS microkernel. ACM Transactions on Computer Systems，2014.

[6]Lennart Beringer, Gordon Stewart, Robert Dockins, and Andrew W. Appel. Verified compilation for shared-memory C. In European Symposium of Programming, Lecture Notes in Computer Science. Springer, 2014. To appear.

[7]Andrew W. Appel, Robert Dockins, Aquinas Hobor, Lennart Beringer, Josiah Dodds, Gordon Stewart, Sandrine Blazy, and Xavier Leroy. Program Logics for Certified Compilers. Cambridge，2014.

[8]Xi Wang, Nickolai Zeldovich, M. Frans Kaashoek, and Armando Solar-Lezama. A differential approach to undefined behavior detection. Communications of the ACM，2016.

四川省教育厅理工科重点项目基金（14ZA0330）。