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
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:
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:
| 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.
|
| 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.
|
| 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 3:00-4:00 |
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 3:00-4:00 |
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 | |