CS 6V81-002: Seminar on Language-based Security

Course Information

Title: CS 6V81-002: Language-based Security
Course Registration Number: 13926
Times: MW 4:00-5:15
Location: ECSS 2.306
Instructor: Dr. Kevin Hamlen (hamlen AT utdallas)
Office Hours: ECSS 3.704, Wed 2:00-4:00

Course Summary

This course will introduce and survey the emerging field of "Language-based Security", in which techniques from compilers and programming language theory are leveraged to address issues in computer security. Topics include:

1. Proof-Carrying Code
2. In-lined Reference Monitoring
3. Typed Intermediate Languages
4. Typed Assembly Language
5. Certifying Compilers
6. Software Fault Isolation

The aim of the course is to allow each student to develop a solid understanding of at least one of these topics, along with a more general familiarity with the range of research in the field. In-course discussion will highlight opportunities for cutting-edge research in each area. If your research involves computer security, this course will provide you with an array of powerful tools for addressing software security issues. If your research involves programming languages and compilers, this course will show you how to take techniques that you might already know and apply them in new and interesting ways.

The course is open to Ph.D. students and Masters students. Undergraduates may enroll with permission of instructor.

Suggested prerequisite: CS 6371 Advanced Programming Languages (or concurrently), or a basic familiarity with type theory. (If not, the student is advised to consult one of the texts on type theory listed later on this page.)

Grading

Homework: Homeworks will consist of assigned readings—usually one required paper and one optional additional paper per class session. Material presented in class will assume that students have read the assigned material before coming to class, so please do the readings ahead of time!

Quizzes (25%): To encourage students to read the assigned material in advance, there will be a very short quiz at the beginning of most classes designed to test whether you have completed the required reading(s) for the day. Quizzes will typically consist of about five multiple-choice questions or short-answer questions. Each student's lowest two quiz scores will be dropped, and his/her quiz grade will be the average of the remaining scores. A missed quiz is a 0, but students are free to make up any quiz as long as the solutions have not yet been posted and the student was not present for the in-class lecture (which typically reveals the quiz answers).

Presentations (25%): Each student will be assigned 1-2 days during the semester during which they will present to the class a summary of the readings for that day. The presentation should provide a technical overview of the paper, a description of how the paper fits into the broader context of the material covered in the course, and should pose some interesting questions or challenges for in-class discussion.

Class Participation (10%): Students are expected to come to each class having read the assigned papers, and prepared with questions, critiques, and discussion topics. Regular participation in in-class discussion will count 10% towards students' grades in the course.

Projects (40%): Students taking the course for a letter grade will work individually or in a team of two to four to complete a course-related project. All project ideas are individually approved by the instructor. Proposals are due by mid-semester. A typical project would involve implementing one of the concepts described in one of the assigned readings, or using one or more of the research-level software packages covered in class to do an interesting program analysis or to address a non-trivial security vulnerability. Some overlap of class project with the student's docteral or masters thesis research is both permitted and encouraged.

Texts

The course has no required textbook, but several of the course topics will draw heavily from material in:

• Benjamin C. Pierce, ed., Advanced Topics in Types and Programming Languages. MIT Press, Cambridge, MA, 2005. (available online from UTD computers)

The following are also useful references for those not already familiar with type theory and/or security:

• Benjamin C. Pierce. Types and Programming Languages. MIT Press, Cambridge, MA, 2002.
• Glynn Winskel. The Formal Semantics of Programming Languages. MIT Press, Cambridge, MA, 1993.
• Matt Bishop. Computer Security: Art and Science. Addison-Wesley, 2003. (available online from UTD computers)

Tentative Course Schedule