Xinming's Research

Research Interests:

My thesis work is on formal analysis of network security. We model the security policies, the network configurations, and software vulnerabilities so that they can be used in formal reasoning. The goal is to automate the security management that nowadays is largely done manually and depends on human experience.

I have also done work in language-based security. Problems caused by the pervasive software vulnerabilities are posing more and more threats to every computer and information system throughout the Internet. I believe the adoption of safe programming principles is both necessary and effective to address this problem.

I am also interested in theorem proving and its application in program and system verification. I worked on the theorem prover Verifun during my internship in (DEC, Compaq) HP's Systems Research Center (2002), and worked on the theorem prover Zap during my internship in Microsoft Research (2004).

Research Papers:

1. MulVAL: A logic-based network security analyzer. Xinming Ou, Sudhakar Govindavajhala, and Andrew W. Appel. 14th USENIX Security Symposium, Baltimore, Maryland, August 2005.
2. A two-tier technique for supporting quantifiers in a lazily proof-explicating theorem prover. K. Rustan M. Leino, Madan Musuvathi, and Xinming Ou. In 11th International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS 05), Edinburgh, U.K., April 2005.
3. Network security management with high-level security policies. Xinming Ou, Sudhakar Govindavajhala, and Andrew Appel. Technical report TR-714-04, Computer Science Dept, Princeton University.
4. Dynamic typing with dependent types. Xinming Ou, Gang Tan, Yitzhak Mandelbaum, and David Walker. In 3rd IFIP International Conference on Theoretical Computer Science (TCS 04) , Toulouse, August 2004.
5. Theorem proving using lazy proof explication. Cormac Flanagan, Rajeev Joshi, Xinming Ou, and James B. Saxe. In 15th Computer-Aided Verification conference (CAV 2003), Boulder, CO, July 2003.
6. Enforcing resource usage protocols via scoped methods. Gang Tan, Xinming Ou, and David Walker. In 10th International Workshop on Foundations of Object-Oriented Languages (FOOL 10), New Orleans, LA, January 2003.

The documents contained in these pages are included to ensure timely dissemination of scholarly and technical work on a non-commercial basis. Copyright and all rights therein are maintained by the authors or by other copyright holders, notwithstanding that they have offered their works here electronically. It is understood that all persons copying this information will adhere to the terms and constraints invoked by each author's copyright. These works may not be reposted without the explicit permission of the copyright holder.