作者：解放军信息工程大学 耿洋洋，常天佑，魏强

摘要：可编程逻辑控制器代码安全是确保工业控制系统安全运行的核心，本文围绕着可编程逻辑控制器的代码安全缺陷进行分析，首先阐述了工控代码安全的相关研究。接着，从可编程逻辑控制器代码逻辑缺陷、安全需求规约两个方面对工控代码缺陷进行分类，分析了针对梯形图语言的3种代码逻辑缺陷产生的机理，并结合梯形逻辑图，利用PLC代码逻辑缺陷，实现拒绝服务攻击、中间人攻击等。最后，本文提出了PLC代码形式化验证中面临的困难，并从中间语言翻译、模型构建和模型检测三方面综述了PLC代码形式化验证的相关研究。

关键词：可编程逻辑控制器；工业控制系统；代码缺陷分析；形式化验证

在线预览：可编程逻辑控制器代码安全缺陷分析综述

摘自《自动化博览》2018年2月刊