We will select appropriate principles of good coding practice for open source software, with the goal of detecting certain classes of common security flaws. We will express these principles as properties in a temporal logic that can be model-checked effectively. A report explaining the selection will be provided. In parallel, we will develop model-checking tools. These tools will be capable of analyzing open source software to check whether it satisfies properties specified in a temporal logic. A report describing the design and evaluation of our initial prototype of a model-checking tool will be provided. Then, we will apply these tools to large open source software packages and enhance the tools as required to improve their practical usefulness. The results of our automated security analysis will be provided, and we will describe any security flaws that we find in open source packages by using our tools. A final report on the project will be provided.