一種基于OpenSSL架構(gòu)HMAC安全模型的研究

◆何 旭 朱鵬飛 任曉靜

一種基于OpenSSL架構(gòu)HMAC安全模型的研究

◆何 旭 朱鵬飛 任曉靜

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

安全模型應(yīng)用的任務(wù)可以是安全認(rèn)證功能。分析了SHA-256環(huán)境下HMAC的Open SSL實現(xiàn)FIPS功能規(guī)范，分析了功能規(guī)范保證預(yù)期加密屬性途徑，分析了哈希函數(shù)構(gòu)造哈希消息認(rèn)證碼的功能規(guī)范。提出了增量API對HMAC和SHA函數(shù)的支持規(guī)則，探索了HMAC安全模型的幾種構(gòu)造方法，得出了HMAC基本安全架構(gòu)。

安全套接字；哈希消息認(rèn)證碼；安全哈希算法；安全模型

HMAC是一種Hash密鑰消息加密認(rèn)證算法[1]，廣泛應(yīng)用于SHA-256加密原語中。信息m的發(fā)送端與接收端共享對話密鑰k，發(fā)送端用HMAC(k,m)計算s并將s添加到m；接收端通過HMAC(k,m)計算出s’并驗證是否是s。理論上不知道k就不能計算出s，接收端也不能夠判斷信息m是否來自發(fā)送端。

使用加密屬性的HMAC或SHA規(guī)范已經(jīng)證明可能與作為計算機程序發(fā)布的規(guī)范存在不同[2]，用C程序可以解釋C的語義與C編譯器不同。

這樣就會導(dǎo)致使用SHA的壓縮函數(shù)可能無法使偽隨機函數(shù)(PRF)具有加密屬性，SHA算法也可能不能正確構(gòu)造壓縮函數(shù)，更為嚴(yán)重的是HMAC算法可能使PRF加密屬性具有不正確性[3]。

1 SHA與HMAC256形式化定義

SHA函數(shù)的FIPS180-4規(guī)范用Coq[4]形式化函數(shù)定義如程序段1所示。

程序段1 SHA函數(shù)的定義：

Definition SHA-256(str:list Z):list Z:=intlist_to_Zlist(hash_blocks init_registers(generate_and_pad str)).

其中hash_blocks，init_registers和generate_and_pad是FIPS標(biāo)準(zhǔn)的轉(zhuǎn)換，Z是Coq整數(shù)型數(shù)據(jù)，list Z的自變量是字符串型其值是整型數(shù)據(jù)。SHA-256是32位無符號模運算，intlist_to_Zlist將32位int型機器碼序列轉(zhuǎn)換為字節(jié)序列的數(shù)字型。SHA-256的功能形式及其所包括功能定義都具有安全性/正確性理論基礎(chǔ)。

使用哈希函數(shù)SHA256構(gòu)造HMAC256完整功能規(guī)范定義如程序段2所示。

程序段2 HMAC256功能定義：

Definition mkKey(:list Z):list Z:=zeropad (if || > 64 then SHA_256else).

Definition KeyPreparation(k:list Z):list byte:=map Byte.repr (mkKey).

Definition HASH:=SHA_256(++).

Definition HmacCore:=HASH(opad⊕)(HASH(ipad⊕)).

Definition HMAC256(:list Z):list Z:=HmacCore(KeyPreparation).

其中zeropad是將64位以字節(jié)為單位的SHA256數(shù)據(jù)塊參數(shù)向右擴展，ipad和opad是FIPS198-1的填充常量，⊕表示XOR運算，++表示連接運算。

2 C程序函數(shù)的API規(guī)范

依賴OpenSSL頭文件的API接口實現(xiàn)的HMAC使用了前置條件、后置條件及循環(huán)常量證明了C程序正確性，邏輯上講最初沒能很好處理指針數(shù)據(jù)類型，后來引入邏輯分離很好地將本地操作封裝在數(shù)據(jù)結(jié)構(gòu)內(nèi)，通過Verifiable C[5]實現(xiàn)C語言的邏輯分離。

用SHA256和HMAC256定義的FIPS180和FIPS198規(guī)范沒有解釋如何在數(shù)組中處理數(shù)值型字符序列，并將結(jié)構(gòu)作為參數(shù)傳遞給C函數(shù)且由其內(nèi)部使用。為了實現(xiàn)API規(guī)范使用Verifiable C可以指定每個函數(shù)API行為，其行為包括操作數(shù)據(jù)結(jié)構(gòu)、前提條件、假定參數(shù)、全局變量中可用的輸入數(shù)據(jù)結(jié)構(gòu)、保證返回值的數(shù)據(jù)符合后置條件。

如下所示是HMAC的API規(guī)范，首先定義了一個Coq記錄類型:

Record DATA:={LEN:Z;CONT:list Z}.

如果key是DATA類型，則LEN(key)是整數(shù)，CONT(key)是整數(shù)序列key的值，此外不使用強制類型轉(zhuǎn)換的LEN所對應(yīng)的CONT屬性的長度。在Verifiable C中為了描述C語言函數(shù)的API，其定義如下:

在HMAC256_spec定義中，WITH子句列出的第一個抽象數(shù)值類型是key指針，其數(shù)值類型是C的值val，表示傳遞HMAC會話密鑰的內(nèi)存地址。在PRE條件的LOCAL部分，形式參數(shù)_key包含函數(shù)入口值kp，在SEP部分的kp處有一個包含實際密鑰字節(jié)的數(shù)據(jù)塊data_block。在后置條件中，再次引用kp表示地址kp的數(shù)據(jù)塊仍然存在且HMAC函數(shù)沒有改變。

程序段3 HMAC256_spec定義:

WITH其值是DATA類型為key，即字節(jié)型的數(shù)值序列。在前提條件PROP子句中，強制使用has_lengthK(LEN key)(CONT key)執(zhí)行。

函數(shù)Int.repr從整型中注入32位有符號/無符號數(shù)據(jù)，這樣temp _n(Vint (Int.repr(LEN)))取整型(LEN msg)并將其轉(zhuǎn)換成32位有符號數(shù)據(jù)，然后將其注入C的值空間，并聲明參數(shù)_n包含在該值的函數(shù)內(nèi)。由has_lengthD強制執(zhí)行LEN在0≤LEN msg<232范圍內(nèi)就具有是合理的，用戶定義的has_lengthK和has_lengthD都在HMAC API規(guī)范內(nèi)。

在前提條件中，地址md包含有未初始化的32字節(jié)memory_block存儲器塊，該地址的值是C函數(shù)的_md參數(shù)值。在后置條件中，地址md的存儲塊已經(jīng)使用HMAC256 (CONT) (CONT key)初始化該數(shù)據(jù)塊。

完全支持OpenSSL的HMAC和SHA函數(shù)都具有增量API。使用密鑰初始化hasher，逐步附加消息片段到散列中，最終生成消息摘要。

3 HMAC安全性實現(xiàn)

程序段4 PRF的定義：

程序段4中給出PRF的定義。f用K→D→R表示的PRF函數(shù)，對于密鑰k:K而言不知道密鑰k的入侵者不能通過隨機函數(shù)(D→R)獲得更多區(qū)分f與k的信息。

入侵者A是通過函數(shù)f構(gòu)造數(shù)據(jù)庫oracle或者與randomFunc進行交互OracleComp，randomFunc通過輸出生成隨機值并予以存儲的隨機函數(shù)，其存儲的目的是便于以后對于相同輸入時可以重復(fù)使用。randomFunc數(shù)據(jù)庫oracle使用列表對作為狀態(tài)，其初始狀態(tài)為空列表對。tt的值是unit型，unit與C語言的”void”非常相似的占位符類型。本定義使用替代箭頭（<_$2)構(gòu)造序列，其中第一個計算產(chǎn)生元組，并為元組中的每個值賦予名稱，箭頭提供元組的大小以便支持解析。

函數(shù)f_oracle封裝函數(shù)f并將其轉(zhuǎn)換為數(shù)據(jù)庫oracle，Comp bool是生成bool類型的隨機計算，Rat是一元非負(fù)有理數(shù)。

入侵者試圖確定oracle在f中是否是隨機函數(shù)，與oracle交互之后入侵者就會進行確認(rèn)。如果有入侵者機會，入侵者的優(yōu)勢定義為f和隨機函數(shù)產(chǎn)生隨機差異，如果該優(yōu)勢足夠小，則f是偽隨機函數(shù)PRF。

程序段5 弱抗沖突WCR的定義:

程序段5定義了一個弱抗沖突函數(shù)WCR。該定義使用單一入侵模型，允許入侵者可與由密鑰控制函數(shù)f定義的oracle進行交互。在此交互結(jié)束時，攻擊者試圖產(chǎn)生沖突，或產(chǎn)生相同輸出的一對不同輸入值。在該入侵模型中，用？=和！=分別表示對等和非對等的入侵執(zhí)行，入侵者的優(yōu)勢在于能夠定位沖突概率。

程序段7 HMAC抽象規(guī)范的定義:

HMAC抽象規(guī)范定義的splitAndPad的作用從位列表中生成一個位向量列表，且根據(jù)需要填充最后一位位向量。app-fpad是一個填充函數(shù)，從長度為c的位向量產(chǎn)生長度為b的位向量。HMAC函數(shù)使用常量opad和ipad從長度為b的密鑰生成長度為2b的密鑰。

程序段8 HMAC的安全性定義:

HMAC的安全性定義通過任意入侵者優(yōu)勢表達式表明HMAC是PRF。該列表描述了每個安全定義的所有參數(shù)。第一個參數(shù)產(chǎn)生隨機密鑰；在PRF_Advantage和RKA_Advantage中，第二個參數(shù)在函數(shù)范圍內(nèi)產(chǎn)生隨機值，參數(shù)c和b是安全參數(shù)h的多項式。如果其他三個項的每個項在h中可忽略不計，入侵者A對HMAC的優(yōu)勢在h中同樣可以忽略不計。并且當(dāng)b和c的值根據(jù)實現(xiàn)使用大小固定時，使用該表達式就可以獲取HMAC安全精度。

圖1 HMAC的安全架構(gòu)圖

4 結(jié)語

類似OpenSSL的開源加密庫構(gòu)成通用通信安全基礎(chǔ)。入侵者通過搜索大量漏洞并利用這些漏洞。編譯器和OS內(nèi)核可以使用零功能正確性缺陷標(biāo)準(zhǔn)強化自身安全性。以模型模塊化方式構(gòu)建常見加密基礎(chǔ)架構(gòu)的關(guān)鍵組件程序段。

[1]吳震，王敏等.針對基于SM3的HMAC的互信息能量分析攻擊[J].通信學(xué)報，2016（1）：57-62.

[2]Secure hash standard （SHS). Tech. Rep. FIPS PUB 180-4，Information Technology Laboratory，National Institute of Standards and Technology，Gaithersburg，MD，Mar. 2012.

[3]何旭，任曉靜.安全規(guī)范模塊驗證方法的研究[J].網(wǎng)絡(luò)安全技術(shù)與應(yīng)用，2018（10）：19-20.

[4]Coq. https://coq.inria.fr.

[5]APPEL，A.W.，DOCKINS，R.，HOBOR，A.，BERINGER，L.，DODDS，J.，STEWART，G.，BLAZY，S.，AND LEROY，X.Program Logics for Certified Compilers. Cambridge，2014.

[6]BACKES，M.，BARTHE，G.，BERG，M.，GR′EGOIRE，B.，KUNZ，C.，SKORUPPA，M.，AND B′EGUELIN，S.Z.Verified security of Merkle-Damgard. In Computer Security Foundations Symposium （CSF），2012 IEEE 25th（2012），IEEE，354-368.

教育部職業(yè)院校教育類專業(yè)教育指導(dǎo)委員會科研課題“互聯(lián)網(wǎng)+背景下課堂教學(xué)模式的創(chuàng)新研究”（2018GGJCKT192）。