摘要： 基于规则的脆弱性分析技术依赖于对系统组件间关系的经验知识,系统复杂性、竞态条件、隐含假设等因素,使规则的生成异常困难。该文提出了采用NuSMV作为Model Checking执行机验证系统安全行为模型的脆弱性分析方法,并详细描述了对两个模型实例进行验证的过程。结果显示,这种方法具有识别已知和未知脆弱性的能力。

关键词: 脆弱性, Modelchecking, NuSMV

Abstract: Techniques based on rules for analysis of vulnerabilities rely on experiences of the interactions of system's components, which appear hard to obtain because of the complexity of system, race condition and underlying assumption. The paper uses NuSMV as model checker to analyze the vulnerabilities of system model, and gives details on verifying two instances. Results show that this approach is capable of identifying known and also unknown system vulnerabilities.

中图分类号: 

• TP393.08