Chinese Journal of Computers   Full Text
Title	A New Property Verification Method for Code Security Based on Pointer Logic
Authors	ZHANG Yang1) CHENG Liang2)
Address	1)(Institute of Software, Chinese Academy of Sciences, Beijing 100190) 2)(Department of Electronic Engineering and Information Science, University of Science and Technology of China, Hefei 230027)
Year	2009
Issue	No.6(1119—1125)
Abstract &   Background	Abstract 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 approach 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. Keywords operating system security; formal verification; code analysis; model checking; pointer logic Background The work attributes to the project “Security Analysis of Windows Vista Kernel and Operating System Controllability Research”, which is supported by National High Technology Research and Development Program (863 Program) of China under grant Nos.2007AA01Z465, 2006AA01Z433, 2007AA01Z414. The code security property verification is an effective way to detect the vulnerability of operating system, which draws wide attention nowadays. Although current code security property verification tools can check various properties of a C program such as whether a certain point is reachable, or whether there exist race conditions in the program, the analysis difficulties brought in by the flexible pointer usage limits the scope of these tools’ application to the real world. In this paper, the authors propose an improved verification method for code security property inspired by the pointer logic. Firstly the program be traversed to be checked with the pointer logic, in order to obtain the equivalence classes of all the pointers. Then, the replacement algorithm is given to convert the pointers in the program to non-pointer type according to the information of the equivalence classes. Without the fuzziness introduced by pointers, the traditional code security property verification tools can do all their property check to the real world code thoroughly.