Windows Vista用户帐户控制机制的反向建模分析

形式化建模分析是发现系统漏洞的有效方法之一，为了解决正向建模对非开源软件进行分析的困难，本文提出了一种反向建模的分析方法。反向建模是一个反馈式的过程。利用模型检验工具验证分析生成的反例在真实系统中进行确认，若反例没有得到确认则对模型进行修正，然后再次进行验证，如此反复。直至反例得到确认，即可得到较为准确的模型并发现系统的不足。本文使用该方法对Windows Vista用户帐户控制机制进行了分析，发现了其不足，取得了较好的效果。