基于系统理论过程分析的安全关键软件安全性验证方法

现代安全关键系统的功能实现越来越依赖于软件，这导致软件的安全性对系统安全至关重要，而软件的复杂性使得采用传统安全性分析方法很难捕获组件交互过程带来的危险。为保证安全关键系统的安全性，提出一种基于系统理论过程分析（STPA）的软件安全性验证方法。在安全控制结构基础上，通过构建带有软件过程模型变量的过程模型，细化分析危险行为发生的系统上下文信息，并以此生成软件安全性需求。然后通过设计起落架控制系统软件，采用模型检验技术对软件进行安全性验证。结果表明，所提方法能够在系统级层面有效识别出软件中潜在的危险控制路径，并可以减少对人工分析的依赖。

Security verification method of safety critical software based on system theoretic process analysis

Functional implementation of modern safety critical systems is increasingly dependent on software. As a result, software security is very important to system security, and the complexity of software makes it difficult to capture the dangers of component interactions by traditional security analysis methods. In order to ensure the security of safety critical systems, a software security verification method based on System Theoretic Process Analysis (STPA) was proposed. On the basis of the security control structure, by constructing the process model with software process model variables, the system context information of dangerous behavior occurrence was specified and analyzed, and the software security requirements were generated. Then, through the landing gear control system software design, the software security verification was carried out by the model checking technology. The results show that the proposed method can effectively identify the potential dangerous control paths in the software at the system level and reduce the dependence on manual analysis.