一种基于OpenSSL架构HMAC安全模型的研究

2019-10-15 05:19朱鹏飞任晓静
网络安全技术与应用 2019年10期
关键词:入侵者哈希密钥

◆何 旭 朱鹏飞 任晓静

一种基于OpenSSL架构HMAC安全模型的研究

◆何 旭 朱鹏飞 任晓静

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

安全模型应用的任务可以是安全认证功能。分析了SHA-256环境下HMAC的Open SSL实现FIPS功能规范,分析了功能规范保证预期加密属性途径,分析了哈希函数构造哈希消息认证码的功能规范。提出了增量API对HMAC和SHA函数的支持规则,探索了HMAC安全模型的几种构造方法,得出了HMAC基本安全架构。

安全套接字;哈希消息认证码;安全哈希算法;安全模型

HMAC是一种Hash密钥消息加密认证算法[1],广泛应用于SHA-256加密原语中。信息m的发送端与接收端共享对话密钥k,发送端用HMAC(k,m)计算s并将s添加到m;接收端通过HMAC(k,m)计算出s’并验证是否是s。理论上不知道k就不能计算出s,接收端也不能够判断信息m是否来自发送端。

使用加密属性的HMAC或SHA规范已经证明可能与作为计算机程序发布的规范存在不同[2],用C程序可以解释C的语义与C编译器不同。

这样就会导致使用SHA的压缩函数可能无法使伪随机函数(PRF)具有加密属性,SHA算法也可能不能正确构造压缩函数,更为严重的是HMAC算法可能使PRF加密属性具有不正确性[3]。

1 SHA与HMAC256形式化定义

SHA函数的FIPS180-4规范用Coq[4]形式化函数定义如程序段1所示。

程序段1 SHA函数的定义:

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标准的转换,Z是Coq整数型数据,list Z的自变量是字符串型其值是整型数据。SHA-256是32位无符号模运算,intlist_to_Zlist将32位int型机器码序列转换为字节序列的数字型。SHA-256的功能形式及其所包括功能定义都具有安全性/正确性理论基础。

使用哈希函数SHA256构造HMAC256完整功能规范定义如程序段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位以字节为单位的SHA256数据块参数向右扩展,ipad和opad是FIPS198-1的填充常量,⊕表示XOR运算,++表示连接运算。

2 C程序函数的API规范

依赖OpenSSL头文件的API接口实现的HMAC使用了前置条件、后置条件及循环常量证明了C程序正确性,逻辑上讲最初没能很好处理指针数据类型,后来引入逻辑分离很好地将本地操作封装在数据结构内,通过Verifiable C[5]实现C语言的逻辑分离。

用SHA256和HMAC256定义的FIPS180和FIPS198规范没有解释如何在数组中处理数值型字符序列,并将结构作为参数传递给C函数且由其内部使用。为了实现API规范使用Verifiable C可以指定每个函数API行为,其行为包括操作数据结构、前提条件、假定参数、全局变量中可用的输入数据结构、保证返回值的数据符合后置条件。

如下所示是HMAC的API规范,首先定义了一个Coq记录类型:

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

如果key是DATA类型,则LEN(key)是整数,CONT(key)是整数序列key的值,此外不使用强制类型转换的LEN所对应的CONT属性的长度。在Verifiable C中为了描述C语言函数的API,其定义如下:

在HMAC256_spec定义中,WITH子句列出的第一个抽象数值类型是key指针,其数值类型是C的值val,表示传递HMAC会话密钥的内存地址。在PRE条件的LOCAL部分,形式参数_key包含函数入口值kp,在SEP部分的kp处有一个包含实际密钥字节的数据块data_block。在后置条件中,再次引用kp表示地址kp的数据块仍然存在且HMAC函数没有改变。

程序段3 HMAC256_spec定义:

WITH其值是DATA类型为key,即字节型的数值序列。在前提条件PROP子句中,强制使用has_lengthK(LEN key)(CONT key)执行。

函数Int.repr从整型中注入32位有符号/无符号数据,这样temp _n(Vint (Int.repr(LEN)))取整型(LEN msg)并将其转换成32位有符号数据,然后将其注入C的值空间,并声明参数_n包含在该值的函数内。由has_lengthD强制执行LEN在0≤LEN msg<232范围内就具有是合理的,用户定义的has_lengthK和has_lengthD都在HMAC API规范内。

在前提条件中,地址md包含有未初始化的32字节memory_block存储器块,该地址的值是C函数的_md参数值。在后置条件中,地址md的存储块已经使用HMAC256 (CONT) (CONT key)初始化该数据块。

完全支持OpenSSL的HMAC和SHA函数都具有增量API。使用密钥初始化hasher,逐步附加消息片段到散列中,最终生成消息摘要。

3 HMAC安全性实现

程序段4 PRF的定义:

程序段4中给出PRF的定义。f用K→D→R表示的PRF函数,对于密钥k:K而言不知道密钥k的入侵者不能通过随机函数(D→R)获得更多区分f与k的信息。

入侵者A是通过函数f构造数据库oracle或者与randomFunc进行交互OracleComp,randomFunc通过输出生成随机值并予以存储的随机函数,其存储的目的是便于以后对于相同输入时可以重复使用。randomFunc数据库oracle使用列表对作为状态,其初始状态为空列表对。tt的值是unit型,unit与C语言的”void”非常相似的占位符类型。本定义使用替代箭头(<_$2)构造序列,其中第一个计算产生元组,并为元组中的每个值赋予名称,箭头提供元组的大小以便支持解析。

函数f_oracle封装函数f并将其转换为数据库oracle,Comp bool是生成bool类型的随机计算,Rat是一元非负有理数。

入侵者试图确定oracle在f中是否是随机函数,与oracle交互之后入侵者就会进行确认。如果有入侵者机会,入侵者的优势定义为f和随机函数产生随机差异,如果该优势足够小,则f是伪随机函数PRF。

程序段5 弱抗冲突WCR的定义:

程序段5定义了一个弱抗冲突函数WCR。该定义使用单一入侵模型,允许入侵者可与由密钥控制函数f定义的oracle进行交互。在此交互结束时,攻击者试图产生冲突,或产生相同输出的一对不同输入值。在该入侵模型中,用?=和!=分别表示对等和非对等的入侵执行,入侵者的优势在于能够定位冲突概率。

程序段7 HMAC抽象规范的定义:

HMAC抽象规范定义的splitAndPad的作用从位列表中生成一个位向量列表,且根据需要填充最后一位位向量。app-fpad是一个填充函数,从长度为c的位向量产生长度为b的位向量。HMAC函数使用常量opad和ipad从长度为b的密钥生成长度为2b的密钥。

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

HMAC的安全性定义通过任意入侵者优势表达式表明HMAC是PRF。该列表描述了每个安全定义的所有参数。第一个参数产生随机密钥;在PRF_Advantage和RKA_Advantage中,第二个参数在函数范围内产生随机值,参数c和b是安全参数h的多项式。如果其他三个项的每个项在h中可忽略不计,入侵者A对HMAC的优势在h中同样可以忽略不计。并且当b和c的值根据实现使用大小固定时,使用该表达式就可以获取HMAC安全精度。

图1 HMAC的安全架构图

4 结语

类似OpenSSL的开源加密库构成通用通信安全基础。入侵者通过搜索大量漏洞并利用这些漏洞。编译器和OS内核可以使用零功能正确性缺陷标准强化自身安全性。以模型模块化方式构建常见加密基础架构的关键组件程序段。

[1]吴震,王敏等.针对基于SM3的HMAC的互信息能量分析攻击[J].通信学报,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]何旭,任晓静.安全规范模块验证方法的研究[J].网络安全技术与应用,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.

教育部职业院校教育类专业教育指导委员会科研课题“互联网+背景下课堂教学模式的创新研究”(2018GGJCKT192)。

猜你喜欢
入侵者哈希密钥
幻中邂逅之金色密钥
幻中邂逅之金色密钥
基于特征选择的局部敏感哈希位选择算法
哈希值处理 功能全面更易用
密码系统中密钥的状态与保护*
文件哈希值处理一条龙
创建KDS根密钥
“入侵者”来袭
巧用哈希数值传递文件
“外星人”入侵档案之隐形入侵者