可编程逻辑控制器(Programmable Logic Controller,PLC)程序易遭受篡改攻击而导致系统违背安全状态,甚至造成物理设备的破坏。当前,PLC代码的安全主要依赖于工程师对代码缺陷的检测,而缺乏工程师对违反安全状态的恶意行为检测。针对PLC程序易遭受篡改攻击而导致系统在违背安全状态下运行的问题,本文在工业控制系统风险分析的基础上,提出一种基于状态验证的PLC程序恶意行为检测方法。本文首先反汇编PLC字节码程序为STL程序,其次根据STL语言的特征构建程序控制流图,然后在控制流图的基础上进行数据流分析,获得程序可执行路径集和程序输入输出之间的映射关系;接下来根据PLC程序周期反馈执行的特点构建程序状态检测模型,最后基于状态验证的方法对安全规约进行验证,实现对PLC程序恶意行为的检测。本文的主要研究工作总结如下:(1)针对PLC程序状态生成过程中状态空间爆炸的问题,本文根据PLC程序的执行规则,提出一种在同一程序扫描周期将相同状态合并以及在不同程序扫描周期对已分析过的状态移除的方法来缓解状态空间爆炸问题。(2)提出一种计时器建模的方法。工业控制系统对实时性要求很高,因此时间是重要的建模参数。由于计时器是跨越多个扫描周期的全局变量,计时器在预定时间内可能会跨越数千个扫描周期,这给包含有计时器的PLC程序建模带来了极大的困难,增加了建模的时间。但是如果不考虑时间就无法检测到与时间相关的安全规约。本文提出一种通过分析部分输出状态转换关系来推导在定时器计时时间内所有输出状态的方法,降低了计时器建模的开销。(3)获取违反安全状态的输入序列。一旦检测到PLC代码中的恶意行为,本文通过逆推PLC程序执行过程获得违反安全状态的输入序列,得到PLC程序恶意行为的触发条件。(4)设计并实现原型系统。本文设计并实现了原型系统,通过实验表明,该方法能够有效地实现对违反安全状态的PLC恶意行为的检测,在给出的5个案例研究中,该方法的检测过程耗时均不超过5分钟。