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

摘要

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