基于规则的安全策略定义语言

基于任务角色访问控制机制,提出类似一阶谓词逻辑的安全策略定义语言,并具有一定的时序表达功能。用户使用这种高层描述语-言可在不同的系统中定义各种特定应用的安全策略。还给出了基于扩展的稳定模型的语义描述,定义了安全策略正确性的条件以及验证方法,并进一步讨论实现安全策略的有关问题。

对机器语言进行检查保证移动代码安全

介绍了一种在安全策略语言的指导下，对机器语言进行安全检查的方法。它使用基于编程语言的理论和实现技术，通过分析程序语义和系统调用等特征，对程序进行检查。安全策略语言提供了一种灵活、统一的安全描述手段,希望这种将安全检查的实现机制和检查内容分离的做法能给其他的研究者提供了有用的参考。

PCC中数组边界检查的优化和生成

PCC的数组边界检查存在着由于无法确定数组下标表达式符号值的范围 ,而造成拒绝执行一些安全的移动代码等问题 .本文给出的一种数组边界检查的优化及生成算法 ,不仅能够比较好地解决了这一问题 ,同时还生成了循环不变式注解中的条件谓词 .我们设计的编译器———认证编译器———已经实现了这些算法 ,并完成了从用C编程语言的类型安全子集编写的源程序到携带注解的Intelx86 /linux汇编语言程序的编译过程 .由于基于语言安全策略系统的证明是建立在携带注解的代码基础之上的 ,因此该认证编译器中实现的算法在移动代码安全检查中非常有用 .