一句话:提出一种面向动态架构组件系统的自动化形式化安全分析方法,通过抽象与增量分析提升运行时可扩展性。
动态软件系统(如自适应系统)的体系结构在运行时会发生变化,为推理并强制安全策略,需要自动化的分析与验证,但现有方法在运行时分析中常面临可扩展性瓶颈。本文提出一种自动化的形式化方法,用于分析具有动态架构的基于组件的系统安全性质。该方法利用形式抽象与增量分析技术降低运行时分析的复杂度,从而支持体系结构动态变化下的组合式安全推理。作者实现了原型并在广泛使用的自适应系统范例 ZNN 上进行了评估;实验结果表明该方法能有效缓解可扩展性问题。
To reason about and enforce security in dynamic software systems, automated analysis and verification approaches are required. However, such approaches often encounter scalability issues, particularly when employed for runtime analysis, which is necessary in software systems with dynamically changing architectures, such as self-adaptive systems. In this work, we propose an automated formal approach for security analysis of component-based systems with dynamic architectures. This approach leverages formal abstraction and incremental analysis techniques to reduce the complexity of runtime analysis. We have implemented and evaluated our approach against ZNN, a widely known self-adaptive system exemplar. Our experimental results demonstrate the effectiveness of our approach in addressing scalability issues.