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!
_version_ 1841530403345661952
author Peng-hui ZHANG
Xi TIAN
Kang-wei LOU
author_facet Peng-hui ZHANG
Xi TIAN
Kang-wei LOU
author_sort Peng-hui ZHANG
collection DOAJ
description 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.
format Article
id doaj-art-c5af801a736d43dd86dc112b74736cff
institution Kabale University
issn 2096-109X
language English
publishDate 2016-07-01
publisher POSTS&TELECOM PRESS Co., LTD
record_format Article
series 网络与信息安全学报
spelling doaj-art-c5af801a736d43dd86dc112b74736cff2025-01-15T03:04:45ZengPOSTS&TELECOM PRESS Co., LTD网络与信息安全学报2096-109X2016-07-012596859546817Firmware vulnerability analysis based on formal verification of software and hardwarePeng-hui ZHANGXi TIANKang-wei LOUIn 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.http://www.cjnis.com.cn/thesisDetails#10.11959/j.issn.2096-109x.2016.00071firmware securityTLAformal verificationvulnerability analysissoftware and hardware collaboration
spellingShingle Peng-hui ZHANG
Xi TIAN
Kang-wei LOU
Firmware vulnerability analysis based on formal verification of software and hardware
网络与信息安全学报
firmware security
TLA
formal verification
vulnerability analysis
software and hardware collaboration
title Firmware vulnerability analysis based on formal verification of software and hardware
title_full Firmware vulnerability analysis based on formal verification of software and hardware
title_fullStr Firmware vulnerability analysis based on formal verification of software and hardware
title_full_unstemmed Firmware vulnerability analysis based on formal verification of software and hardware
title_short Firmware vulnerability analysis based on formal verification of software and hardware
title_sort firmware vulnerability analysis based on formal verification of software and hardware
topic firmware security
TLA
formal verification
vulnerability analysis
software and hardware collaboration
url http://www.cjnis.com.cn/thesisDetails#10.11959/j.issn.2096-109x.2016.00071
work_keys_str_mv AT penghuizhang firmwarevulnerabilityanalysisbasedonformalverificationofsoftwareandhardware
AT xitian firmwarevulnerabilityanalysisbasedonformalverificationofsoftwareandhardware
AT kangweilou firmwarevulnerabilityanalysisbasedonformalverificationofsoftwareandhardware