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

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