◆何 旭 任曉靜

安全規(guī)范模塊驗(yàn)證方法的研究

◆何 旭 任曉靜

(達(dá)州職業(yè)技術(shù)學(xué)院 四川 635001)

針對(duì)大多數(shù)軟件組件驗(yàn)證其安全性是非常重要的，本文對(duì)驗(yàn)證軟件本身安全性進(jìn)行了簡(jiǎn)單介紹。分析了軟件隔離在操作系統(tǒng)內(nèi)核的虛擬內(nèi)存保護(hù)機(jī)制內(nèi)和不接受不受信任輸入的加密身份驗(yàn)證，分析了靜態(tài)分析與功能正確性驗(yàn)證的功能規(guī)范說明的程序建模及數(shù)據(jù)抽象。提出了功能規(guī)范端到端、模塊化、編譯程序來進(jìn)行功能正確性驗(yàn)證的保護(hù)機(jī)制，探索了模塊安全與功能正確保護(hù)機(jī)制驗(yàn)證的方法。得出了內(nèi)核、加密和編譯器可以通過編譯功能進(jìn)行正確性驗(yàn)證的途徑。

組件；安全性；保護(hù)機(jī)制；功能規(guī)范；驗(yàn)證

0 引言

一個(gè)計(jì)算機(jī)系統(tǒng)是由各種硬件與軟件組件構(gòu)成的，這些組件可能存在漏洞，因此具有強(qiáng)制性保護(hù)機(jī)制的可信內(nèi)核是確保一個(gè)組件的惡意漏洞不能傳播到其他組件的有效措施[1]。但是一個(gè)可信的內(nèi)核自身可能會(huì)非常龐大，它包括：實(shí)現(xiàn)虛擬內(nèi)存保護(hù)、網(wǎng)絡(luò)協(xié)議、加密協(xié)議、編譯器等。

計(jì)算機(jī)系統(tǒng)是由組件、軟硬件的進(jìn)程以及封裝層等模塊化方式構(gòu)建的，在這些層（或其中一個(gè)組件）中分析人員可能不想知道很多關(guān)于下一個(gè)組件的內(nèi)部結(jié)構(gòu)，例如網(wǎng)絡(luò)協(xié)議人員不想成為編譯優(yōu)化人員而想成為加密專家。

信任由不同組件建立起來的系統(tǒng)是至關(guān)重要的，一個(gè)龐大的系統(tǒng)不可避免地存在漏洞，從而黑客就能夠入侵到該系統(tǒng)。當(dāng)然也可以考慮到下列情形進(jìn)行驗(yàn)證。

（1）通過對(duì)所有這些組件進(jìn)行端對(duì)端、模塊化、推理驗(yàn)證，從而可以確認(rèn)具有實(shí)質(zhì)性的信任，這樣可以大幅提高系統(tǒng)的安全性。

（2）驗(yàn)證必須在不同領(lǐng)域進(jìn)行，程序邏輯或程序細(xì)化可以證明實(shí)現(xiàn)具體程序抽象算法的正確性，應(yīng)用程序推理可以用來驗(yàn)證能夠?qū)崿F(xiàn)目標(biāo)的抽象算法。

（3）高階純函數(shù)編程規(guī)范是功能規(guī)范驗(yàn)證模塊化程序常用的有效方法。

1 靜態(tài)分析與功能正確性驗(yàn)證

一些研究方法使用靜態(tài)分析工具檢查程序的安全性。有些具有安全屬性的程序的分析工具每一次執(zhí)行都是安全的則認(rèn)為具有可靠性，否則認(rèn)為是不可靠的。這樣的工具在軟件工程過程中是非常有用，可以減少錯(cuò)誤數(shù)量并提高可靠性特別是可靠性工具應(yīng)用于計(jì)算機(jī)安全方面，例如，Java類檢測(cè)工具可以保證不信任的代碼即使在缺少硬件存貯保護(hù)的情況下也是可靠的，這種可靠的靜態(tài)分析工具是一種形式化驗(yàn)證方法。

通過靜態(tài)分析操作系統(tǒng)內(nèi)核、加密庫以及字節(jié)碼驗(yàn)證等機(jī)制，將客戶端程序彼此分離，并保護(hù)系統(tǒng)代碼免受客戶端程序的影響。因此這些保護(hù)機(jī)制不僅要保證安全性而且還必須是正確可靠。操作系統(tǒng)內(nèi)核或加密庫沒有緩沖溢出也是不夠的，還必須計(jì)算正確。因此形式化的機(jī)器檢查其功能正確性驗(yàn)證的重要程序必須是實(shí)現(xiàn)保護(hù)機(jī)制的系統(tǒng)代碼。

2 功能規(guī)范說明

程序的功能規(guī)范說明表示程序的可觀察行為，數(shù)學(xué)關(guān)系和功能程序是兩種不同功能的研究方法，考慮如下C程序。

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

int i,min;

min=a[0];

for(i=0;i

if(a[i]

return min;

}

該C程序使用了三種不同的功能規(guī)格說明，排列{α,σ}表示變量α以當(dāng)前內(nèi)容為序列σ的一組排列。

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 σ) σ}

規(guī)格說明A和B表示輸入和輸出之間的數(shù)學(xué)關(guān)系，但是相對(duì)更嚴(yán)格，A只是確保返回值是數(shù)組的所有元素而不一定是唯一元素。但是這也不能表示B一定比A嚴(yán)格，可能A正是客戶端所需要的。規(guī)范說明C表示程序正好計(jì)算出該函數(shù)，滿足C的任何程序也將滿足A和B，也就是說C至少與A或B一樣嚴(yán)格。實(shí)際上任何以這種范式編寫的規(guī)范說明一定具有最強(qiáng)的后置條件，這是因?yàn)槭褂玫暮瘮?shù)語言具有確定性和全面性，因而不會(huì)出錯(cuò)且計(jì)算結(jié)果是唯一的。

A可能會(huì)被認(rèn)為正是客戶端需要的而B和C卻過多，規(guī)范C看起來冗長(zhǎng)。研究表明，用函數(shù)語言編寫規(guī)范說明也是非常有效的，常采用三級(jí)方法進(jìn)行驗(yàn)證描述。

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

該驗(yàn)證采用了常用的模塊化方式使其驗(yàn)證更加有效，精細(xì)化驗(yàn)證可以用在編程中，體現(xiàn)一些語言（如C、Java或匯編語言）之間的關(guān)系以及實(shí)現(xiàn)其給定的函數(shù)。在該驗(yàn)證中，關(guān)于數(shù)學(xué)算法方面的內(nèi)容通常是不必要的，所有內(nèi)容都可以在程序?qū)傩缘母呒?jí)驗(yàn)證中驗(yàn)證。

對(duì)功能規(guī)范的端到端、模塊化、編譯程序等都可以全面驗(yàn)證保護(hù)機(jī)制的功能正確性。例如使用功能性算法證明三層驗(yàn)證的細(xì)化層，OpenSSL SHA-256和HMAC用C語言實(shí)現(xiàn)并用證明其正確性[2]。通過離散邏輯證明顯示其獲會(huì)話期密鑰計(jì)算入侵者無法區(qū)分的HMAC與偽隨機(jī)函數(shù)PRF的正確性[3]，該驗(yàn)證通過推算其概率分布達(dá)到計(jì)算正確性的目的。

3 程序建模及數(shù)據(jù)抽象

對(duì)于SHA-256與HMAC來講，只要給定一個(gè)輸入，那么其輸出是唯一的，因此也就容易用C程序?qū)崿F(xiàn)純語言描述。但對(duì)于任何大型軟件系統(tǒng)或其中的一個(gè)模塊，從輸入到輸出不僅僅是一個(gè)簡(jiǎn)單的函數(shù)或功能描述，一個(gè)模塊具有內(nèi)部狀態(tài)以及在外部狀態(tài)下運(yùn)行的接口操作（方法）。在函數(shù)語言中，可以將其表示為表征類型的從屬記錄、“當(dāng)前內(nèi)部狀態(tài)”類型的值以及一系列表征類型或其它輸入的函數(shù)，并生成表達(dá)類型或其它輸出。

數(shù)據(jù)抽象的本質(zhì)是抽象數(shù)據(jù)類型ADT的私有表示形式可以通過關(guān)聯(lián)量進(jìn)行建模。不僅私有變量的類型必須被量化約束，而且表征不變量也是一樣。

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;

}

上面示例表示了具有私有變量的類型與被量化約束的關(guān)系，且模塊接口的規(guī)范說明部分是不受限制的。

為了顯示編譯產(chǎn)生SHA/HMAC語言程序的正確性，研究中引用兩個(gè)更加獨(dú)立的模塊化來證明。

Leroy關(guān)于CompCert的C編譯器的證明是正確的，其使用了C語言的形式化語義理論[6]。另外，Appel用可驗(yàn)證的C程序邏輯證明了Leroy表達(dá)的SHA和HMAC[7]。這兩種證明之間沒有太多重疊，然而在其規(guī)范接口上做了許多研究工作，主要集中在內(nèi)存模型和操作語義的Coq表示上[8]。同樣，CertiKOS研究了關(guān)于上下文細(xì)化與CompCert編譯器正確性證明的端到端連接問題。

SHA-2（安全散列算法）是一種使用迭代塊壓縮的算法，在256位模式下512位塊與256位散列混合產(chǎn)生一個(gè)新256位散列，這樣的塊可以鏈接在一起且奇數(shù)長(zhǎng)度的字符串由填充及長(zhǎng)度后綴來處理。

Bellare基于迭代塊壓縮（如SHA）提出了用于對(duì)稱密鑰加密認(rèn)證的HMAC算法并證明了其加密安全性，特別對(duì)于缺少會(huì)話密鑰的多項(xiàng)式時(shí)間使入侵者無法將隨機(jī)函數(shù)與HMAC區(qū)分開，HMAC是一種PRF（偽隨機(jī)函數(shù)）。

通過機(jī)器檢查證明，OpenSSL的SHA+HMAC加密是安全的，是一種基于PRF的加密。

Appel用C程序證明OpenSSL SHA-256并驗(yàn)證FIPS 180；Beringer用C證明OpenSSL HMAC并驗(yàn)證FIPS 198。

4 結(jié)論

用模塊化自動(dòng)檢查的方法驗(yàn)證重要系統(tǒng)安全組件功能的正確性是非常實(shí)用的，文中研究使用了三種重要的模塊化驗(yàn)證原則：（1）使用功能規(guī)范編寫成一個(gè)功能性程序，將特定領(lǐng)域的推理與低級(jí)程序語言驗(yàn)證分離出來；（2）使用低級(jí)編程語言（如C語言或匯編語言）的操作語義將程序驗(yàn)證與編譯器驗(yàn)證（或機(jī)器體系結(jié)構(gòu)驗(yàn)證）分開；（3）為了驗(yàn)證模塊化程序，使用高階邏輯描述，通過對(duì)謂詞量化來進(jìn)行抽象。最后，為了最大限度地減少規(guī)范接口上的語義歧義，都像通用高階邏輯證明一樣，所有的驗(yàn)證都可以在一個(gè)通用框架內(nèi)完成并可以嵌入工具。

[1]鄧良，曾慶凱.一種在不可信操作系統(tǒng)內(nèi)核中高效保護(hù)應(yīng)用程序的方法.軟件學(xué)報(bào)，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]何旭，任曉靜.約束偽隨機(jī)函數(shù)的構(gòu)造及應(yīng)用研究.網(wǎng)絡(luò)安全技術(shù)與應(yīng)用，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.

四川省教育廳理工科重點(diǎn)項(xiàng)目基金（14ZA0330）。