安全关键系统是指若系统失效或误动作，会产生人员重伤或死亡，或者设备的严重毁损，或者环境的危害后果的系统。在物联网等网络化系统迅猛发展的当下，对安全关键系统的控制越来越多地使用网络进行。保障安全关键系统的可靠性已不再仅仅局限于系统本身硬件和软件的稳定运行，更需要深入考虑网络攻击可能给系统功能带来的严重威胁与破坏。由于安全关键系统失效将引发极其严重的后果，其影响深远且难以估量。因此，识别与防御针对安全关键系统的网络攻击变得格外关键。基于离散事件系统理论，本研究对网络攻击下系统的建模与攻击识别，以及传感器攻击下安全编辑函数的设计问题进行了研究。
针对攻击下系统的建模与攻击识别问题，本研究对攻击识别问题进行了形式化定义，指出该问题可通过计算特定的攻击识别函数来解决。本研究设计了一种算法，旨在构建网络攻击下受控系统的模型，该模型详细记录了系统在遭受攻击时的所有潜在行为及攻击类型。在此基础上，进一步构建其观测自动机，用以计算攻击识别函数。研究结果显示，解决攻击识别问题的复杂度与系统规模之间呈指数级的关系。最后，利用Python语言对所提出的算法进行了仿真实现。
针对传感器攻击下安全编辑函数设计问题，本研究对安全编辑函数、安全编辑函数存在性验证问题和安全编辑函数设计问题进行了形式化定义。为了有效地解决编辑函数存在性验证问题，提出设计全攻击与编辑结构（All Insert and Edit Structure，AEAS）的方法，该结构描述了系统、编辑函数、传感器攻击者及控制器之间的相互作用。基于AEAS框架，提出了全攻击与编辑修剪结构（All Insert and Edit-Trim Structure，AEAS-T）的算法，给出了安全编辑函数存在的充分必要条件，有效解决了编辑函数存在性的验证问题。进一步地，为解决编辑函数设计问题，提出确立编辑函数设计结构的算法。最后，利用Python语言实现了所提出算法的实现与仿真。
本研究聚焦于安全关键系统内的一个具体案例——有轨电车平交路口信号系统，并采用前文提出的理论框架对该系统进行建模、攻击识别以及安全编辑函数的设计。在有轨电车穿越路口的情景下，对有轨电车平交路口信号系统进行建模，描述其正常工作逻辑过程。识别平交路口可能遭受的传感器攻击与执行器攻击，并针对由此可能导致的路权冲突和系统失效两种不期望的情形，设计了安全编辑函数以进行防御，确保了平交路口信号系统的安全与稳定运行，进而验证了所提出理论的准确性与实用性。

Safety critical systems are defined as systems that, in the event of failure or malfunction, could result in serious injury or death to personnel, severe damage to equipment, or significant environmental hazards. In the rapidly evolving landscape of networked systems such as the Internet of Things, control of safety-critical systems is increasingly carried out using networks. Ensuring the reliability of safety critical systems now extends beyond the stable operation of hardware and software components alone; it necessitates a thorough consideration of the potential threats and disruptions posed by network attacks on system functionality. Given the potentially catastrophic consequences associated with safety critical systems, their impacts are profound and difficult to quantify. Therefore, the identification and defense against network attacks targeting safety critical systems becomes paramount. Drawing upon the theory of discrete event systems, this thesis investigates the modeling and attack identification of systems under network attacks, as well as the design of safe edit functions under sensor attacks.
For the problem of modeling and identifying attacks on systems, this thesis offers a formal delineation of the attack identification problem, asserting that it can be addressed through the computation of a dedicated attack identification function. The study introduces an algorithm aimed at constructing a model of the targeted system under cyber-attack, elucidating all potential system behaviors in the face of attacks and delineating various attack types. Subsequently, an observer is devised to facilitate the computation of the attack identification function. The findings underscore an exponential correlation between the complexity of resolving the attack identification problem and the system's scale. Finally, the proposed algorithm is realized through coding and implementation in the Python language.
To address the safe edit function design problem under sensor attacks, this paper formally defines the safe edit function, the safe edit function existence verification problem and the safe edit function design problem. In order to effectively solve the verification problem of the existence of the edit function, the algorithm for constructing the All Insert and Edit Structure (AEAS), which describes the interactions between the system, the edit function, the sensor attacker and the supervisor, is proposed. Based on the AEAS framework, the algorithm of All Insert and Edit-Trim Structure (AEAS-T) is proposed, which gives the sufficient and necessary conditions for the existence of a secure edit function, and effectively solves the problem of verifying the existence of the edit function. Further, to solve the edit function design problem, the algorithm to establish the edit function design structure is proposed. As a conclusion of the research, the coding of the proposed algorithm is implemented using Python language.
This paper focuses on a specific case within safety-critical systems, the tram level crossing signalling system. The theoretical framework presented in the previous paper is used for modelling, attack identification and design of safe edit functions for this system. In the scenario of a tram crossing an intersection, the tram level crossing signalling system is modelled to describe its normal operating logic process. Sensor and actuator attacks on the level crossing are identified, and a safe edit function is designed to defend against the undesired scenarios of right-of-way conflict and system failure, ensuring the safe and stable operation of the level crossing signalling system, and thus verifying the accuracy and practicability of the proposed theory.