| PCC中数组边界检查的优化和生成 |
| |
| 引用本文： | 胡荣贵,陈意云,郭帆,张昱. PCC中数组边界检查的优化和生成[J]. 小型微型计算机系统, 2003, 24(12): 2278-2282 |
| |
| 作者姓名： | 胡荣贵 陈意云 郭帆 张昱 |
| |
| 作者单位： | 中国科学技术大学,计算机科学与技术系,安徽,合肥,230026 |
| |
| 基金项目： | 国家自然科学基金 (60 1 730 4 9)资助 |
| |
| 摘 要： | PCC的数组边界检查存在着由于无法确定数组下标表达式符号值的范围，而造成拒绝执行一些安全的移动代码等问题。本文给出的一种数组边界检查的优化及生成算法，不仅能够比较好地解决了这一问题，同时还生成了循环不变式注解中的条件谓词。我们设计的编译器——认证编译器——已经实现了这些算法，并完成了从用C编程语言的类型安全子集编写的源程序到携带注解的Intelx86／linux汇编语言程序的编译过程。由于基于语言安全策略系统的证明是建立在携带注解的代码基础之上的，因此该认证编译器中实现的算法在移动代码安全检查中非常有用。
|
| 关 键 词： | PCC 数组边界检查 认证编译器 控制流图 注解 移动代码 语言安全策略系统 |
| 文章编号： | 1000-1220(2003)12-2278-05 |
Optimization and Creation for Array Bound Check in Proof Carrying Code |
| |
| HU Rong-gui,CHEN Yi-yun,GUO Fan,ZHANG Yu. Optimization and Creation for Array Bound Check in Proof Carrying Code[J]. Mini-micro Systems, 2003, 24(12): 2278-2282 |
| |
| Authors: | HU Rong-gui CHEN Yi-yun GUO Fan ZHANG Yu |
| |
| Abstract: | |
| |
| Keywords: | certifying compiler control flow graph proof-carrying code annotation optimization |
| 本文献已被 CNKI 维普 万方数据 等数据库收录！ |
