信息安全研究 ›› 2017, Vol. 3 ›› Issue (7): 601-609.

• 赛博物理系统(CPS) 专题 • 上一篇    下一篇

基于时间自动机的 CPS 安全建模和验证

苏琪   

  1. 浙江工业大学计算机科学与技术学院杭州310023
  • 收稿日期:2017-07-19 出版日期:2017-07-15 发布日期:2017-07-18
  • 通讯作者: 苏琪
  • 作者简介:硕士研究生,主要研究方向为形式化方法、信息安全.

Modeling and Verifying Security Properties of Cyber-Physical System Based on Timed Automata

  • Received:2017-07-19 Online:2017-07-15 Published:2017-07-18

摘要: 信息物理融合系统(cyber-physical system, CPS)作为一个新的研究方向,在其研究与发展过程中遇到了众多的问题,一些关于CPS安全的问题逐渐呈现.对CPS的设计安全进行探索性研究,主要针对CPS系统各部分之间如何安全地交互进行建模,并讨论安全数据的攻击及其防御措施的有效性.以网络化水位控制系统为例,以时间自动机为形式化建模语言对系统进行建模、验证和分析.建模过程中,采用分层的安全体系结构,分别将系统的各个组成部分的工作抽象为时间自动机模型.这些模型组成一个系统,刻画出完整的CPS工作过程.最后,利用模型检测工具PAT验证系统恢复机制的有效性.

关键词: 时间自动机, 形式化方法, 信息物理融合系统(CPS), 安全, 验证, 建模

Abstract: Cyber-physical system (CPS), as a new research direction, has encountered a lot problems in the research and development. There are some problems about CPS security gradually appeared. In this paper, the design safety of CPS is explored. We mainly make a model on the safe interaction between the various parts of the CPS and discuss the security data attacks and the effectiveness of its defense measures. In this paper, we use the network water level control system as an example, and timed automata as formal modeling language for modeling, validating and analysing. In the process of modeling, we utilize a layered safety architecture. The work of each component of the system is respectively abstracted as a timed automata model. Those models constitute a system which describe the complete work process of CPS. Finally, by using the model-checking tool PAT, we present a verification for the effectiveness of automated recovery mechanism.

Key words: timed automata, formal method, cyber-physical system, safety, verification, modeling