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

◆何 旭 朱鹏飞 任晓静

一种基于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）。