无线传感器网络中基于多移动代理的拓扑设计

提出了一种适用于无线传感器网络的基于多个移动代理的能量高效信息收集方案(cell with Multiple Mobile SinksMethod,CMMSM).通过一种基于分簇的无干扰拓扑分布设计,配合移动代理的使用,大大降低了MAC和路由协议的设计复杂程度.仿真结果证明了新方案的能量高效性,和满足不同时延要求的应用可扩展性.     

基于下推系统可达性分析的输出信道信息流检测

提出了一种对含输出信道的命令式语言进行信息流安全性分析的方法。将程序抽象为下推系统,通过自合成将不千涉性转化为安全性属性,将两次相关执行中向输出信道的输出操作分别抽象为由下推规则表示的存储和匹配操作,通过对标错状态的可达性分析验证程序是否满足终止不敏感不干涉性。演化后的方法支持程序的发散执行,通过上界回退算法找到强制终止首次执行所需的最大输出信道上界。实验说明该方法与现有工作相比具有更高的精确性和验证效率。     

State-oriented Noninterference for CCS

We address the question of typing noninterference (NI) in the calculus CCS, in such a way that Milner's translation into CCS of a standard parallel imperative language preserves both an existing NI property and the associated type system. Recently, Focardi, Rossi and Sabelfeld have shown that a variant of Milner's translation, restricted to the sequential fragment of the language, maps a time-sensitive NI property to that of Persistent Bisimulation-based Non Deducibility on Compositions (PBNDC) on CCS. However, since CCS was not equipped with a type system, the question of whether the translation preserves types could not be addressed. We extend Focardi, Rossi and Sabelfeld's result by showing that a slightly simpler variant of Milner's translation preserves a time-insensitive NI property on the full parallel language, by mapping it again to PBNDC. As a by-product, we formalise a folklore result, namely that Milner's translation preserves a behavioural equivalence on programs. We present a simple type system ensuring PBNDC on CCS, inspired by existing type systems for the π-calculus. Unfortunately, this type system as it stands is too restrictive to grant the expected type preservation result. We sketch a solution to overcome this problem.     

一种保持多等级安全策略细化后无干扰属性的方法

针对多等级架构细化中安全属性（即无干扰属性）保持的问题,提出一个细化函数和若干细化规则。通过细化函数将安全域分解为若干子安全域,通过若干细化规则限定子安全域与其他安全域以及子安全域间需要满足的关系。使用四个定理对细化后的架构或者策略进行形式化的描述和分析表明,细化后的架构或者策略仍然保持原架构或者策略的安全属性（即无干扰属性）。