论文部分内容阅读
现代计算机系统和网络环境中,由于访问控制等安全措施的实施,进程的行为受到各种条件制约,一方面要遵循一定的访问控制策略,如访问一个对象时必须拥有一定的安全级别、权限、角色或者先完成一定的任务才能进行某些动作等,另一方面还要受到运行环境的约束,例如硬件控制或者IP地址的绑定等。论文基于访问控制资源的概念统一描述安全级别、权限、角色或者运行环境等访问控制中的基本概念,将基于这些概念的访问控制描述成如下计算现象:进程必须拥有一定的访问控制资源,并且进程运行过程中要使用和消耗这些资源才能完成动作。为了刻画和研究这种计算现象,论文提出了一种刻画资源使用和消耗的演算系统RUCCS(Resources Usage and Consumption Calculus System),给出了RUCCS的语法和语义,并对其行为理论、逻辑特征以及应用进行了研究。论文的主要研究内容包括:1)提出了访问控制资源概念,使得现有的访问控制模型在此概念下得到统一。研究了在并发和分布式环境中以及实施了访问控制等安全策略下进程运行的特点,把访问控制中使用的安全级别、权限、角色和进程运行环境等抽象为进程的资源,使得访问控制在这个特殊的资源概念下得到统一,即不同的访问控制技术就是使用不同的资源实施访问裁定的策略。2)提出了一个基于资源使用和消耗的演算系统,用以研究并发环境中的访问控制理论。从并发理论出发,为进程演化中需要使用和消耗资源这种计算现象建模,提出了带资源使用和消耗的演算系统RUCCS,给出了其语法、归约语义和结构化操作语义,证明了这两种语义间的协调性定理。围绕资源的使用和消耗,相对于经典进程代数CCS,RUCCS有三个方面的重要变化:(1)进程动作前增加了动作执行所需要满足的资源条件布尔表达式;(2)引入了资源环境的概念,用以刻画和记录进程资源的动态变化情况,具体而言,它包含了进程拥有和消耗资源的相关信息;(3)引入了进程标识符机制,进程标识符承担资源分配者角色,而进程则是动作执行者。这三个方面的扩展使得RUCCS具有更好的表达能力,但也增加了系统的复杂性。3)提出了基于观测能力集合的观测互模拟概念,并对其基本性质进行了研究。研究了RUCCS的行为理论,除了用系统的强互模拟来研究系统间的行为等价外,还从资源的拥有、使用和消耗出发,指出拥有资源的状况决定了一个系统与另外一个系统之间的交互能力,亦即观测能力,为此提出了基于观测能力集合的观测互模拟概念,包括强和弱两种形式,并研究了其基本性质。4)基于Hennessy-Milner逻辑,研究了RUCCS的逻辑特征,建立了系统间行为等价与逻辑等价之间的内在联系,使得既可以从行为等价上研究访问控制系统的行为特征,也可以用逻辑系统刻画访问控制系统满足的性质。5)基于RUCCS建立了一个统一的访问控制理论框架,通过对资源的例化可以完成目前访问控制模型规范描述,表明RUCCS具有很强的表达能力。6)采用RUCCS研究了几个典型的进程代数系统,包括:通信距离受限的进程代数、考虑成本的进程代数以及安全进程代数,这进一步说明RUCCS不但具有丰富的表达能力,而且还有很大的适用范围。