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...
Saved in:
Main Authors: | , , |
---|---|
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 |