Firmware vulnerability analysis based on formal verification of software and hardware

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...

Full description

Saved in:
Bibliographic Details
Main Authors: Peng-hui ZHANG, Xi TIAN, Kang-wei LOU
Format: Article
Language:English
Published: POSTS&TELECOM PRESS Co., LTD 2016-07-01
Series:网络与信息安全学报
Subjects:
Online Access:http://www.cjnis.com.cn/thesisDetails#10.11959/j.issn.2096-109x.2016.00071
Tags: Add Tag
No Tags, Be the first to tag this record!
Description
Summary: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.
ISSN:2096-109X