%A 张朋辉,田曦,楼康威 %T 基于软硬件协同形式验证的固件漏洞分析技术 %0 Journal Article %D 2016 %J 网络与信息安全学报 %R 10.11959/j.issn.2096-109x.2016.00071 %P 59-68 %V 2 %N 7 %U {https://www.infocomm-journal.com/cjnis/CN/abstract/article_170017.shtml} %8 2016-07-15 %X

为了系统高效地分析固件中潜在的安全隐患,提出了一种基于行为时序逻辑 TLA 的软硬件协同形式验证方法。通过对固件工作过程中的软硬件交互机制进行形式建模分析,在动态调整攻击模型的基础上,发现了固件更新过程中存在的安全漏洞,并通过实验证实了该漏洞的存在,从而证明了形式验证方法的可靠性。