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

提出了一种检查代码安全的类型安全策略 ,详细描述了该策略的逻辑表示、形式化描述和基于该策略的证明方法 ,最后给出一个基于该策略的定理证明器HBTSTP 策略的核心思想是给每个合法的内存地址赋予类型 ,使用符号表达式记录内存的状态变化 ,对于需要读写内存的指令 ,调用证明器进行类型检查 。