Firmware vulnerability analysis based on formal verification of software and hardware

Peng-hui ZHANG; Xi TIAN; Kang-wei LOU

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

您当前的位置：

首页 >

文章列表页 >

Firmware vulnerability analysis based on formal verification of software and hardware

Academic paper | 更新时间：2024-06-03

- Firmware vulnerability analysis based on formal verification of software and hardware
- Chinese Journal of Network and Information Security Vol. 2, Issue 7, Pages: 59-68(2016)
- 作者机构：
- 作者简介：
- 基金信息：
- DOI：10.11959/j.issn.2096-109x.2016.00071
  CLC： TP309
- Online First：2016-07，
  
  Published：15 July 2016
- 稿件说明：
移动端阅览
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：

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 .

Views

635

下载量

CSCD

Alert me when the article has been cited

提交

Tools

Publicity Resources

Software patch comparison technology through semantic analysis on function

Research on OLE object vulnerability analysis for RTF file

Related Author

Yan CAO

Long LIU

Yu WANG

Qingxian WANG

De-guang LE

Liang ZHANG

Sheng-rong GONG

Li-xin ZHENG

Related Institution

State Key Laboratory of Mathematical Engineering ＆Advanced Computing

Henan University of Engineering

School of Computer Science and Engineering, Changshu Institute of Technology, Changshu

School of Computer Science and Technology, Soochow University

College of Engineering, Huaqiao University

⁰