微控制器是电子设备中的核心器件。对微控制器中的固件恶意代码进行检测，是电子设备安全性分析研究的热点和重要内容。开展固件代码恶意性检测不仅有利于发现设备中存在的安全隐患，同时有助于电子设备故障排除和设备维护。本文以国家“863”目标导向类课题（编号2009AA01Z434）的研发为背景，结合固件代码的特点，分析了固件恶意功能实现机制，重点对固件恶意代码的检测方法进行研究，采用模型检验技术，实现对固件恶意代码的检测。论文的主要工作和贡献包括：1、提出了一种将控制流分析和数据流分析相结合的Kripke结构生成算法。针对由固件代码生成Kripke结构时遇到的间接跳转、间接存储、调用返回、中断和时序等问题，综合运用了变量定值分析、区间分析以及快速位运算算法等多项技术，成功解决了Kripke结构生成中的关键问题，实现了Kripke结构的自动构建。2、提出了一种面向位运算的变量区间分析方法——快速位运算算法。该算法包括了变量的不确定位形式（Uncertainty Bit Form, UBF）计算算法、面向UBF的位运算算法和UBF的区间生成算法，用于解决因固件代码中同时存在字节级（标量）和位级（向量）两种运算而造成的计算效率问题。实验结果表明，快速位运算算法在程序变量取值范围较大时效率远高于依次迭代法，并且算法耗时整体稳定，随着区间范围的增大呈下降趋势。3、设计并实现了基于模型检验的固件恶意代码检测原型系统FPAnalyzer。测试结果表明该系统能够成功检测固件恶意代码，验证了本文研究方法的正确性和有效性。