PLC代码利用相关研究,PLC代码缺陷分类
本文主要观点
1、plc代码利用相关研究
2、plc代码缺陷分类：plc代码逻辑缺陷、plc代码安全需求规约
3、plc代码形式化分析与验证：plc形式化分析中面临的困难、plc代码形式化分析
随着工业控制系统由封闭走向互联，大量的控制器配备了以太网通信组件，使得攻击者可以直接访问plc硬件及其编程软件。但plc逻辑控制层缺少认证和监测等保护措施，plc代码的安全缺陷成为工业控制系统的重要安全威胁之一。
第一部分 plc代码利用相关研究
与传统的编程语言一样，plc存在代码安全缺陷，而这些代码安全缺陷为攻击者攻击工业控制系统留下了后门。
2013年south carolina大学的sidney对plc代码设计安全缺陷进行了深入的研究，并把plc代码设计级缺陷主要分为基于硬件缺陷和基于软件缺陷两种。攻击者可以利用plc代码缺陷破坏代码逻辑，进行中间代码插桩，实现任意代码执行等。
2014年北京科技大学李伟泽等提出和分析了一种针对scada系统的新型的网络物理攻击——伪逻辑攻击。
2015年在blackhat-us会议上klick等在西门子s7-300中注入了一种新型的后门，通过注入工具实现了在s7-300上进行snmp扫描sock5代理功能。作者利用plc程序中存在跳转指令的安全缺陷，成功在主程序ob1前嵌入恶意指令从而可以控制plc的启停以及输出寄存器。
2016年11月在blackhat欧洲会议上ali abbasi等实现了对plc输入/输出接口的新攻击，该攻击通过篡改输出输入引脚改变系统的运行逻辑。
2017年3月，来自印度海德拉巴和新加坡的学者，演示了针对工业控制系统的plc梯形图逻辑炸弹（ladder logic bombs，llb）。该逻辑炸弹是用梯形图语言编写的恶意软件，这种恶意软件可被攻击者注入到plc现有控制逻辑中，通过改变控制动作或者等待特定的触发信号来激活恶意行为，以实现传感器数据篡改，系统敏感信息获取以及plc拒绝服务攻击等。
第二部分 plc代码缺陷分类
不同于传统的it系统，工业控制系统有其特殊的编程语言，根据国际电工委员会制定的工业控制编程语言标准（iec61131-3），plc的编程语言包括以下五种：梯形图语言（ladderlogic programming language，ld）、指令表语言（instruction list，il）、功能模块图语言（function block diagram，fbd）、顺序功能流程图语言（sequential function chart，sfc）及结构化文本语言（structured text，st）。本文中的代码缺陷研究也是基于上述编程语言展开的。
工业控制系统的入侵与传统互联网入侵虽然手段上大同小异，但工业控制系统的部署与其物理工艺流程紧耦合，因此利用工艺流程中的代码逻辑缺陷成为针对工业控制系统的有效打击手段之一，如陷阱门、逻辑炸弹、特洛伊木马、蠕虫、zombie等，且这类新的恶意代码具有更强的传播能力和破坏性。本文主要研究基于软件的plc代码缺陷，并从代码逻辑缺陷和违反安全需求规约两个方面对plc代码缺陷进行分类研究。
（一）plc代码逻辑缺陷
plc代码逻辑缺陷具有隐蔽性强的特性，难以发现，可以潜伏多年，传统的安全防御思路无法解决这方面问题。在工业控制系统中，一次开关动作不执行，工艺执行流程的改变以及特定的输出响应故障都可能造成毁灭性的破坏。
本文以梯形图语言为例分析plc代码逻辑缺陷，梯形图语言形象直观，与继电器的控制电路的表达方式极为相似。梯形图由触点、线圈等图形符号结合数字指令、算术运算指令、控制指令等指令符号构成，plc代码逻辑缺陷也是由这些元素和组件位置放置不恰当、链接和范围不正确引起的。表1给出了plc代码逻辑缺陷分类及其相关描述。
表1 plc代码逻辑缺陷分类表
通过利用表1中列举的plc代码逻辑缺陷，可实现拒绝服务攻击，中间人攻击、改变控制器正常的工作流程等，对工业控制系统造成难以估量的损失。下面给出几个plc代码缺陷分析和利用。
（1）计时器条件竞争缺陷
plc编程中的计时器可通过设置预设时间触发计时器。定时器完成位元件的不正确放置可能导致涉及定时器完成位的过程和定时器本身进入竞争条件。当定时器完成位成为激活其自身触发机制的必需元素时，发生这种竞争条件使得定时器陷入死循环并使定时器复位。
如图1所示，把计时器的预设值设为0，使得定时器触发位和定时器同时打开，造成计时器持续振荡，使得输出o4.1无法被触发，致使程序流程顺序错误或进程无法关闭等故障，实现拒绝服务攻击。
图1 计时器条件竞争缺陷梯形图
（2）比较函数硬编码缺陷
plc逻辑代码中的数字指令包含比较指令，该比较指令如果编码不正确可能会导致安全隐患，使得恶意用户可以通过比较指令将不正确的数据插入到进程中。这些数据可能会导致进程序列发生变化，或者导致进程完全中止。
如图2所示，假设常开触点i0.1可以触发高压锅炉的初始化，常开触点后连接一个比较函数，o4.1控制高压锅炉的关闭进程。直到a的值大于等于b的值时，o4.1被激活，锅炉停止加热。如果比较元素b不参考符号表中的数值而是使用定值进行硬编码，b中的数据是不受保护的，我们通过提高b的温度值，使得高压锅炉不断加热直到设备损坏甚至发生爆炸。
图2 比较函数缺陷梯形图
（3）跳转和链接缺陷
跳转和链接缺陷是由一些可影响程序执行顺序的跳转指令和逻辑块指令的错误的跳转到某个程序段而引起。这种类型的代码缺陷类似于中间人攻击，攻击者可以利用错误的跳转指令跳转到一个非预期的位置，并且把在非预期的位置插入恶意的程序段，再返回到跳转之前的位置。
图3给出了基于跳转和链接缺陷的代码利用方法，我们可以利用跳转到子程序jsr函数从file1跳转到恶意代码文件file3中，引入恶意的子程序再返回到jsr跳转之前位置，完成恶意代码的插入，实现中间人攻击。
图3 跳转和链接缺陷图
（二）plc代码安全需求规约
除了plc代码逻辑缺陷，plc代码在物理现场的安全需求属性也将决定plc缺陷利用的成功与否。安全需求属性是由工业控制现场的安全要求决定，指的是为了保证工业控制系统的安全，对设备状态、时序、时间、输入输出量等的约束。如一个电机的额定转速不超过2000rpm以及交叉路口的绿灯不能同时点亮等约束条件。在代码中可能由于程序员的疏忽导致违反安全需求属性的情况，就需要对其进行检测。可见安全需求属性不是常量，而需要实际用户进行描述并输入到检测器中。pavlovic等对plc的设备状态、时序、时间、输入输出量等安全需求进行了约束。本文将安全需求总结为分为以下五类，如表2所示。
表2 plc代码安全需求规约表
第三部分 plc代码形式化分析与验证
plc代码采用“顺序扫描，不断循环”的工作方式，典型的plc的工作过程包括三个不同阶段：把输入数据读入存储器、处理存储器中的数据和更新输出数据。plc程序仅包含有限的状态集合和有限的变量，且程序内部不包含循环，安全需求依赖于输出变量等，所以在一定程度上形式化验证技术适用于plc程序安全分析和恶意代码检测。
形式化分析分为定理证明和模型检测两种方法，定理证明过程过于复杂和冗繁，实际中利用定理证明来验证plc程序正确性的研究并未得到认可。模型检测是一种广泛使用的形式化方法，他更适合用于plc代码的验证，相比于传统的计算机程序，对低级的plc程序建模会更容易，因为他的状态转换系统相对简单。
（一）plc形式化分析中面临的困难
（1）plc缺乏高级编程语言
plc编程属于低级编程语言且编程语言众多，语法语义晦涩，采用分层寻址，地址寻址复杂，存在隐式的类型数据，建模难度大，语言属性易丢失。
（2）时间建模缺失
工业控制系统的实时性要求很高，因此对时间进行建模极为重要，时间建模的对象应包括定时器的累积时间、单条指令的运行时间和执行周期时间，由于定时器是跨循环周期的全局变量，建模时将时间考虑在内会极大地提高建模的难度并增加检测的时间，但不考虑时间就无法检测出与时间相关的安全规约。
（3）物理环境建模缺失
工控系统与物理环境关系密切，工业控制器的输入一般可以认为是物理环境的输出，输出一般可以认为是物理环境的输入，构成一个闭环回路，不考虑物理环境就无法精确地模拟出工业控制器的行为。
（4）状态空间爆炸
plc代码包含的变量多，状态空间大，对plc代码进行建模分析是建立在状态转化基础上的，如果直接进行模型检测会造成状态空间爆炸的问题。
（二）plc代码形式化分析
plc代码形式化验证旨在检测出plc代码缺陷，防止恶意代码的入侵。目前通过形式化验证方式发现plc代码缺陷的研究主要集中于对plc代码形式化模型构建、plc代码缺陷及安全需求规约描述以及plc代码模型检测技术的研究，如图4所示。
（三）plc控制代码检测的技术路线
（1）中间语言翻译
由于工业控制器支持多种标准编程语言，且语法语义上都有较大差异，现有的模型检测技术大都基于特定的编程语言，为了降低建模的复杂性，我们需要把plc编程语言转化成模型检测器可以处理的中间语言。
darvas等提出了将plc程序的scl语言转化为基于nusmv的中间模型方法，它是一种接近于自动机模型的中间模型。mclaughlin等给出了将plc的指令表il语言代码翻译为基于vine的中间语言ilil的方法。zonouz等通过反编译的方法将mc7code转化为中间语言ilil，该中间语言ilil同样使用bitblaze二进制分析工具vine插件来描述。
（2） 时间模型构建
工业控制系统的实时性要求很高，因此时间是很重要的建模对象。延时寄存器（on-delay timer，ton）用于确保plc中实时性属性，ton指令为plc的输入信号提供延迟机制。对ton计时器建模会极大地提高建模的难度并增加检测的时间，但不考虑时间就无法检测出与时间相关的安全规约。因此对ton计时器的形式化验证成为plc代码形式化验证的瓶颈之一。
近年来也有一些对ton计时器的建模研究，masder等最早开始这方面的研究，他们将il程序转换为时间自动机模型并使用自动机和prometa模型两种方式对计时器建模。willems使用时间自动机对ton模型建模计来解决关于ton的问题。wan等在定理证明器coq中针对梯形图语言对ton计时器进行形式化验证，但没有给出通用模块的plc程序形式化描述。sidi在定理证明器coq中针对指令表语言对ton计时器进行形式化验证。
（3）模型检测技术
模型检测是一种广泛使用的自动化验证技术，选择合适的模型来验证系统，并且通过系统地探测建模来检查所要验证的所需属性。由于模型检测可以自动执行，并能在系统不满足性质时提供反例路径，因此在工业界比演绎证明更受推崇。模型检测在plc系统安全的验证方面特别有用，因为与传统的计算机编程相比，可以更容易地将低级plc代码建模为状态转换系统。
目前研究中用到的模型检测工具有很多， 如smv、uppaal、spin等。yoo等使用verilog模型和cadencesmv模型对核电站控制系统的plc代码进行模型检查。mclaughlin等开发了一个tsv
（trusted safety verifier）工具，该工具是利用teg（temporal execution graph）图来进行模型检测，在原始的il代码对输出变量赋值再转换到ilii中间语言，依据被给的安全需求，tsv使用生成的teg图来决定具体的原子命题值。zonouz等同样利用teg图的方法进行模型检测，先对线性时序逻辑规范公式进行取反接着得到teg-ur图模型p，然后在模型m中搜寻满足的路径，最后，如果在第三步中不存在任何路径，则可认为原始代码满足安全需求，能够安全地执行。如果存在路径，则可以通过违反约束的路径条件得到相应的反例。
实际开发的plc程序包含的多个变量和状态空间，执行路径较复杂。会遇到状态空间爆炸的问题。解决状态空间爆炸问题最有效的方法是符号执行，mclaughlin等提出一种合并具有相同输出的输入来避免等价状态生成的状态聚合方法。guo等提出了一种用于自动测试plc编程语言符号执行工具symplc。symplc将plc源代码作为输入，并在应用符号执行之前将其转换为c语言，以系统的生成测试输入来覆盖每个周期任务中的所有路径。为此，他们提出了一些plc特定缩减技术，用于识别和消除冗余。
在工业控制系统中，一个微小的代码缺陷可能影响到整个工业流程遭受破坏甚至威胁到生命财产安全。本文围绕着工业控制系统控制代码安全展开研究，从plc代码逻辑缺陷、代码安全需求规约两个方面对工控代码缺陷进行分类，并结合了现实中常见的梯形图逻辑缺陷构造了代码利用场景，基于这些代码逻辑缺陷实现了对工业控制系统的拒绝服务攻击，中间人攻击等。plc代码形式化验证是发现plc代码缺陷的一种重要且有效的方法，文章最后围绕着如何实现，简要从中间语言翻译，时间模型构建和模型检测技术三个方面阐述了plc代码形式化验证的技术路线及研究进展。
5G SA终端规模商用需要整个产业链作出怎样的努力？
上汽奥迪第二款量产车型曝光：或为Q8
iQOO公布新机充电测试结果 4000mAh大电池从1.21%到100%仅用46分钟
如何设计微波或光子通信中的非互易设备？
Mass Storage协议
PLC代码利用相关研究,PLC代码缺陷分类
将气体流量传感器y应用于制氧机流量监测中
压电加速度计的工作原理
LED真实与照
Modbus转ethercat网关在农业中的应用主要体现
关于TCP协议总结的硬核干货
什么是汽车的ABD-自动制动差速器
芯片的流片方式有哪几种
魅蓝6评测 彻彻底底的百元机
第三季度全球整体电信设备市场报告发布，华为以绝对优势领先
亚马逊云计算营收排名首位 阿里巴巴第二季云计算营收劲增130%
机器视觉LED光源分类及特点解析
未来电视智能化的时代开启
如今哪些手机最受关注？魅蓝5s已成热度最高千元机！
诚意满满的小米6，准备倒计时了
1、plc代码利用相关研究
2、plc代码缺陷分类：plc代码逻辑缺陷、plc代码安全需求规约
3、plc代码形式化分析与验证：plc形式化分析中面临的困难、plc代码形式化分析
随着工业控制系统由封闭走向互联，大量的控制器配备了以太网通信组件，使得攻击者可以直接访问plc硬件及其编程软件。但plc逻辑控制层缺少认证和监测等保护措施，plc代码的安全缺陷成为工业控制系统的重要安全威胁之一。
第一部分 plc代码利用相关研究
与传统的编程语言一样，plc存在代码安全缺陷，而这些代码安全缺陷为攻击者攻击工业控制系统留下了后门。
2013年south carolina大学的sidney对plc代码设计安全缺陷进行了深入的研究，并把plc代码设计级缺陷主要分为基于硬件缺陷和基于软件缺陷两种。攻击者可以利用plc代码缺陷破坏代码逻辑，进行中间代码插桩，实现任意代码执行等。
2014年北京科技大学李伟泽等提出和分析了一种针对scada系统的新型的网络物理攻击——伪逻辑攻击。
2015年在blackhat-us会议上klick等在西门子s7-300中注入了一种新型的后门，通过注入工具实现了在s7-300上进行snmp扫描sock5代理功能。作者利用plc程序中存在跳转指令的安全缺陷，成功在主程序ob1前嵌入恶意指令从而可以控制plc的启停以及输出寄存器。
2016年11月在blackhat欧洲会议上ali abbasi等实现了对plc输入/输出接口的新攻击，该攻击通过篡改输出输入引脚改变系统的运行逻辑。
2017年3月，来自印度海德拉巴和新加坡的学者，演示了针对工业控制系统的plc梯形图逻辑炸弹（ladder logic bombs，llb）。该逻辑炸弹是用梯形图语言编写的恶意软件，这种恶意软件可被攻击者注入到plc现有控制逻辑中，通过改变控制动作或者等待特定的触发信号来激活恶意行为，以实现传感器数据篡改，系统敏感信息获取以及plc拒绝服务攻击等。
第二部分 plc代码缺陷分类
不同于传统的it系统，工业控制系统有其特殊的编程语言，根据国际电工委员会制定的工业控制编程语言标准（iec61131-3），plc的编程语言包括以下五种：梯形图语言（ladderlogic programming language，ld）、指令表语言（instruction list，il）、功能模块图语言（function block diagram，fbd）、顺序功能流程图语言（sequential function chart，sfc）及结构化文本语言（structured text，st）。本文中的代码缺陷研究也是基于上述编程语言展开的。
工业控制系统的入侵与传统互联网入侵虽然手段上大同小异，但工业控制系统的部署与其物理工艺流程紧耦合，因此利用工艺流程中的代码逻辑缺陷成为针对工业控制系统的有效打击手段之一，如陷阱门、逻辑炸弹、特洛伊木马、蠕虫、zombie等，且这类新的恶意代码具有更强的传播能力和破坏性。本文主要研究基于软件的plc代码缺陷，并从代码逻辑缺陷和违反安全需求规约两个方面对plc代码缺陷进行分类研究。
（一）plc代码逻辑缺陷
plc代码逻辑缺陷具有隐蔽性强的特性，难以发现，可以潜伏多年，传统的安全防御思路无法解决这方面问题。在工业控制系统中，一次开关动作不执行，工艺执行流程的改变以及特定的输出响应故障都可能造成毁灭性的破坏。
本文以梯形图语言为例分析plc代码逻辑缺陷，梯形图语言形象直观，与继电器的控制电路的表达方式极为相似。梯形图由触点、线圈等图形符号结合数字指令、算术运算指令、控制指令等指令符号构成，plc代码逻辑缺陷也是由这些元素和组件位置放置不恰当、链接和范围不正确引起的。表1给出了plc代码逻辑缺陷分类及其相关描述。
表1 plc代码逻辑缺陷分类表
通过利用表1中列举的plc代码逻辑缺陷，可实现拒绝服务攻击，中间人攻击、改变控制器正常的工作流程等，对工业控制系统造成难以估量的损失。下面给出几个plc代码缺陷分析和利用。
（1）计时器条件竞争缺陷
plc编程中的计时器可通过设置预设时间触发计时器。定时器完成位元件的不正确放置可能导致涉及定时器完成位的过程和定时器本身进入竞争条件。当定时器完成位成为激活其自身触发机制的必需元素时，发生这种竞争条件使得定时器陷入死循环并使定时器复位。
如图1所示，把计时器的预设值设为0，使得定时器触发位和定时器同时打开，造成计时器持续振荡，使得输出o4.1无法被触发，致使程序流程顺序错误或进程无法关闭等故障，实现拒绝服务攻击。
图1 计时器条件竞争缺陷梯形图
（2）比较函数硬编码缺陷
plc逻辑代码中的数字指令包含比较指令，该比较指令如果编码不正确可能会导致安全隐患，使得恶意用户可以通过比较指令将不正确的数据插入到进程中。这些数据可能会导致进程序列发生变化，或者导致进程完全中止。
如图2所示，假设常开触点i0.1可以触发高压锅炉的初始化，常开触点后连接一个比较函数，o4.1控制高压锅炉的关闭进程。直到a的值大于等于b的值时，o4.1被激活，锅炉停止加热。如果比较元素b不参考符号表中的数值而是使用定值进行硬编码，b中的数据是不受保护的，我们通过提高b的温度值，使得高压锅炉不断加热直到设备损坏甚至发生爆炸。
图2 比较函数缺陷梯形图
（3）跳转和链接缺陷
跳转和链接缺陷是由一些可影响程序执行顺序的跳转指令和逻辑块指令的错误的跳转到某个程序段而引起。这种类型的代码缺陷类似于中间人攻击，攻击者可以利用错误的跳转指令跳转到一个非预期的位置，并且把在非预期的位置插入恶意的程序段，再返回到跳转之前的位置。
图3给出了基于跳转和链接缺陷的代码利用方法，我们可以利用跳转到子程序jsr函数从file1跳转到恶意代码文件file3中，引入恶意的子程序再返回到jsr跳转之前位置，完成恶意代码的插入，实现中间人攻击。
图3 跳转和链接缺陷图
（二）plc代码安全需求规约
除了plc代码逻辑缺陷，plc代码在物理现场的安全需求属性也将决定plc缺陷利用的成功与否。安全需求属性是由工业控制现场的安全要求决定，指的是为了保证工业控制系统的安全，对设备状态、时序、时间、输入输出量等的约束。如一个电机的额定转速不超过2000rpm以及交叉路口的绿灯不能同时点亮等约束条件。在代码中可能由于程序员的疏忽导致违反安全需求属性的情况，就需要对其进行检测。可见安全需求属性不是常量，而需要实际用户进行描述并输入到检测器中。pavlovic等对plc的设备状态、时序、时间、输入输出量等安全需求进行了约束。本文将安全需求总结为分为以下五类，如表2所示。
表2 plc代码安全需求规约表
第三部分 plc代码形式化分析与验证
plc代码采用“顺序扫描，不断循环”的工作方式，典型的plc的工作过程包括三个不同阶段：把输入数据读入存储器、处理存储器中的数据和更新输出数据。plc程序仅包含有限的状态集合和有限的变量，且程序内部不包含循环，安全需求依赖于输出变量等，所以在一定程度上形式化验证技术适用于plc程序安全分析和恶意代码检测。
形式化分析分为定理证明和模型检测两种方法，定理证明过程过于复杂和冗繁，实际中利用定理证明来验证plc程序正确性的研究并未得到认可。模型检测是一种广泛使用的形式化方法，他更适合用于plc代码的验证，相比于传统的计算机程序，对低级的plc程序建模会更容易，因为他的状态转换系统相对简单。
（一）plc形式化分析中面临的困难
（1）plc缺乏高级编程语言
plc编程属于低级编程语言且编程语言众多，语法语义晦涩，采用分层寻址，地址寻址复杂，存在隐式的类型数据，建模难度大，语言属性易丢失。
（2）时间建模缺失
工业控制系统的实时性要求很高，因此对时间进行建模极为重要，时间建模的对象应包括定时器的累积时间、单条指令的运行时间和执行周期时间，由于定时器是跨循环周期的全局变量，建模时将时间考虑在内会极大地提高建模的难度并增加检测的时间，但不考虑时间就无法检测出与时间相关的安全规约。
（3）物理环境建模缺失
工控系统与物理环境关系密切，工业控制器的输入一般可以认为是物理环境的输出，输出一般可以认为是物理环境的输入，构成一个闭环回路，不考虑物理环境就无法精确地模拟出工业控制器的行为。
（4）状态空间爆炸
plc代码包含的变量多，状态空间大，对plc代码进行建模分析是建立在状态转化基础上的，如果直接进行模型检测会造成状态空间爆炸的问题。
（二）plc代码形式化分析
plc代码形式化验证旨在检测出plc代码缺陷，防止恶意代码的入侵。目前通过形式化验证方式发现plc代码缺陷的研究主要集中于对plc代码形式化模型构建、plc代码缺陷及安全需求规约描述以及plc代码模型检测技术的研究，如图4所示。
（三）plc控制代码检测的技术路线
（1）中间语言翻译
由于工业控制器支持多种标准编程语言，且语法语义上都有较大差异，现有的模型检测技术大都基于特定的编程语言，为了降低建模的复杂性，我们需要把plc编程语言转化成模型检测器可以处理的中间语言。
darvas等提出了将plc程序的scl语言转化为基于nusmv的中间模型方法，它是一种接近于自动机模型的中间模型。mclaughlin等给出了将plc的指令表il语言代码翻译为基于vine的中间语言ilil的方法。zonouz等通过反编译的方法将mc7code转化为中间语言ilil，该中间语言ilil同样使用bitblaze二进制分析工具vine插件来描述。
（2） 时间模型构建
工业控制系统的实时性要求很高，因此时间是很重要的建模对象。延时寄存器（on-delay timer，ton）用于确保plc中实时性属性，ton指令为plc的输入信号提供延迟机制。对ton计时器建模会极大地提高建模的难度并增加检测的时间，但不考虑时间就无法检测出与时间相关的安全规约。因此对ton计时器的形式化验证成为plc代码形式化验证的瓶颈之一。
近年来也有一些对ton计时器的建模研究，masder等最早开始这方面的研究，他们将il程序转换为时间自动机模型并使用自动机和prometa模型两种方式对计时器建模。willems使用时间自动机对ton模型建模计来解决关于ton的问题。wan等在定理证明器coq中针对梯形图语言对ton计时器进行形式化验证，但没有给出通用模块的plc程序形式化描述。sidi在定理证明器coq中针对指令表语言对ton计时器进行形式化验证。
（3）模型检测技术
模型检测是一种广泛使用的自动化验证技术，选择合适的模型来验证系统，并且通过系统地探测建模来检查所要验证的所需属性。由于模型检测可以自动执行，并能在系统不满足性质时提供反例路径，因此在工业界比演绎证明更受推崇。模型检测在plc系统安全的验证方面特别有用，因为与传统的计算机编程相比，可以更容易地将低级plc代码建模为状态转换系统。
目前研究中用到的模型检测工具有很多， 如smv、uppaal、spin等。yoo等使用verilog模型和cadencesmv模型对核电站控制系统的plc代码进行模型检查。mclaughlin等开发了一个tsv
（trusted safety verifier）工具，该工具是利用teg（temporal execution graph）图来进行模型检测，在原始的il代码对输出变量赋值再转换到ilii中间语言，依据被给的安全需求，tsv使用生成的teg图来决定具体的原子命题值。zonouz等同样利用teg图的方法进行模型检测，先对线性时序逻辑规范公式进行取反接着得到teg-ur图模型p，然后在模型m中搜寻满足的路径，最后，如果在第三步中不存在任何路径，则可认为原始代码满足安全需求，能够安全地执行。如果存在路径，则可以通过违反约束的路径条件得到相应的反例。
实际开发的plc程序包含的多个变量和状态空间，执行路径较复杂。会遇到状态空间爆炸的问题。解决状态空间爆炸问题最有效的方法是符号执行，mclaughlin等提出一种合并具有相同输出的输入来避免等价状态生成的状态聚合方法。guo等提出了一种用于自动测试plc编程语言符号执行工具symplc。symplc将plc源代码作为输入，并在应用符号执行之前将其转换为c语言，以系统的生成测试输入来覆盖每个周期任务中的所有路径。为此，他们提出了一些plc特定缩减技术，用于识别和消除冗余。
在工业控制系统中，一个微小的代码缺陷可能影响到整个工业流程遭受破坏甚至威胁到生命财产安全。本文围绕着工业控制系统控制代码安全展开研究，从plc代码逻辑缺陷、代码安全需求规约两个方面对工控代码缺陷进行分类，并结合了现实中常见的梯形图逻辑缺陷构造了代码利用场景，基于这些代码逻辑缺陷实现了对工业控制系统的拒绝服务攻击，中间人攻击等。plc代码形式化验证是发现plc代码缺陷的一种重要且有效的方法，文章最后围绕着如何实现，简要从中间语言翻译，时间模型构建和模型检测技术三个方面阐述了plc代码形式化验证的技术路线及研究进展。
5G SA终端规模商用需要整个产业链作出怎样的努力？
上汽奥迪第二款量产车型曝光：或为Q8
iQOO公布新机充电测试结果 4000mAh大电池从1.21%到100%仅用46分钟
如何设计微波或光子通信中的非互易设备？
Mass Storage协议
PLC代码利用相关研究,PLC代码缺陷分类
将气体流量传感器y应用于制氧机流量监测中
压电加速度计的工作原理
LED真实与照
Modbus转ethercat网关在农业中的应用主要体现
关于TCP协议总结的硬核干货
什么是汽车的ABD-自动制动差速器
芯片的流片方式有哪几种
魅蓝6评测 彻彻底底的百元机
第三季度全球整体电信设备市场报告发布，华为以绝对优势领先
亚马逊云计算营收排名首位 阿里巴巴第二季云计算营收劲增130%
机器视觉LED光源分类及特点解析
未来电视智能化的时代开启
如今哪些手机最受关注？魅蓝5s已成热度最高千元机！
诚意满满的小米6，准备倒计时了