基于广义痛点传播模型的安全级范围动态调整方法

基于广义痛点传播模型的安全级范围动态调整方法

计算机安全模型的主要目标是防止非法阅读或修改信息。控制信息的传播和间接污染。通常的访问控制模型（如rc和rbac）比前者更好地支持后者。然而，对于后者的目标不太了解。例如，rc和rbac策略可以表示用户可以读取用户b的数据，但不能有效表示b在a中传播数据的意图。为了有效实现最后一个目标，我们可以防止通常使用不可靠或有脆弱性的程序传播导致的信息泄漏和破坏系统完整性。此外，信息流模型还可以防止在系统中实体之间的信息流动，防止不允许使用的信息流。这已经是现代操作系统中最重要的安全模型之一。然而，传统的信息流模型（如经典的blp和biba模型）非常严格，需要唯一的信息流。大多数不可能形成可用的系统。现在，提高可用性的主要途径是动态适应安全级别，包括两种方法：一种是安全级范围方法。在安全级范围方法中,可信主体的当前安全级可在一个范围内动态变化,使得可信主体在不违背模型规则的情况下获得更多访问权限.这体现了弱静态原则.该方法的优点是实施简单,易于分析安全性.然而,主体的安全级函数是与系统状态无关的函数,在主体的生命周期内,主体的安全级范围不会发生变化,这意味着主体的权限保持不变.这并不符合最小权限原则还有一类方法借鉴了软件测试中的用于跟踪和分析输入数据在程序内部流向的污点传播机制基于以上分析,我们提出广义污点传播模型(generalizedtaintpropagationmodel,简称GTPM).模型的目标是为存在不可信应用程序的操作系统提供保密性和完整性保护.模型的基本思想是:定义实体的安全标记是由非等级的输入型和输出型类型标签组成的集合,实施对实体的动态隔离保护;引入主体能力概念,区分提高和降低安全级为两种不同能力,以有效表达主体发送和接受能力;进一步拓展污点传播语义.模型的特点是关闭污点传播方法中已知隐蔽通道,并且可有效防止污点积累.另外,形式化构建和分析抽象GTPM系统也是本文的一个主要工作.本文在分析相关工作的基础上,首先定义GTPM的相关概念,然后用CSP语言描述模型规格,最后,在定义可降密无干扰安全的基础上,分析抽象CTPM系统的无干扰性质.1广义规制问题的框架污点传播模型由于在主体权限最小化方面的特点,一直是信息流模型研究中的主要方向之一.不少研究偏重于污点传播机制的设计和实现,较少涉及污点传播控制和污点积累问题,也没有考虑隐蔽通道问题.例如:用于保密性保护的高水标模型High-Water-Mark一些研究通过分布式的降密和去污来缓解污点积累.IFEDAC模型在以上的这些污点传播模型中,一个非污点进程在收到另一个污点进程的信息时,系统会自动地将这个非污点进程调整为污点进程,这种标记调整机制存在一类共性的隐蔽通道问题.文献[5]给出了一个相应的隐蔽通道构造方案.考虑一个污点进程A试图传递1位敏感信息给一个未被污染的进程C.攻击者构建了两个未被污染的进程B随着计算机性能的提高,该隐蔽通道带宽会极大地增加.为了防止此类隐蔽通道,作为Asbestos系统的后继HiStar系统针对上述模型和系统的不足,本文提出广义污点传播模型.一方面仍然支持标记的隐式调整,保证模型的可用性;另一方面通过拓展污点传播语义来关闭上述提到的隐蔽通道,以保证模型的安全性.同时,通过主体删除标签来体现主体降密去污能力,防止污点积累.通过引入有约束的特定访问能力,以保证主体能力的有效性.本模型引入了类型标签和基于标签的主体能力等概念,早期的文献[15]给出类似的标签概念,但是它的每个标签表示系统内某个实体的标识,基于这些标签构建的标记难以表达实体的动态隔离,而且它的保护模型(如完整性保护)不支持污点传播.安全性上,我们的模型和先前污点传播模型的最主要的不同是,它不存在污点传播模型中已知的隐蔽通道.2基于gtp的操作系统信息流控制2.1特定访问能力s系统中所有被保护实体分为主体和客体两类,其中主体集合定义1(实体标记).集合Luf0cdDSuf0b4DI定义了系统中所有实体的所有可能标记.每个实体o的标记L标记在偏序关系上可形成一个格.需要指出的是,最高完整级是uf066(记作uf095定义2(能力).集合(37)uf0cdCuf0c8E定义了系统中所有可能的主体能力.其中:(1)Cuf0cd(DSuf0c8DI)uf0b4{+,-}定义了系统中的主体调整自身标记的所有可能的能力.对于主体s拥有的能力C(2)对于主体s和保密性标签d,若d我们用主体的有约束的特定访问能力是主体调整自身标记能力的补充.信息流保密性保护要求一个使用了升密能力的主体如果没有降密能力,将会失去对所有公开文件写的能力,但是有的应用场景会允许该主体写指定的公开文件.这一特定行为被认为是安全可信的,不会造成信息泄露,但不认为它写信息到其他所有公开文件是安全的(如果仍然被认为是安全的行为,可以通过赋予主体降密能力来解决).同样的,信息流完整性保护要求一个感染了污点的主体如果没有去污能力,将会失去对高完整级(无污点)信息的修改(写)的能力,但是有的应用场景会允许该主体修改指定的高完整级文件.这一特定行为被认为是安全可信的,不会造成完整性破坏,但不认为它修改其他所有高完整级文件是可信的(如果仍然被认为是安全的行为,可以通过赋予该主体去污能力来解决)针对这些情况,我们可以将那些指定的特殊访问需求看成是该主体的特定访问能力,可以不受严格的信息流保护约束.在有多个域时,需要指出在主体读了指定域的保密性信息或者感染了指定域的完整性污点后,不能再使用这些能力,即不将主体在任何标记状态下的特定访问都看成安全可信,以对主体使用该能力进行约束,防止主体滥用该特定能力.如果约束为空,则主体可以在任何标记状态下使用该能力.对于主体s以权限op访问实体o,引入一个判断该主体是否具有相应特定访问能力的谓词CEP(s,o,op).当且仅当存在一个(S主体能力取自产生该主体的可执行客体属性,由授权管理员设置和管理,在主体创建时由系统读取和载入.第1节提到的隐蔽通道的原因是系统会隐式地改变B定义3(安全的信息流动和标记隐式变化).实体p以权限op如果条件(a)满足,在消息流动后,q的标记被污染,从而发生标记的隐式变化,即定义3规定的安全的信息流动有两种情况:一是同时考虑信息流出方发送能力和信息流入方接受能力情况下,低保密级的信息向高保密级流动,高完整级的信息向低完整级流动,并实施污点传播.从便于实际应用考虑,这里规定信息流出方p的标记不发生隐式变化,为此涉及到p的能力是C(i)主体p可从主体q接收到消息,当且仅当条件(a)、条件(b)、条件(d)同时满足,或者条件(a)、条件(c)、条件(d)同时满足:(a)q存在;(c)CEP(p,q,ipcrecv);(d)q已发消息给p.若p做出从q接收消息的动作(系统调用),则p的标记调整如下:uf0b7如果条件(a)、条件(b)满足,则p的标记被污染(调整)为Suf0b7如果条件(a)不满足或条件(b)不满足,则p的标记被调整为S(ii)主体p可读或动态加载客体q,当且仅当条件(a)、条件(b)同时满足,或者条件(a)、条件(c)同时满足:(a)q存在;若p做出读或动态加载q的动作(系统调用),则p的标记调整如下:uf0b7如果条件(a)、条件(b)满足,则p的标记被污染为Suf0b7如果条件(a)不满足或条件(b)不满足,则p的标记被调整为S(iii)主体p可写客体q,当且仅当条件(a)、条件(b)同时满足,或者条件(a)、条件(c)同时满足:(a)q存在;(iv)主体p可创建标记为(S(a)q不存在;(v)主体p可删除客体q,当且仅当下面的条件成立:(a)q存在;(vi)若主体p可执行客体o,创建主体(进程)q,当且仅当条件(a)、条件(b)、条件(c)同时满足,或者条件(a)、条件(d)同时满足:(a)o存在;(d)CEP(p,o,exec)(其中,新主体q的能力取自客体o的属性).若p做出执行客体o的动作(系统调用),则p的标记调整如下:uf0b7如果条件(a)、条件(b)满足,则p的标记被污染为S·如果条件(a)不满足或条件(b)不满足,则p的标记被调整为创建q后,如果条件(a)、条件(b)、条件(c)满足,q的标记设置为该执行过程可以看做p读访问o和p写访问q两个过程:前一过程中,p至少可以知道o是否存在的信息;后一过程中,如果p带参数启动q,则q直接读到p发来的参数信息,即使不带参数执行,如果只有p才会启动q,则启动本身就是q获得的来自p的信息.删除主体通过该主体接受其他主体要求退出消息(情况(i))后主动退出完成.或由系统强制删除该主体,客体重命名,客体复制、移动可以通过创建、读、写和删除客体操作并遵循相应的安全要求来实施.定义4(安全的标记显式变化).X是主体s的保密性或完整性标记,Xuf0a2是s请求的关于X的新值,从X到Xuf0a2的显式变化是安全的,当且仅当Xuf0a2-Xuf0cdC相应地,X是主体s的保密性或完整性标记,Y是客体o的与X同类型的标记,Yuf0a2是s请求的关于o的标记Y的新标记,从Y到Yuf0a2的显式变化是安全的,当且仅当X-C主体可以在能力范围内主动改变自己的标记,如文字处理进程主动提高密级以产生第1份机密文档;PGP软件主动降密(如果PGP没有升密能力)以发送文档密文.结合主体标记的显式变化,安全信息流动条件放宽为主体可以修改客体标记的要求是与定义3一致的,可通过s读o内容uf0aes将内容写到临时文件uf0aes删除ouf0aes创建标记为Yuf0a2的ouf0aes读临时文件uf0aes写ouf0aes删除临时文件完成,给出客体标记改变要求是为了简化系统处理.基于上述定义,下一节给出模型的确切语义.2.2gtpm的组成GTPM形式化规格(specification)试图通过数学符号对模型实现系统的性质及行为进行精确、简洁的描述这种确切描述反映了模型的精确要求,可以消除实现语义上的二义性,同时也是进行形式化验证(verification)和安全性分析的基础.本文采用通信顺序进程CSP图1描述了GTPM实现系统的组成原理,引用监视器(referencemonitor,简称RM)依据授权策略控制主体对被保护实体的访问行为,限制非授权访问;安全服务器(SecServer)根据主客体标记以及访问动作做出决策;标记状态管理器(labelstatemanager,简称LSM)存储和维护系统实体的标记状态信息以及实体能力等信息.这3个组件构成系统安全核.安全核应该足够小,以保证效率和利于进行安全性分析和测试.主客体是系统的受保护对象.每个主体i通过信道api2.2.1csp下的csp执行在常见的操作系统中,用户进程通过系统调用访问系统资源和服务,如进程通信、读或写文件等,不直接交互的用户进程间的并发执行用混合算子描述.用CSP进程USER其中,P是系统中可能的主体标识符PID的集合;USER_LIVEUSER部分系统调用没有返回结果(如写、执行客体等),是因为调用结果也是一种信息,可能导致隐蔽通道.为了提高可用性,同时不违背模型安全性要求,安全核可以将每次用户进程的系统调用结果发送给一个安全调用结果查询服务进程USER2.2.2改变主客体标记RM并发处理来自不同用户进程的系统调用,它用子进程RM_ITEM进程RM_ITEMRM_ITEM进程SYN_SO通过锁机制和CSP的并发机制实现对同一主客体标记状态信息的互斥访问.一个系统调用涉及到两个以上主客体时,加锁优先顺序定为标识号从小到大的客体,然后是标识号从小到大的主体,以防止死锁.进程SYN_SO的事件集aSYN={enterS,leaveS,enterO,leaveO}.其中:uf0b7主体同步进程SYN_S=|||i:P@SYN_Suf0b7客体同步进程SYN_O=|||i:O@SYN_O识集合.进程BUFF缓存和中转进程间通信信息,为简单起见,这里为每对通信进程设置一个消息槽.消息槽提供放入/取出消息服务,消息还未取出时,再次写入新消息,旧消息被覆盖.由于主体的标记会动态变化,消息槽同时还会记录发送者发送消息时的标记信息.消息槽状态变迁如下:当USER当USER当USER主体退出时,除了通知系统更新标记状态信息外,还要清空该主体的发送缓冲区.改变主客体标记主要是通知系统更新标记状态信息.2.2.3主体退出时的运作SecServer进程也是并发处理来自RM各个子进程的请求,其子进程SS_ITEMSecServer=(|||i:P@SS_ITEM其中,子进程CEP进程通信的控制点在接收方发出接受请求后,SS_SEND进程SS_EXEC读、写、创建和删除客体以及改变标记的决策过程与以上两个类似,创建客体时,客体以后执行该客体产生的新主体的能力由管理员设置客体属性来实现,这里通过信道nonceCE随机设置来模拟.主体退出时,需要更新LSM中标记信息和可用主体标识符集合.2.2.4程lsmsc软件设计LSM进程维护着主体和客体的标记信息、能力信息和存在信息,子进程LSM_S_LIVE进程LSM_S则是所有LSM_S_LIVE类似地,子进程LSM_O_LIVE进程LSM_O是所有LSM_O_LIVE进程LSM_ID_MGRLSM的行为可描述如下:2.2.5系统外在行为及其机制基于以上组件,安全核可以被描述为RM,SecServer和LSM的并发:由于整个系统是安全核和用户进程的并发,系统外在行为可以描述为其中,aKERNEL={intercom,intermgr,buff,nonce,cep}uf0c8aSYN.这里用到了屏蔽算子,SYSTEM3基于gtpm的非干扰分析本节将分析SYSTEM3.1进程等价模型定义5(基本的无干扰).给定一个CSP进程SYS,其事件集aSYS=aHIGHuf0c8aLOW,且aHIGHuf0c7aLOW=uf066,SYS是基本的无干扰安全当且仅当基本的无干扰要求禁止high事件发生的系统和原系统之间在分别屏蔽所有high事件后是进程等价的关系.CSP主要有3个进程等价验证模型,依次是:迹模型(tracemodel)、稳定失败模型stablefailuresmodel和失败/发散模型(failures/divergencesmodel).其中:迹模型根据两个CSP进程的迹集合是否相同来判断它们是否等价稳定失败模型根据两个CSP进程的迹集合和失败集是否分别相同来判断它们是否等价;失败/发散模型根据两个CSP进程的迹集合、失败集和发散迹是否分别相同来判断它们是否等价.3个模型验证进程间等价性的程度和需要验证的状态空间个数都是递增的.迹模型可以验证安全性质分析SYSTEM根据模型要求,可能引发状态变化的系统调用有api其他子进程不需要更新状态,以SEND规格调整后的SYSTEM基于事件的标记信息,定义6对SYS定义6(high事件和low事件).在CSP进程SYS3.2保密性保护的非前置性基本的无干扰安全严格限制high事件干扰low进程,这可能没有反映出实际的安全需求.很多信息流模型允许有条件地从high进程到low进程的信息流动,但是需要对其管理,如通过可信中介完成或至少进行审计.在GTPM模型中,这些信息流动需要流经降密器(declassifer)以进行降密处理,降密器是有删除保密标签能力的主体或者是在指定状态下有特定访问能力的主体.降密器的行为可看做降密处理,这使得GTPM不满足定义5.需要给出一种合理的无干扰安全定义,它允许Declassifer和low进程影响所有其他进程;同时,允许high进程影响其他high进程和Declassifers,但是不允许high进程影响low进程.这是一种不传递的无干扰(intransitivenoninterference)定义7(可降密的无干扰).给定一个CSP进程SYS,其事件集aSYS=aHIGHuf0c8aLOW,aHIGHuf0c7aLOW=uf0c6aMIDuf0cdaSYS,SYS是可降密的无干扰安全当且仅当可降密的无干扰要求禁止aHIGH-aMID中事件发生的系统SYSuf0a2和原系统之间在分别屏蔽所有aHIGHuf0c8aMID事件后等价.也就是说,要求aMID事件集对low进程的影响与aMIDuf0c8aHIGH事件集对low进程的影响相同,使得low进程无法推测降密器以外的high进程做了什么,high不能试图通过降密器干扰low进程.如果aMID={uf0d7},定义7与定义5相同,此时不允许降密器存在.分析SYS定义8(mid事件).在CSP进程SYS定义8允许aMID和aHIGH(或aLOW)之间存在交集,其实,aMID包括降密器处于high状态和low状态下的所有行为事件集,这里面存在非降密事件,如降密器发信息给high进程和从low进程读信息等.不过在SYS定理1.对于任意保密性标签d,SYS证明:根据定义7和定义8,即证以下等式成立:在SYS在SYS在SYS在SYS所以,如果我们能够证明在|P|=8,|O|=8而且初始时有一个状态为({uf0d7},{t对于|p|=5,|O|=5,初始时有一个状态为({×},{t验证过程在环境tool/FDR2.83,OS/Ubuntu9.10,CPU/P42.8GHz,RAM/2GB下进行,验证结果是断言为真,验证执行时间大约是1680s.基于上述分析和自动化验证结果,得知对于任意保密性标签d,SYS以上分析了保密性保护中的无干扰,对于任意完整性标签d,我们完全可以定义类似的完整性无干扰安全,同时将high事件定义标记包含完整性标签d的事件,将low事件定义为不包含d的事件,将污点程序看做high主体,非污点程序看做low主体,并采用相似的方法证明污点程序不能干扰非污点程序,从而不能影响非污点程序的完整性.需要强调的是,由于我们的规格是在较高的层次上给出的,没有捕获低层次实现细节,如CPU、Cache、内存、硬盘和网络等行为,因此证明的结论难以反证不存在模型化这些硬件实现细节的隐蔽通道,实现时遵守这些规格,系统只是有了获得无干扰安全性质的基础和可能,下一步需要继续细节化规格,以使验证结果反映更加实际的系统的性质.4基于ds的即时通信软件在本节中,我们通过一个典型的应用示例来分析说明GTPM在可用性方面比传统的信息流模型有明显的提高.(1)系统环境图2描述了一个较常见的桌面系统组成,其中:IM是用户的即时通信软件,如各种聊天工具.IM会将可能涉及用户隐私的信息放到IMdata中;Office是一套办公软件,用户用它来处理办公文档Officefiles,其中部分文档涉及公司秘密;PGP是一款可以提供邮件加密功能的安全电子邮件软件,用户用它与自己的公司同事进行安全的办公文件传输;NortonAntivirus是一款杀毒软件,通过杀毒,可以有效、及时地清除系统中的病毒和木马程序,但是它需要定时更新病毒库;OSUpdatedpackages是用户从网上下载的系统更新安装包,用于操作系统更新;Explorer是操作系统与用户之间的交互接口程序;Firefox是一款户用来访问万维网的浏览器.另外,用Downloaddata表示Firefox在网络通信时下载的临时文件;OSconfigfiles存储了操作系统运行所需的重要配置信息.(2)安全需求(1)IM软件不能窃取秘密的Officefiles,也不能破坏officefiles和OSconfigfiles的完整性.这是考虑到有些即时通信软件不可信或者因有漏洞而存在被利用可能,从而变成间谍或病毒程序;也不允许Office软件窃取IM的数据,但允许IM的网络通信.(2)NortonAntivirus可以检测检测IMdata,Officefiles这些包含个人隐私或商业秘密的数据中是否含有病毒,但是不能泄露这些信息到网络.即使NortonAntivirus不可信或有漏洞也不能泄露这些信息,但是允许它在线的病毒库更新.(3)秘密的办公文档Officefiles可通过PGP软件加密后发送出去,PGP收到网上发来的邮件经过杀毒后可被Officeprocess读取.(4)允许Explorer修改OSconfigfile,但是当Explorer加载了从网上下载的Downloaddata时,应禁止Explorerprocess修改OSconfigfile.这是由于如果Explorer或者浏览器存在漏洞,导致Exlprer动态加载不可信的动态链接库,则存在系统被劫持的可能.这也是比较常见的一种网络攻击方式.(5)从网上下载的OSUpdatedpackages需经过查毒,确保无病毒后才能允许其运行时修改OSconfigfile从而成功的更新操作系统.(3)已有其他主要模型的可用性分析(i)安全级范围模型该模型目前未发现隐蔽通道,它是BLP模型的改进.在该模型中,主体的当前安全级是一个二元组(uf061-minv-max),用L安全需求(2)允许NortonAntivirus读秘密文档、读/写非秘密文档和网络,但是当它读取秘密文档后,系统应该立刻回收该进程对非秘密文档和网络的写权限.以后所有该进程写操作的对象都应该升级到秘密类型,当进程重新启动(reinitialized)后,可恢复其对非秘密文档和网络的写权限,这是一种要求随着主体访问历史变化而调整主体权限的策略.安全级范围方法要么允许NortonAntivirus读秘密文档,要么不允许NortonAntivirus读秘密文档,它难以表达安全需求(2)要求的策略,该策略从某种程度上体现了保密性最小权限原则.安全需求(4)允许Explorerprocess修改OSconfigfile,但是当它动态加载从网上下载的低可信度的动态库或组件时,系统应该立刻回收Explorerprocess对OSconfigfile的修改权限.这种对主体权限随历史访问而变化的要求,也是安全级范围模型无法用策略表达的.该需求要求的策略从某种程度上体现了完整性最小权限原则.安全需求(2)解决不好,存在秘密泄露或者无法正常杀毒的问题;安全需求(4)解决不好,存在无法访问万维网或者系统感染病毒的问题.而安全级范围方法不能制定出有效的策略来满足这些安全需求.(ii)Histar/Flume系统已有的未发现隐蔽通道的Histar或Flume系统由于可以表达主体的实际权限变化的策略,可满足以上安全需求.由于篇幅的关系,我们只分析它们在可用性方面存在的不足.由于Histar或Flume系统均不是污点传播模型,不支持标记的隐式调整,需要主体自己主动地调整自己的标记,这会导致以下不足:(a)由于进程的标记调整包括各种升级和降级可能,而且为了防止隐蔽通道,进程不能获得通信对方或者访问客体的标记信息,进程自己未必能做出及时和正确选择,最终可能还是需要系统的使用者完成.这意味着用户在系统的使用过程中需要经常地手动调整主体的标记,这不仅让用户体验不好,而且也需要用户有相关的专业知识才行;(b)每个应用程序需要增加标记调整功能,这需要改动程序和应用软件厂商的合作,操作起来有难度;(c)显示标记调整需要系统调