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

张朋辉; 田曦; 楼康威

doi:10.11959/j.issn.2096-109x.2016.00071

您当前的位置：

首页 >

文章列表页 >

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

学术论文 | 更新时间：2024-06-03

- 基于软硬件协同形式验证的固件漏洞分析技术
- Firmware vulnerability analysis based on formal verification of software and hardware
- 网络与信息安全学报 2016年2卷第7期页码：59-68
- 作者机构：
- 作者简介：
  
  [ "张朋辉（1989-），男，河南安阳人，国防科学技术大学硕士生，主要研究方向为专用集成电路可信性设计、硬件安全性分析。" ]
  [ "田曦（1971-），男，湖南长沙人，博士，国防科学技术大学副教授、硕士生导师，主要研究方向为信息安全、可信性设计。" ]
  [ "楼康威（1992-），男，浙江金华人，国防科学技术大学硕士生，主要研究方向为专用集成电路可信性设计、电子信息系统信号安全分析。" ]
- 基金信息：
  
  国家高技术研究发展计划基金资助项目;The National High Technology Research and Development Program(2015AA2557)
- DOI：10.11959/j.issn.2096-109x.2016.00071
  中图分类号： TP309
- 网络首发：2016-07，
  
  纸质出版：2016-07-15
- 稿件说明：
移动端阅览
张朋辉, 田曦, 楼康威. 基于软硬件协同形式验证的固件漏洞分析技术[J]. 网络与信息安全学报, 2016,2(7):59-68.

Peng-hui ZHANG, Xi TIAN, Kang-wei LOU. Firmware vulnerability analysis based on formal verification of software and hardware[J]. Chinese Journal of Network and Information Security, 2016, 2(7): 59-68.
张朋辉, 田曦, 楼康威. 基于软硬件协同形式验证的固件漏洞分析技术[J]. 网络与信息安全学报, 2016,2(7):59-68. DOI： 10.11959/j.issn.2096-109x.2016.00071.

Peng-hui ZHANG, Xi TIAN, Kang-wei LOU. Firmware vulnerability analysis based on formal verification of software and hardware[J]. Chinese Journal of Network and Information Security, 2016, 2(7): 59-68. DOI： 10.11959/j.issn.2096-109x.2016.00071.

摘要

为了系统高效地分析固件中潜在的安全隐患，提出了一种基于行为时序逻辑 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.

关键词

Keywords

references

ZIMMER V , ROTHMAN M , MARISETTY S . Beyond BIOS:developing with the unified extensible firmware interface [M ] . Intel Press , 2010 .

BROSSARD J , DEMETRESCU F . Hardware backdooring is prac-tical [J ] . BlackHat,Las Vegas,USA , 2009 , 58 ( 1 ).

RONTTI T , JUUSO A M , TAKANEN A . Preventing DoS attacks in NGN networks with proactive specification-based fuzzing [J ] . IEEE Communications Magazine , 2012 , 50 ( 9 ): 164 - 170 .

RUI MA , DAGUANG WANG , CHANGZHEN HU , et al . Test data generation for stateful network protocol fuzzing using a rule-based state machine [J ] . Tsinghua Science and Technology , 2016 , 21 .

周仕钧 . 基于二进制补丁比对技术的漏洞特征分析与研究 [D ] . 昆明：云南大学， 2013 .

ZHOU S J . Holes characteristics analysis and research based on binary patch [D ] . Kunming : Yunnan University , 2013 .

KIM S , KIM R Y C , PARK Y B . Software vulnerability detection methodology combined with static and dynamic analysis [J ] . Wire-less Personal Communications , 2015 : 1 - 17 .

郑宇军，张蓓，薛锦云 . 软件形式化开发关键部件选取的水波优化方法 [J ] . 软件学报， 2016 ( 4 ): 933 - 942 .

ZHENG Y J , ZHANG B , XUE J Y . Water ware optimization method of Software for multination development key components selection [J ] . Journal of Software , 2016 ( 4 ): 933 - 942 .

CALINESCU R , GHEZZI C , JOHNSON K , et al . Formal verifica-tion with confidence intervals to establish quality of service proper-ties of software systems [J ] . IEEE Transactions on Reliability , 2016 , 65 ( 1 ): 107 - 125 .

KUMAR S , CHANDRA G , YADAV D . Formal verification of security protocol with B method[C]// IEEE International Confer-ence on Computer and Communication Technology . c2014 : 161 - 167 .

LACH J , BINGHAM S , ELKS C , et al . Accessible formal verifica-tion for safety-critical hardware design[C]// Reliability and Main-tainability Symposium,IEEE Computer Society . c2006 : 29 - 32 .

CHOI H , YIM M K , LEE J Y , et al . Formal verification of an in-dustrial system-on-a-chip[C]// IEEE International Conference on Computer Design . c2000 : 453 - 458 .

LAMPORT L . Specifying systems,the TLA+ language and tools for hardware and software engineers [J ] . Software Quality Profes-sional , 2002 ( 4 ): 43 .

CHAUDHURI K , DOLIGEZ D , LAMPORT L , et al . Verifying safety properties with the TLA+ proof system[M]//Automated Reasoning . Berlin Heidelberg:Springer 2010 : 142 - 148 .

LU T , MERZ S , WEIDENBACH C . Towards verification of the pastry protocol using TLA+[C]// Formal Techniques for Distrib-uted Systems Proceedings . c2011 : 244 - 258 .

KALLENBERG C , BUTTERWORTH J , KOVAH X , et al . Defeat-ing signed BIOS enforcement [J ] . EkoParty,Buenos Aires , 2013 .

ZHANG H , MERZ S , GU M . Specifying and verifying PLC sys-tems with TLA+:a case study [J ] . Computers ＆ Mathematics with Applications , 2010 , 60 ( 3 ): 695 - 705 .

NARAYANA P , CHEN R , ZHAO Y , et al . Automatic vulnerability checking of IEEE 802.16 WiMAX Protocols through TLA+[C]//IEEE Workshop on Secure Network Protocols . c2006 : 44 - 49 .

HEASMAN J . Implementing and detecting a PCI rootkit [J ] . Re-trieved February , 2006 , 20 : 3 .

BUDRUK R , ANDERSON D , SOLARI E . PCI express system architecture [J ] . Addison Wesley , 2003 .

YIN Y . Implementation of PCI expansion ROM mechanism [J ] . Computer Engineering＆Applications , 2005 .

WOJTCZUK R , RUTKOWSKA J . Attacking SMM memory via Intel CPU cache poisoning [J ] . Invisible Things Lab , 2009 .

浏览量

635

下载量

CSCD

文章被引用时，请邮件提醒。

提交

工具集

关联资源

基于函数语义分析的软件补丁比对技术

面向RTF的OLE对象漏洞分析研究