Analysis and implementation method of program to detect inappropriate information leak

For a program which handles secret information, it is very important to prevent inappropriate information leaks from a program with secret data. D.E. Denning (1976) proposed a mechanism to certify the security of program by statically analyzing information flow, and S. Kuninobu et al. (2000) proposed a more practical analysis framework including recursive procedure handling, although no implementation has been yet made. We propose a method of security analysis implementation, and show a security analysis tool implemented for a procedural language. We extend Kuninobu´s algorithm by devising various techniques for analysis of practical programs that have recursive calls and global variables. This method is validated by applying our tools to a simple credit card program, and we confirm that the validation of program security is very useful