基于Model Checking的系统脆弱性分析

摘要

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