一种基于指针逻辑的代码安全属性分析方法

A New Property Verification Method for Code Security Based on Pointer Logic

在分析和总结前人工作的基础上,提出了一种改进的代码安全属性验证方法.该方法在利用传统的源代码安全属性验证工具的基础上,加入了指针逻辑,针对现有代码属性分析技术只能对C语言子集进行分析验证的不足,利用指针逻辑对源代码的分析结果对源代码中的指针进行替换,从而避开了传统静态代码属性验证工具对指针处理功能太弱的瓶颈,可以实现对C语言中的部分指针及运算进行处理.

This paper proposes an improved verification method for code security property on the basis of the study of predecessors＇ work. According to the situation that current code property verification can only deal with a subset of C programming language, this paper introduces the pointer logic, whose result can be used by the replacement algorithm to substitute all the pointers in the source code, to the conventional code security property verification tools. The proposed ap- proach avoids the weakness of pointer processing in the traditional static code property verification, and therefore can handle pointers in C programming language when property verification partially.