基于软硬件协同形式验证的固件漏洞分析技术

摘要

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