首先,建立具有良好描述性和操作性的脆弱性模型.这个模型除了用于总结、帮助理解已知脆弱性的特征和性质外,更重要地是为建立脆弱性测试的基本缺陷库提供指导.接下来,从两个方面进行脆弱性发现.第一,将软件缺陷注入技术和脆弱性测试分析相结合,实现了基于环境缺陷注入的两个脆弱性测试系统.测试系统在程序与环境进行交互的接口上注入根据脆弱性模型产生的缺陷,然后观测程序的反应,如果程序有违反系统安全策略的行为,就可认为发现了程序中存在的脆弱性.测试系统初步解决了包括避免测试例的组合爆炸、环境恢复以及分布式测试等技术问题,基本具备了自动化脆弱性测试能力,并在实际测试中发现了若干已知漏洞.第二,基于Model Checking的形式化安全性验证.建立简化的Unix系统(主要是文件系统)的模型后,采用NuSMV作为Model Checking执行机,验证系统安全行为模型是否满足安全约束.从实际效果来看,这种方法可以完整地复现某些已知脆弱性.由于NuSMV是在系统行为模型中并未包含关于脆弱性的知识的情况下给出攻击步骤的,因此这种方法具有识别未知脆弱性的能力.