网络与信息安全学报 ›› 2016, Vol. 2 ›› Issue (7): 59-68.doi: 10.11959/j.issn.2096-109x.2016.00071

• 学术论文 • 上一篇    下一篇

基于软硬件协同形式验证的固件漏洞分析技术

张朋辉(),田曦,楼康威   

  1. 国防科学技术大学电子科学与工程学院,湖南 长沙 410003
  • 修回日期:2016-06-27 出版日期:2016-07-15 发布日期:2020-03-26
  • 作者简介:张朋辉(1989-),男,河南安阳人,国防科学技术大学硕士生,主要研究方向为专用集成电路可信性设计、硬件安全性分析。|田曦(1971-),男,湖南长沙人,博士,国防科学技术大学副教授、硕士生导师,主要研究方向为信息安全、可信性设计。|楼康威(1992-),男,浙江金华人,国防科学技术大学硕士生,主要研究方向为专用集成电路可信性设计、电子信息系统信号安全分析。
  • 基金资助:
    国家高技术研究发展计划基金资助项目(2015AA2557)

Firmware vulnerability analysis based on formal verification of software and hardware

Peng-hui ZHANG(),Xi TIAN,Kang-wei LOU   

  1. School of Electronic Science and Engineering,National University of Defense Technology,Changsha 410003,China
  • Revised:2016-06-27 Online:2016-07-15 Published:2020-03-26
  • Supported by:
    The National High Technology Research and Development Program(2015AA2557)

摘要:

为了系统高效地分析固件中潜在的安全隐患,提出了一种基于行为时序逻辑 TLA 的软硬件协同形式验证方法。通过对固件工作过程中的软硬件交互机制进行形式建模分析,在动态调整攻击模型的基础上,发现了固件更新过程中存在的安全漏洞,并通过实验证实了该漏洞的存在,从而证明了形式验证方法的可靠性。

关键词: 固件安全, TLA, 形式验证, 漏洞分析, 软硬件协同

Abstract:

In order to analyze the potential vulnerabilities in the firmware systematically and effectively,a formal verification method based on TLA,in a collaborated form of software and hardware was proposed.With this method,the interaction mechanism of software and hardware in the computer boot process was modeled and analyzed.By adjusting the attack model,a secure vulnerability in the update process of the firmware was found,and its existence by an experiment,which proved the reliability of formal verification was demonstrated.

Key words: firmware security, TLA, formal verification, vulnerability analysis, software and hardware collaboration

中图分类号: 

No Suggested Reading articles found!