CS 6V81-003: Language-based Security

Course Information

Title: CS 6V81-003: Language-based Security
Course Registration Number: 81895
Times: MW 1:00-2:15
Location: ECSN 2.110
Instructor: Dr. Kevin Hamlen (hamlen AT utdallas)
Instructor's Office Hours: MW 4:00-5:00, ECSS 3.704
TA: Kyle Marple (kbm072000 AT utdallas)
TA's Office Hours: Tu Th 2:00-4:00, ECSS 4.409

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. Certifying Compilers
  2. In-lined Reference Monitors
  3. Software Fault Isolation
  4. Address Space Randomization
  5. Binary Obfuscation
  6. Web Scripting Security
  7. Information Flow Control

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 you do research involving software security, this course will provide you with an array of powerful tools for addressing software security issues. If you do research involving programming languages or compilers, this course will show you how to take techniques that you already know and apply them to a new and important problem domain. If your career involves management or development of high-assurance software systems, this course will provide a comparative analysis of traditional versus language-based techniques.

The course is open to Ph.D. students and Masters students. Interested undergraduates should see the instructor for permission to take the course.

Suggested (non-mandatory) prerequisite: CS 6371 Advanced Programming Languages (or taken concurrently)


Homework: Homeworks will consist of assigned readings, usually one required paper per class session. Students must thoroughly read each paper before class in order to adequately prepare for in-class quizzes and discussions.

Quizzes (30%): Each class will begin with a short quiz testing the students comprension of the assigned reading for the day. Questions will typically be multiple choice or short answer. The easier questions will be designed to test whether the student has read the material at all, and the harder ones will test deeper understanding of more subtle points.

Class Participation (10%): Students are expected to come to class having read the assigned paper(s), and prepared with questions, critiques, and discussion topics. Regular attendance and class participation will count 10% towards their grades in the course.

Project (40%): Students 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. Project proposals will be due early in the semester (deadline to be announced). A typical project involves implementing one of the concepts described in one of the assigned readings, or by 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 vulnerability. Some overlap of class projects with the student's doctoral or masters thesis research is both permitted and encouraged.

Presentations (20%): Each project team will deliver 2 20-minute presentations. At midsemester, they will present a 20-minute overview of their project idea, along with background and motivation. At semester end, they will present a 20-minute summary of project outcomes and results. Not all team members need speak, but all are expected to participate in preparation of the presentation (e.g., slide creation). All team members will share a common presentation grade.


In our study of the Coq theorem proving system, we will be using the following online textbook:

For those who wish to explore Coq in greater depth (e.g., for developing their projects), the following book by the Coq developers is highly recommended:

Additionally, the following two texts available through the UTD library may be useful for general background on type theory and computer security, respectively:

Tentative Course Schedule

Date Topic Assigned Reading(s)
Introduction and Review
Mon 8/27 Introduction: Course Summary and Logistics
Lecture Slides
No assigned reading. Download and install Coq. Start playing with it and following the tutorial.
Wed 8/29 The Science of Security
Lecture Slides
J. Bau and J. C. Mitchell. Security Modeling and Analysis. IEEE Security & Privacy 9(3):18-25, 2011.
Mon 9/3 No class: Labor Day
Wed 9/5 Programming Languages Foundations: Types
Lecture Slides
F. B. Schneider, G. Morrisett, and R. Harper. A Language-based Approach to Security. Informatics: 10 Years Back, 10 Years Ahead, Lecture Notes in Computer Science, 2000.
Mon 9/10 Programming Language Foundations: Theorem-proving and Program-development A. Datta, J. Franklin, D. Garg, L. Jia, and D. K. Kaynar. On Adversary Models and Compositional Security. IEEE Security & Privacy 9(3):26-32, 2011.
Automated Theorem-proving
Wed 9/12 Intro to Coq
Coq Transcript
B. C. Pierce, C. Casinghino, M. Greenberg, V. Sjöberg, and B. Yorgey. Software Foundations: Basics: Functional Programming and Lists: Data Structures in Coq. U. Pennsylvania, 2012.
  • Homework (instead of quiz): Prove theorems plus_n_Sm and plus_comm in Coq, and then solve the "4 stars, recommended (binary)" exercise near the bottom of the Basics chapter. Submit solutions as a text file via eLearning.
Mon 9/17 Coq Polymorphism
Coq Transcript
B. C. Pierce, C. Casinghino, M. Greenberg, V. Sjöberg, and B. Yorgey. Software Foundations: Poly: Polymorphism and Higher-Order Functions. U. Pennsylvania, 2012.
  • Homework (instead of quiz): Prove the map_rev theorem in Coq. To get you started, here is a template file with the basic definitions you'll need.
Wed 9/19 Program Development in Coq
Coq Transcript
No assigned reading. Form groups and generate project ideas.
Mon 9/24 Certifying Imperative Programs
Lecture Slides
A. Nanevski, G. Morrisett, A. Shinnar, P. Govereau, and L. Birkedal. Ynot: Dependent Types for Imperative Programs. In Proceedings of the 13th ACM SIGPLAN Int. Conf. on Functional Programming (ICFP), pp. 229-240, 2008.
Web Security
Wed 9/26 Web Security Problems
Lecture Slides
Ú. Erlingsson, B. Livshits, and Y. Xie. End-to-end Web Application Security. In Proceedings of the 11th Workshop on Hot Topics in Operating Systems, 2007.
Mon 10/1 Short class: Quiz only T. Ball, V. Levin, and S.K. Rajamani. A Decade of Software Model Checking with SLAM. Communications of the ACM, 54(7):68-76, 2011.
Wed 10/3 Language-based JavaScript Security
Lecture Slides
L. A. Meyerovich and B. Livshits. ConScript: Specifying and Enforcing Fine-Grained Security Policies for JavaScript in the Browser. In Proceedings of the 31st IEEE Symposium on Security & Privacy, pp. 481-496, 2010.
Fri 10/5 at 11:00am Distinguished Lecture (TI Auditorium) Guest speaker: Thomas Ball, Microsoft
In-lined Reference Monitors
Mon 10/8 Theory of IRMs, Safety, and Liveness
Lecture Slides
F. B. Schneider. Enforceable Security Policies. ACM Trans. Inf. Syst. Secur. 3(1):30-50, 2000.
Wed 10/10 Type-based IRM Certification
Presentation Tips
Lecture Slides
K. W. Hamlen, G. Morrisett, and F. B. Schneider. Certified In-lined Reference Monitoring on .NET. In Proc. of the ACM SIGPLAN Workshop on Programming Languages and Analysis for Security (PLAS), pp. 7-16, 2006.
Mon 10/15 Project Proposal Presentations
Wed 10/17 Project Proposal Presentations
Mon 10/22 Aspect-oriented Programming and IRMs
Lecture Slides
K. W. Hamlen, M. M. Jones, and M. Sridhar. Aspect-Oriented Runtime Monitor Certification. In Proc. of the 18th Int. Conf. on Tools and Algorithms for the Construction and Analysis of Systems (TACAS), pp. 126-140, 2012.
Software Fault Isolation
Wed 10/24 Control-flow Integrity
Lecture Slides
M. Abadi, M. Budiu, Ú. Erlingsson, and J. Ligatti. Control-Flow Integrity: Principles, Implementations, and Applications. In Proc. of the ACM Conf. on Computer and Communications Security, pp. 340-353, 2005.
Mon 10/29 Google Native Client
Lecture Slides
B. Yee, D. Sehr, G. Dardyk, J. B. Chen, R. Muth, T. Ormandy, S. Okasaka, N. Narula, and N. Fullagar. Native Client: A Sandbox for Portable, Untrusted x86 Native Code. Communications of the ACM, 53(1), 2010.
Wed 10/31 No Class: Attend TexSAW
Mon 11/5 CISC SFI Without Source Code
Lecture Slides
R. Wartell, V. Mohan, K. W. Hamlen, and Z. Lin. Securing Untrusted Code via Compiler-Agnostic Binary Rewriting. In Proc. of the 28th Annual Computer Security Applications Conf. (ACSAC), 2012, in press.
Code-injection Attacks and Defenses
Wed 11/7 Control-flow Hijacking
Lecture Slides
H. Shacham, M. Page, B. Pfaff, E.-J. Goh, N. Modadugu, and D. Boneh. On the Effectiveness of Address-Space Randomization. In Proc. of the ACM Conf. on Computer and Communications Security (CCS), pp. 298-307, 2004.
Fri 11/9
Data Execution Prevention and Return-oriented Programming
Located in ECSS 3.503
Lecture Slides
E. J. Schwartz, T. Avgerinos, and D. Brumley. Q: Exploit Hardening Made Easy. In Proc. of the 20th USENIX Security Symposium, 2011.
Mon 11/12 Code randomization
Quiz on reading from Fri 11/9
Lecture Slides
V. Pappas, M. Polychronakis, and A. D. Keromytis. Smashing the gadgets: Hindering Return-oriented Programming Using In-place Code Randomization. In Proc. of the IEEE Symposium on Security & Privacy, pp. 601-615, 2012.
Wed 11/14 Short class: Quiz on reading from Mon 11/12 No assigned reading
Mon 11/19 No Class: Fall Break
Wed 11/21 No Class: Fall Break
Mon 11/26 Legacy code randomization
Lecture Slides
R. Wartell, V. Mohan, K. W. Hamlen, and Z. Lin. Binary Stirring: Self-randomizing Instruction Addresses of Legacy x86 Binary Code. In Proc. of the 19th ACM Conference on Computer and Communications Security (CCS), 2012.
Binary Obfuscation
Wed 11/28 No Class: Class moved to Friday
Fri 11/30
Polymorphic Malware
Located in SLC 2.302
No quiz (quiz deferred to Monday 12/3)
Z. Wu, S. Gianvecchio, M. Xie, and H. Wang. Mimimorphism: A New Approach to Binary Code Obfuscation. In Proc. of the ACM Conf. on Computer and Communications Security (CCS), pp. 536-546, 2010.
Mon 12/3 Metamorphic Malware
Project Instructions
V. Mohan and K. W. Hamlen. Frankenstein: Stitching Malware from Benign Binaries. In Proc. of the 6th USENIX Workshop on Offensive Technologies (WOOT), 2012.
Information Flow Control
Wed 12/5 No Class (due to ACSAC)
Reading is optional (but highly recommended!): no quiz
A. Sabelfeld and A. C. Myers. Language-Based Information-Flow Security. IEEE Journal on Selected Areas in Communications, 21(1):5-19, 2003.
Mon 12/10 Project Presentations
Wed 12/12 Project Presentations
Mon 12/17
12:00 noon
Final Projects Due