硬件木马对原始电路的恶意篡改,已成为集成电路面临的核心安全威胁。为了保障集成电路的安全可信,研究人员提出了诸多硬件木马检测方法。其中,模型检测作为一种形式化验证方法,在设计阶段可有效检测出硬件木马。首先,阐述了模型检测的工作原理和应用流程;其次,介绍了基于模型检测的硬件木马检测技术的研究进展;最后,指出了当前该技术所面临的瓶颈,并讨论了潜在的研究方向。