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:

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

Tentative Course Schedule

Date Topic Presenter(s)
Introduction and Review
Mon 1/7 Course overview and introduction to Language-based Security
Instructor [slides]
Wed 1/9 Introduction: Verification Conditions
Instructor [slides]
Mon 1/14 Introduction: Type-theory
  • Quiz 1 on: Fred B. Schneider, Greg Morrisett, Robert Harper. A language-based approach to security. Informatics: 10 Years Back, 10 Years Ahead, Lecture Notes in Computer Science, Vol. 2000, Springer-Verlag, Heidelberg, 86-101.
  • Supplemental (non-mandatory) reading: Benjamin C. Pierce. Types and Programming Languages: Chapters 23 and 24. MIT Press, Cambridge, MA, 2002.
  • Supplemental (non-mandatory) reading: Glynn Winskel. The Formal Semantics of Programming Languages: Chapters 2,6. MIT Press, Cambridge, MA, 1993.
Instructor [slides]
[quiz 1 solutions]
Wed 1/16 Introduction: Computer Security
Instructor [slides]
Mon 1/21 Martin Luther King Day N/A
Memory Safety and Control-Flow Safety
Wed 1/23 Software Fault Isolation
Moore [slides]
[quiz 2 solutions]
Mon 1/28 SFI for CISC
Wartell [slides]
[quiz 3 solutions]
Wed 1/30 Control Flow Integrity
  • Quiz 4 on: Martín Abadi, Mihai Budiu, Úlfar Erlingsson, Jay Ligatti. Control-Flow Integrity: Principles, Implementations, and Applications. ACM Conference on Computer and Communication Security, Alexandria, VA, November 2005.
  • Supplemental (non-mandatory) reading: Úlfar Erlingsson, Martín Abadi, Michael Vrable, Mihai Budiu, and George C. Necula. XFI: Software Guards for System Address Spaces. In Proceedings of the 7th International Symposium on Operating Systems Design and Implementation (OSDI'06), Seattle, Washington, November 2006.
  • Supplemental (non-mandatory) reading: Martín Abadi, Mihai Budiu, Úlfar Erlingsson, and Jay Ligatti. A Theory of Secure Control-Flow. International Conference on Formal Engineering Methods, Manchester, UK, November 2005.
Cooke [slides]
[quiz 4 solutions]
Minimizing the Trusted Computing Base
Mon 2/4 Proof-Carrying Code
Instructor [slides]
Wed 2/6 Proof-Carrying Code
  • Quiz 5 on: George C. Necula and Peter Lee. Safe Kernel Extensions Without Run-time Checking. In Proceedings of the 2nd Symposium on Operating Systems Design and Implementation (OSDI'96), Seattle, Washington, October 1996.
  • Supplemental (non-mandatory) reading: George Necula. Proof-Carrying Code. In Proceedings of the 24th Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL'97), Paris, France, January 1997.
  • Additional Reference Material: George C. Necula and Peter Lee. Proof-Carrying Code. Technical Report CMU-CS-96-165, Carnegie Mellon University, Pittsburgh, Pennsylvania, November 1996.
  • See also: George Necula's PCC Page
DeVries [slides]
[quiz 5 solutions]
Mon 2/11 Typed Assembly Language Instructor [slides]
Wed 2/13 Dependently Typed Assembly Language
  • Quiz 6 on: David Aspinall and Martin Hofmann. Dependent Types. In Benjamin C. Pierce, ed., Advanced Topics in Types and Programming Languages: Chapter 2.1, pp. 45-47 (up to exercise 2.1.1), MIT Press, Cambridge, MA, 2005. (available online from UTD computers)
  • Quiz 6 on Section 1 of: Hongwei Xi and Robert Harper. A Dependently Typed Assembly Language. In Proceedings of the International Conference on Functional Programming (ICFP'01), Florence, Italy, September 2001.
Desautels [slides]
[quiz 6 solutions]
Securing Legacy Code
Mon 2/18 Cyclone: A TAL-Targeting, C-like Language
  • Quiz 7 on: Trevor Jim, Greg Morrisett, Dan Grossman, Michael Hicks, James Cheney, and Yanling Wang. Cyclone: A Safe Dialect of C. In Proceedings of the USENIX Annual Technical Conference, Monterey, CA, June 2002.
  • Supplemental (non-mandatory) reading: Michael Hicks, Greg Morrisett, Dan Grossman, and Trevor Jim. Experience with Safe Manual Memory-management in Cyclone. In Proceedings of the 4th International Symposium on Memory Management, Vancouver, BC, 2004.
Marple [slides, handout]
[quiz 7 solutions]
Wed 2/20 CCured: A PCC-Targeting, C-like Language
  • Quiz 8 on: George C. Necula, Scott McPeak, Westley Weimer. CCured: Type-Safe Retrofitting of Legacy Code. In Proceedings of the 29th ACM Symposium on Principles of Programming Languages (POPL'02). Portland, OR, 2002.
  • Supplemental (non-mandatory) reading: Jeremy Condit, Matthew Harren, Scott McPeak, George C. Necula, Westley Weimer. CCured in the Real World. In Proceedings of the ACM Conference on Programming Language Design and Implementation (PLDI'03), San Diego, CA, June 2003.
Chenault [slides]
[quiz 8 solutions]
In-lined Reference Monitors
Mon 2/25 In-lined Reference Monitoring
Jones [slides]
[quiz 9 solutions]
Wed 2/27 Composable Policies
  • Quiz 10 on: Lujo Bauer, Jay Ligatti, and David Walker. Composing Security Policies with Polymer. In Proceedings of the ACM Conference on Programming Language Design and Implementation (PLDI'05), June 2005.
  • Supplemental (non-mandatory) reading: Lujo Bauer, Jarred Ligatti, and David Walker. Types and Effects for Non-interfering Program Monitors. In Software Security—Theories and Systems. Mext-NSF-JSPS International Symposium, Lecture Notes in Computer Science, Vol. 2609, Tokyo, Japan, November 2002.
Sridhar [slides]
[quiz 10 solutions]
Mon 3/3 Certified In-lined Reference Monitoring
Instructor [slides]
[quiz 11 solutions]
Information Flow
Wed 3/5 Overview of Language-based Information Flow
Burke [slides]
[quiz 12 solutions]
Mon 3/10 Spring Break N/A
Wed 3/12 Spring Break N/A
Mon 3/17 Class Cancelled N/A
Wed 3/19 Information Flow for Java
  • Quiz 13 on: Andrew C. Myers. JFlow: Practical Mostly-Static Information Flow Control. In Proceedings of the 26th ACM Symposium on Principles of Programming Languages (POPL'99), San Antonio, TX, January 1999.
  • Supplemental (non-mandatory) reading: Christian Grothoff, Jens Palsberg, and Jan Vitek. Encapsulating Objects with Confined Types. In Proceedings of the ACM Conference on Object-Oriented Programming Languages, Systems, and Applications (OOPSLA'01), Tampa Bay, FL, October 2001.
Urbano [slides]
[quiz 13 solutions]
Mon 3/24 Distributed Information Flow
Saeedloei [slides]
[quiz 14 solutions]
Theoretical Underpinnings of PCC, TAL and IRM's
Wed 3/26 Foundational Proof-Carrying Code
  • Quiz 15 on: Andrew W. Appel. Foundational Proof-Carrying Code. In Proceedings of the 16th Annual IEEE Symposium on Logic in Computer Science (LICS'01), Boston, MA, June 2001.
Instructor [slides]
[quiz 15 solutions]
Mon 3/31 Computational Theory of In-lined Reference Monitors Instructor
[quiz 16 solutions]
Functional Programming
Wed 4/2 Efficient, Safe Code via High-level Functional Languages
Hoglan [slides]
[quiz 17 solutions]
Obfuscation and Randomization
Mon 4/7 Address Space Randomization
Greene [slides]
[quiz 18 solutions]
Wed 4/9 Instruction Set Randomization
Instructor [slides]
[quiz 19 solutions]
Mon 4/14 Course Evaluations
Obfuscation and Type Systems
Instructor [slides]
[quiz 20 solutions]
Student Research
Wed 4/16 Aspect-Oriented Programming and IRM's
Jones
Mon 4/21 Project Presentations
  • Slot 1: Chenault, Greene, Marple (CCured)
  • Slot 2: Burke, Saeedloei, Urbano (CFI)
Various
Wed 4/23 Project Presentations
  • Slot 3: Jones, Moore, Sridhar (IRM's)
  • Slot 4: Cooke, Desautels, DeVries, Hoglan (CFI)
Various
Mon 4/28 Project Presentations
  • Slot 5: Wartell (PittSFIeld)
Course Wrap-up
Various
Wed 5/7
5:00pm
FINAL DEADLINE FOR PROJECTS: May 7th, 5:00pm
Email the following to me (hamlen at utdallas):
  • source code
  • executable code if possible (in case I can't get something to compile)
  • project write-up (approximately 5-10 pages, or more if you wish)
Your write-up should include:
  • names and email addresses of all contributors
  • detailed instructions on how to compile and test your code
  • a summary of what you attempted to do
  • an analysis of what succeeded, what didn't, and why
  • recommendations for future work
  • citations of any related work

The UTD email system does not like well-known extensions like .zip and .gz. To email me an archive, rename the extension to something benign (e.g., submission.foo) and tell me in the email body what the "real" extension should be.