现代半导体芯片规模越来越大、设计越来越复杂,为了缩短开发周期、降低设计成本,芯片中往往会使用大量IP核。而这些IP核往往由第三方提供,其安全性无法保证,恶意厂商可能会在IP核中植入后门或硬件木马,导致整个芯片和系统的信息安全受到严重威胁,因此需要可靠的验证手段来检测第三方IP核的安全性。本文提出了一种基于形式化验证的属性验证方法,用于第三方IP软核RTL级信息流安全检测,结合IP核的安全需求对IP核的安全属性进行描述,制定符合形式化验证的规范描述方式,可以在不影响原电路正常功能的前提下,自动的对IP核是否满足安全属性进行检测。本文对IP核安全路径验证的基本理论进行分析,介绍了IP核安全路径验证所需的环境及方法。所提出的IP核代码污迹标记和追踪方法通过寄存器级的污迹标记位,可以更加直观地观测IP核中的信息流走向,从而分析出IP核中数量庞大而复杂的数据路径,加上安全属性的描述,以构建良好的验证环境。现有的可信度验证方法不能同时兼顾效率和准确性的优点,在众多的安全路径中,有一些是安全需求不关注的,如果穷举所有路径进行验证就会浪费大量的时间和精力,本文详细介绍了如何选取关键路径并且切断无关路径以提高检测的效率和准确性;同时针对可能面对的级联复杂的超长路径,传统的验证方法无法对其直接进行检测,本文提出的超长路径的可组合性证明方法巧妙的将其转化为几条短路径的组合性证明,降低了验证工作的难度。本文设计并实现了一个自动化工具链,并对该工具链的整体方案和程序函数进行详细的说明,实现了安全路径的选取和组合性证明,并针对TrustHub上含有硬件木马或后门的Verilog代码和IP核进行了测试,包括加密类IP核(AES、3DES)、通信类IP核(RS232)、总线IP核(CAN)等等,成功地检测出IP核的信息安全问题,并且与传统方法相比提高了检测的效率和准确性,表明本文提出的验证方法对第三方IP核的安全性检测有非常重要的参考价值。