Research

Ph.D. Theses

Practical Static Analysis Framework for Inference of Security-Related Program Properties

By Yin Liu
Advisor: Ana Milanova
February 17, 2010

A static analysis framework for inference of security-related program properties is presented in the thesis. Within this framework we infer ownership, immutability and information flow for the protection of object access, data confidentiality and integrity. We propose runtime models that capture these properties. We design and implement ownership, immutability and information flow inference analyses for Java. These analyses reveal information about object access and information flow in the program, and may help uncover serious vulnerabilities.

We have performed empirical investigation on a set of Java components, and a set of small-to-large Java programs. The results indicate that the analyses are practical and precise. Therefore, the analyses can be integrated in program comprehension tools that support effective reasoning about software security and software quality.

We have illustrated several applications of the framework to show the usage of the inferences. We illustrate the usage of ownership analysis on reasoning about shared objects in open concurrent Java programs. We identify three structural patterns for object sharing: we classify shared objects as central, owned or distributed. We argue that these patterns facilitate the understanding of concurrent programs. We perform experiments on several medium-to-large Java programs, which reveal the structure of sharing in real-world Java programs. We illustrate the usage of the static information flow analysis on three applications. The first application of information flow analysis is security violation detection. We perform experiments on a set of Java web applications and the experiments show that the information flow analysis effectively detects security violations. The second application is type inference. Our experiments on the Java web applications show that our flow analysis successfully infers security types. The last application studies the effect of thread-shared variables on thread-local variables. Our experiments on a set of multi-thread programs show that most of the thread-local variables are affected by the thread-shared variables.

Return to main PhD Theses page