基于类型化内存地址的安全策略的设计与实现  

Design and Implementation of a Safety Policy Based on Typed Memory Address

作　　者：郭帆[1] 陈意云[1] 胡荣贵[1] 

机构地区：[1]中国科学技术大学计算机科学与技术系,合肥230026

出　　处：《计算机研究与发展》2003年第7期1001-1007,共7页Journal of Computer Research and Development

基　　金：国家自然科学基金 ( 60 173 0 49)

摘　　要：提出了一种检查代码安全的类型安全策略 ,详细描述了该策略的逻辑表示、形式化描述和基于该策略的证明方法 ,最后给出一个基于该策略的定理证明器HBTSTP 策略的核心思想是给每个合法的内存地址赋予类型 ,使用符号表达式记录内存的状态变化 ,对于需要读写内存的指令 ,调用证明器进行类型检查 。In this paper, a kind of type safety policy is introduced, which is used to assure code safety The logic representation, formal description, and proof method of the policy are discussed in detail A and theorem prover HBTSTP based on the policy is also presented at the end of the paper The core idea of the policy is that any valid memory address has an attached type, and a symbol expression is used to trace the change of the whole memory state For instructions that need to read or write memory, HBTSTP is called to check whether the destination is type safe if it is type safe, then the read or write operation is memory safe

关 键 词：类型安全策略 证明方法 类型检查 代码安全 逻辑表示 形式化描述 

分 类 号：TP311[自动化与计算机技术—计算机软件与理论]