Instructor Trent Jaeger (tjaeger 'at' cse.psu.edu)
Location 223B IST
Meeting Times M 2:00pm-4:50pm
Credits 3
Office Hours Prof. Jaeger: by appointment


In this course, we study the latest research in methods to verify security properties in programs, security policies, and systems at large. While formal verification has long been a focus in the security community, commodity systems have been too complex for such verification methods to be applied in practice. Nonetheless, in the last ten years a variety of advances in both verification methods as well as innovative applications have been made to detect security problems and verify security properties in commodity systems. The course aims to provide foundations of verification methods, examine specific methods used to address specific challenges, and explore how to leverage such methods in the future to analyze security in large scale systems.

Topics will include vulnerabilities in ordinary systems, basic security principles, static analysis foundations, analysis for bug finding in programs, security policy analysis, analyses for specific types of security problems, and specialized static analysis techniques applicable to such problems. We will work from a short book on analysis techniques for security, and augment the text with research papers, some classical and some recent. There will also be two programming projects to explore the technological issues in the context of the program and security policy analysis.

A detailed list of a lecture by lecture contents, assignments, and due dates (subject to change as semester evolves) is available on the course calendar.


The course will be graded on presentations, participation, and a final project in the following proportions:

40% Course Project
10% Reviews
40% Midterm and Final
10% Class Participation

Course Projects

There will be two course projects, one focusing on program analysis and one focusing on security policy analysis.


You will be expected to write reviews for some (about ten) of the assigned papers during the semester.

Class Participation

Class participation focuses on the readings assigned for the class. During the lecture, we will discuss the readings, and students are required to participate in discussions during each lecture. It is strongly suggested that students do the reading prior to this class. Ultimately, the students' ability to exhibit comprehension of readings is essential to a good grade.

Lateness Policy

All milestones are assesed a 20% per-day late penalty, up to a maximum of 4 days. Unless the problem is apocalyptic, don't give me excuses. Students with legitmate reasons who contact the professor before the deadline may apply for an extension.

Required Texts

The course will consist of readings assigned papers and the text below. The specific papers will be posted on the course calendar.

Academic Integrity Policy

Students are required to follow the university guidelines on academic conduct at all times. Students failing to meet these standards will automatically receive a 'F' grade for the course. The instructor carefully monitors for instances of offenses such as plagiarism and illegal collaboration, so it is very important that students use their best possible judgement in meeting this policy. The instructor will not entertain any discussion on the discovery of an offense, and will assign the 'F' grade and refer the student to the appropriate University bodies for possible further action.

Note that students are explicitly forbidden to copy anything off the Internet (e.g., source code, text) for the purposes of completing an assignment or the final project. Also, students are forbidden from discussing or collaborating on any assignment except were explicitly allowed in writing by the instructor.

Ethics Statement

This course considers topics involving personal and public privacy and security. As part of this investigation we will cover technologies whose abuse may infringe on the rights of others. As an instructor, I rely on the ethical use of these technologies. Unethical use may include circumvention of existing security or privacy measurements for any purpose, or the dissemination, promotion, or exploitation of vulnerabilities of these services. Exceptions to these guidelines may occur in the process of reporting vulnerabilities through public and authoritative channels. Any activity outside the letter or spirit of these guidelines will be reported to the proper authorities and may result in dismissal from the class.

When in doubt, please contact the instructor for advice. Do not undertake any action which could be perceived as technology misuse anywhere and/or under any circumstances unless you have received explicit permission from Professor Jaeger.

Course Updates