windows vista用户帐户控制机制的反向建模分析.pdf

收藏

编号:20181110221227437248    类型:共享资源    大小:242.87KB    格式:PDF    上传时间:2019-02-16
  
2
金币
关 键 词:
windowsvista用户帐户控制机制的反向建模分析
资源描述:
doi:10。3969,j.issn.1671—1122.2009.10。017 Windows Vista用户 帐户控制机制的反向建模分析 赵栋,罗军,王蕾 (国防科技大学,湖南长沙410073) j 摘要:形式化建模分析是发现系统漏洞的有效方法之一,为了解决正向建模时非开源软件进行分析的困难,本文提出了一种 、.反向建模的分析方法。反向建模是一个反馈式的过程,利用模型检验工具验证分析生成的反例在真实系统申进行确认,若反例没有 ,得到确认则对模型进行修正,然后再次进行验证,如此反复,直至反例得到确认,即可得到较为准确的模型并发现系统的不足。本 ;文使用该方法对WindowsVism用户帐户控制机制进行了分析,发现了其不足,取得了较好的效果。 关键词:Windows Vmm;用户帐户控制;反向建模 : 中图分类号:开309 文献标识码:A ≈. j?? j; 1反向建模的分析方法 与传统的正向建模相比,反向建模是一个反馈式的过程。 对于“黑盒”系统,最初建立的模型是通过实验、文档推测 出来的,难以准确地反应系统的特点。利用模型分析工具生 成的反例进行实验,若反例没有得到确认,则将反例用于指 导模型的修正,多次反复,不断完善模型,直至反例得到确认, 此时得到的模型就相对比较精确地反应了真实的系统。 建模分析需要用形式化的语言描述模型并用相应的工具 进行验证。本文采用Alloy。Alloy是一种基于一阶逻辑的结 构化建模语言【l】,AlloyAnalyzer是Alloy模型的自动分析工具。 在Alloy中,待验证的属性描述为断言(Assertion)。对于给 定的模型,Alloy Analyzer可以验证断言是否成立。如果断言 不成立,Alloy Analyzer将给出反例。 反向建模的分析方法如图l所示,包括构建、提取、转换、 验证及确认修正5个步骤。 图1反向建模的分析方法 1.1构建模型 模型是一个状态转换系统,包括状态的定义和状态转换 规则。系统状态是由集合以及集合之间的关系组成的,它们 都是系统中组件和组件之间关系的抽象。我们把系统的各种 行为抽象为操作。操作会引起系统状态发生改变,我们根据 系统的行为给出状态转换规则。 给定操作名称op,操作前状态S和相应的参数,状态转 换规则给出操作后状态S’,这意味着,系统处于状态S时进行 op操作,系统将转换到状态S’。 为-了使用Alloy语言描述状态转换规则,我们为每个操 作定义一个谓词,每个渭词至少有两个参数:状态S和状态st, 不同的谓词还有各自必需的其他参数。我们把所有的状态和 操作组织成一个单向链表,其中状态和操作交替出现,且链 表头、尾节点都是状态。链表节点之间必须满足状态转换规则。 对于“黑盒”系统,初次建模时,是通过实验、文档描 述推测得到模型。随后通过反例确认的反馈,对模型做出多 次的修正。当反例得到确认时,得到的模型就相对比较准确 地反应了系统的真实状况。 1.2提取期望属性 我们根据一定的原则和文档的描述,提出系统应该具有 的一些属性,称之为期望属性。下一步的工作就是验证系统 是否具备这些期望属性。 1.3期望属性转换成断言 有些期望属性可以通过观察实验得到验证,而有些属性 并不显而易见,通过形式化分析工具的帮助,我们可以验证 系统是否具备期望属性。 期望属性是用自然语言描述的,为了进行形式化验征, 需要以先前构建的Alloy模型为依据,把期望属性转换成 Alloy语言描述的断言(Assert)。 1.4验证及生成反例 使用Alloy A矗alyzer验证断言是否成立。Alloy Analyzer 可以通过生成一个模型的快照来证明某个事实或给出命题成 万方数据 立的实例,我们称之为正例;也可以在限定的范围内穷举各 种情况以验证断言是否成立,若不成立将给出反例。这些反 例将作为测试用例,用于实际系统的测试。 1.5反例的确认和模型的修正 若第四步中断占不成立,并不一定意味着系统不满足期 望属性,有可能是建模过程中的偏差,造成模型没有准确地 反映系统的真卖晴况。 2 UAC简介 2.1引入UAC的目的 Windows内置一个管理员组Administrators和一个标准 用户组Users。前者拥有较高的授权,后者只有较低的授权。 微软一直建议用户平常使用标准用户帐户登陆,只在必要时 才切换到管理员帐户。但用户为了方便通常一直使用管理员帐 户登陆,软件开发商也习惯于假定软件运行在管理员帐户。于 是,微软在Vista中引入了UAC,目的在于限制帐户的权限和 特权,强制用户运行在标准用户的安全环境—Fo 2.2 UAC机制对用户特权的控制 UAC机制是最小特权原则的体现。最小特权原则是安全 系统的重要原则,它要求用户只拥有完成任务所必需的特权, 而不是全部【3】。这使得攻击者即便攻击成功也没有过多的特 权,从而限制攻击者的破坏能力,减少损失。 UAC机制强制任何应用程序只拥有标准用户的权限和特 权,应用程序要想获得更高的权限和特权必须得到明确的授 权跚。只有用户信任的程序才能获得高级特权,恶意程序因 没有所需的特权从而无法对系统造成进一步的破坏。 在Windows安全系统中,有权限(Permission)和特权 (Privilege)的两个概念f31。权限(Permission)是一种许可, 它允许进程对特定的对象进行特定类型的访问,如读、写、 执行等。进程访问资源时会标明期望的访问类型,系统负责 检查进程是否拥有该权限。特权(Privilege)是执行诸如关机、 修改系统配置等关键操作时必需的标志。执行这类操作时, Windows会检查进程的令牌是否包含必需的特权。权限作用 于具体的对象,而特权没有明确的作用对象。 UAC实现了对用户权限和特权的控制,本文关注的是 UAC对用户特权的控制。为了实现对特权的控制,管理员用 户登陆时,系统创建两个令牌:完全令牌(Full Token)和过 滤令牌(Filter Token)[210前者拥有完全的特权,后者过滤掉 了高级特权,只拥有普通特权。管理员用户的第一个进程只 获得过滤令牌,子进程默认继承父进程的令牌。进程创建时, 若系统发现新进程需要高级特权,且父进程的令牌是过滤令 牌,会弹出对话框要求用户确认,在获得用户确认后,进程 将取得完全令牌,从而获得完成任务所需的高级特权,这个 过程称为特权提升。u蛇对木马和误操作有很好的防护效果, 对Windows系统安全是一个显著的增强。 3 UAC特权控制的反向建模分析 3.1 UAC特权控制模型 总结第三章对uAc的分析,我们把用户、组、进程、特权(包 括普通特权和高级特权)等表示为集厶,用二元关系来表示 他们之间的二元关系。下面给出模型的定义。 定义I UAC特权控制模型M=(USER,GROUP,PRO,TASK,PRI, NPRI.HPRI),其中 USER表示片i户集合、GROUP表示组集合、PRO表示进程集合、TASK 表示任务集合、PR f表示特权集合、NPRI表示普通特权集合,HPRI表示高 级特权集合。HPRI和NPRI构成PRI的一个划分。 定义2系统状态s=(V'R),其中: V=(Us,Gs,PROs),lb(Us2Gs,Gs2PRI,Us2PRI,Us2PROs,PROsPRI,PROs2T,T 2PRI) Us、Gs、PROs分别表示一个状态下的用户集合.组集合和进程集At它 们分别是USER、GROUP、PRO的子集。每个状态的Gs集合中缺省有两个元 素Admins和Stusers,分别代表Windows系统中内置的管理员组和标准甩户组。 Us2Gs.Gs2PRI。Us2PR!,Us2PROs,PROs2PRI,PROs2T是二元关系。其中: Us2Gs c USERXGROUP,且是多对多的,表示用户集合与组之问的对应 关系。一个用户可以隶属于多个组,一个组可以包含多个用户。 Gs2PRI∈G8×PRI,Us2PR!∈UsXPRI,且都是多对多的,分别表示组 和特权之|’甘J、用户与特权之间的对应关系。在Windows中可以配置某个特权 授予组也可以授予用户。一个用户可以隶属于一个或多个组。用户可以自身获 得特权,也町以作为一个组的成员获得特权。 Us2PROs∈UsXPROs,且是—对多的,表示用户和进程之间的对应关系。 一个用户拥有多个进程代表其执行各种任务,而每个进程只属于一个用户。 PROs2PRISPROsXPRI.且是多对多的。表示进程与特权之间的对应关系。 进程可以拥有多个特权。一个特权也Ⅱ丁以授予多个进程。进程所拥有的特权 并不一定和进程所属片I户拥有的特权相I司,而是后者的子集,这也是UAC特 权控制的关键。 PROs2T∈PROsXTASK,且是—对多或零对多的,表示进程与任9}之间 的对应关系。一个进程可以执行多个任第一个任务只交给一个进程来执行 或者没有任何进程执行该任务。 T2PRl∈三TASKXPRI,且是多对多的,表示任务和特权之间的对应关系, 完成每个任务都需要相应的特权。 系统所有ur能的状态的集合记为State。 图2所示的是一个状态s下所包含的集合和二元关系。 图2系统状态包含的集合与关系 模型的基本操作如表1所示。 其中最关键的是UserLogon、CreateProcess和Elevate, 这三个操作实现了UAC的特权控制。UserLogon创建登录 万方数据 表1 UAC特权控制模型的操作 操作名称 说明 UserLogon 用户登录 CreateProcess 创建新进程 ExitProcess 终止进程 AddUser 增加用户 DelUser 删除用户,AddUser的逆操作 AddGroup 增加组 DelGroup 删除组。AddGroup的逆操作 AddUseffoGroup 向组中增加用户 DelUserFromGroup 从组中删除用户,AddUserToGroup的逆操作 AuthToGroup 将某特权授F组 AuthToUser 将某特权授予用户 UnAuthFromGroup 取消对组的授权.AuthToGroup的逆操作 UnAuthFromUser 取消对用户的授权,AuthToUser的逆操作 AssignTask 安排进程执行任务 UnAssignTask 取消进程的任务,AssignTask的逆操作 Elevate 进程特权提升 用户的第一个进程,根据特权控制策略赋予进程相应的特 权。CreateProcess创建新进程,子进程继承父进程的特权。 Elevate实现进程的特权提升。 给出了谓词UserLogon的定义,该定义描述了操作 UserLogon的状态转换规则。其中,AssignedMaxPrivileges[s, U】表示在状态s下’用户u可能的最大特权。注意下划线标注 的代码,这段代码的意思是:如果登陆用户是管理员组的成员, 则从用户的第一个进程的最大特权集合中剔除高级特权赋予 该进程,否则赋予最大特权。 3.2期望属性和断言 针对UAC特权控制,本文提出两条期望属性。 期望属性l:任何状态下,任何进程所拥有的高级特权集 合都是此时进程执行的任务所必需的高级特权集合的子集。 期望属性2:任何状态下,任何进程若拥有高级特权, 则或者该进程之前经历过特权提升操作,或者该高级特权是 通过进程的父进程继承得到的。 期望属性l是严格的最小特权原则的体现,期望属性2 是我们期望UAC应有的功能。把这两个属性转换成Alloy语 言描述的断言。 3.3分析结果及改进建议 期望属性1不需要用工具分析就可以发现是不成立的。 UAC对特权的控制是粗粒度的,管理员用户只有两个令牌: 完全令牌和过滤令牌。特权提升操作会赋予进程完全令牌, 把所有的高级特权全部赋予进程,即使有些高级特权并不是 进程执行任务必需的。作为改进,可以引入更加细粒度的特 权控制,在特权提升时,只赋予执行任务所必需的高级特权, 而不是所有特权。 期望属性2的验证需要借助工具的分析。在Alloy Analyzer_12验证该断言,报告发现了反例。Alloy Analyzer生 成反例的图形,并允许用户指定图形的显示方式。 下面我们在Vista上实验该反例的是否存在。系统中有两 51 个用户zhao和zhao sT,分别属于Administrators组和Users 组。修改系统时间是一个涉及系统安全的操作,需要高级特 权sesystemtimePrivilege,默认配置下Users组甩户没有该 特权。在本地安全策略中配置Users组用户可以修改系统时 间,注销后使用zhao ST帐户登陆,查看该用户的shell进程 explorer.exe的令牌,拥有高级特权sesystemtimePrivilege。 在该帐户下修改系统时间,没有弹出任何提示和阻止,可以 顺利完成修改。 由此反例得到确认,UAC的确存在不足。分析原因,主 要在于用户登陆时,只是对管理员组用户进行高级特权过滤, 没有考虑到如果配置不当,标准用户组的用户也有可能拥有 高级特权,导致标准用户组的用户直接获得了高级特权。作 为改进,在登陆时,系统不应只关注用户是否属于管理员组, 而是无论属于那个组都直接过滤掉所有高级特权。这样做可 以避免用户不恰当的配置带来的不利影响。 4总结与展望 本文提出了一种针对非开源软件系统的反向建模分析方 法,并使用该方法对Vista UAC的特权控制机制进行了形式 化分析。我们采用Alloy语言对模型和断言进行形式化描述, 并使用自动化模型分析工具Alloy Analyzer对模型进行分析 和验证,发现了UAC的一些不足,并提出了改进建}义。 UAC除了对特权的控制,还包括对权限的控制,并且 与Vista系统的强制完整级控制(Mandatory Integrity Control, MIC)口1机制有紧密的联系。下一步我们将使用反向建模方法 把MIC与UAC结合起来进行形式化分析,发现可能存在的 不足。●(责编程斌) 参考文献: 【l】D.Jackson.Alloy:A Lightweight Object Modeling Notation[J1. Technical Report 797.MIT Lab for Computer Science,February 2000. 【212 Michael Howard and David LeBlanc[M].Writing Secure Code for Windows Vista.MicrosoR Press,20{)7. 13l Mark E.Russinovich,and David A.Solomon.Microso矗Windows InternaLs.Fourth Edition:MicrosoR Windows Server“2003,Windows xP.and Windows 2000[MI.Microso丘Press,2004. 【414 Technet.User Account Control Overview[OL】.http://technet. microsoft.com/en-us/windowsvista/aa906021.aspx. f5 I Mark Russinovich.PsExec,User Account Control and Security Boundaries[OLl.http://blogs.technet.com/markrussinovich/archive/ 2007/02/12/638372.aspx. 基金项目:国家“863”计划资助项目(2007AA012461) 作者简介:赵栋(1985一)。男,硕士研究生,主要研究方向:操作 系统和信息安全;罗军(1984一),男.研究员,硕士,主要研究方向: 操作系统和信息安全;王蕾(1977一),女,助理研究员,博士,主要 研究方向:操作系统安全、可信计算、计算机系统结构。 万方数据
展开阅读全文
  皮皮文库所有资源均是用户自行上传分享,仅供网友学习交流,未经上传用户书面授权,请勿作他用。
0条评论

还可以输入200字符

暂无评论,赶快抢占沙发吧。

关于本文
本文标题:windows vista用户帐户控制机制的反向建模分析.pdf
链接地址:http://www.ppdoc.com/p-10914335.html
关于我们 - 网站声明 - 网站地图 - 资源地图 - 友情链接 - 网站客服客服 - 联系我们

copyright@ 2008-2018 皮皮文库网站版权所有
经营许可证编号:京ICP备12026657号-3 

收起
展开