CS 6335: Language-based Security

2024-08-22 Admin 写评论

Hello, if you have any need, please feel free to consult us, this is my wechat: wx91due

CS 6335: Language-based Security

Course Summary

This course introduces and surveys the field of Language-based Software Security, in which techniques from compilers and programming language theory are leveraged to address issues in computer security. Topics include:

  1. Formal Methods-based Software Development
  2. In-lined Reference Monitors
  3. Software Fault Isolation
  4. Address Space Randomization
  5. Binary Software Attack Surface Reduction
  6. Certifying Compilation
  7. Web Scripting Security
  8. Information Flow Controls
  9. Cyber-deceptive Software Engineering

Course learning objectives:

  1. Ability to apply formal methods for software development
  2. Ability to develop approaches for in-lining reference monitors for enforcing security policies
  3. Ability to understand concepts in cyber deceptive software engineering
  4. ability to develop approaches for binary software attack surface reduction

About half of the course is devoted to formal methods-based development of secure software, with a focus on program-proof co-development and higher-order functional programming. The remainder of the course surveys alternative and complementary cybersecurity solutions founded on programming language semantics-based analysis, transformation, monitoring, and compilation of code. In-course discussion will highlight opportunities for cutting-edge research in each area. If you conduct work involving software security, this course will provide you with an array of powerful tools for addressing software security issues. If your work involves programming language design and implementation, 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 complementary course: Interested students may wish to consider taking CS 6371 Advanced Programming Languages before/after this course or concurrently, since it presents material that supplements and enhances several of the above topics.

Grading

Homework (30%): For the first 10 weeks of the course, students will complete a series of programming exercises assigned through eLearning. Background material helpful for completing the exercises can be found in the online textbook Software Foundations.

Quizzes (30%): Most classes will begin with a short quiz testing the students comprension of an 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, and the harder ones will test deeper understanding of more subtle points.

Class Participation (10%): Students are expected to come to class or attend online 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 (30%): Students will work individually or in a small team for the last 6 weeks of the course to complete a small project. A typical project will involve implementing and/or formally verifying a language-based security mechanism covered in the class or related to class material. Students conducting research are encouraged to choose projects that synergize with their research activities. Students will present their projects in class, with the presentation counting toward their project grade.

Attendance policy: This course is taught in an in-person modality with the expectation that students will typically interact with the instructor and other students during class through live discussion. Students should therefore only rely upon remote learning materials (e.g., recorded lectures) as a supplement to the in-person lectures, or to cover university-recognized abences (e.g., health and safety concerns, religious observances, etc.).

Texts

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

  • Benjamin C. Pierce, Arthur Azevedo de Amorim, Chris Casinghino, Marco Gaboardi, Michael Greenberg, Cătălin Hriţcu, Vilhelm Sjöberg, and Brent Yorgey. Software Foundations, Version 6.3. University of Pennsylvania, August 2023.

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

Additionally, the following text available through the UTD library may be useful for general background on type theory and functional programming:

Tentative Course Schedule

Date Topic Assigned Reading(s) Coq Exercises
Program-Proof Co-development
Lecture 1:
Mon 8/19 		Introduction to Language-based Security
Lecture Slides
Coq Demo 		Assignment 1 due 8/28
(Coq Basics)
Lecture 2:
Wed 8/21 		Functional Programming with Coq
Coq Transcript
Lecture 3:
Mon 8/26 		Program-Proof Co-development H. Zhang, S. Wang, H. Li, T.-H. Chen, and A.E. Hassan. A Study of C/C++ Code Weaknesses on Stack Overflow. IEEE Transactions on Software Engineering, 48(7):2359–2375, July 2022.
Lecture 4:
Wed 8/28 		Parametric Polymorphism M. Zamani, S. Irtiza, S. Wickramasuriya, and K.W. Hamlen. RANSAQ: Searching Source-Binary Hybrid Code Property Graphs for Vulnerabilities. Manuscript, November 2024.
No Class:
Mon 9/2 		No class: Labor Day Assignment 2 due 9/11
(Induction)
Lecture 5:
Wed 9/4 		Type Universes P. Hudak. Conception, Evolution, and Application of Functional Programming Languages. ACM Computing Surveys, 21(3):359–411, May 1989.
  • Required sections: Abstract, Introduction, 2.1, 2.3, and 2.4
Lecture 6:
Mon 9/9 		Inductive Propositions X. Leroy. Formal Verification of a Realistic Compiler. Communications of the ACM, 52(7):107–115, 2009.
Lecture 7:
Wed 9/11 		Minimal Trusted Computing Base no assigned reading
Lecture 8:
Mon 9/16 		Constructivistic Logic no assigned reading Assignment 3 due 9/23
(Lists)
Language-based Security Foundations
Lecture 9:
Wed 9/18 		The Science of Software Security J. Bau and J. C. Mitchell. Security Modeling and Analysis. IEEE Security & Privacy 9(3):18–25, 2011.
Lecture 10:
Mon 9/23 		Software Model-checking M. Müller-Olm, D. Schmidt, and B. Steffen. Model-Checking: A Tutorial Introduction. In Proc. 6th Int. Sym. Static Analysis (SAS), pp. 330–354, September 1999.
  • Required sections: 1–4.2 and 5
  • I will not quiz you on the parts about fixed point theory in Section 3.3, but do read the paragraph on Computational Tree Logic.
Lecture 11:
Wed 9/25 		Type-based Information Flow Security A. Sabelfeld and A.C. Myers. Language-Based Information-Flow Security. IEEE J. Selected Areas in Communications, 21(1):5–19, 2003. Assignment 4 due 9/30
(Polymorphism)
Code-reuse Attacks and Defenses
Lecture 12:
Mon 9/30 		Return-oriented Programming E.J. Schwartz, T. Avgerinos, and D. Brumley. Q: Exploit Hardening Made Easy. In Proc. 20th USENIX Security Symposium, 2011.
Lecture 13:
Wed 10/2 		Control-flow Integrity M. Abadi, M. Budiu, Ú. Erlingsson, and J. Ligatti. Control-Flow Integrity: Principles, Implementations, and Applications. In Proc. ACM Conf. Computer and Communications Security, pp. 340–353, 2005. Assignment 5 due 10/9
(Logical Operators)
Lecture 14:
Mon 10/7 		Machine-checked Native Code Validation D. Brumley, I. Jager, T. Avgerinos, and E.J. Schwartz. BAP: A Binary Analysis Platform. In Proc. Int. Conf. Computer Aided Verification (CAV), 2011.
Lecture 15:
Wed 10/9 		Superset Disassembly E. Bauman, Z. Lin, and K.W. Hamlen. Superset Disassembly: Statically Rewriting x86 Binaries Without Heuristics. In Proc. Network and Distributed Systmes Security Sym. (NDSS), 2018.
Lecture 16:
Mon 10/14 		Binary Stirring R. Wartell, V. Mohan, K.W. Hamlen, and Z. Lin. Binary Stirring: Self-randomizing Instruction Addresses of Legacy x86 Binary Code. In Proc. ACM Conf. Computer and Communications Security (CCS), 2012. Assignment 6 due 10/28
(Inductive Props)
Lecture 17:
Wed 10/16 		Binary Attack Surface Reduction M. Ghaffarinia and K.W. Hamlen. Binary Control-flow Trimming. In Proc. ACM Conf. Computer and Communications Security (CCS), 2019.
In-lined Reference Monitors
Lecture 18:
Mon 10/21 		Theory of IRMs F.B. Schneider. Enforceable Security Policies. ACM Transactions on Information and System Security, 3(1):30–50, 2000.
Lecture 19:
Wed 10/23 		TBA TBA
Lecture 20:
Mon 10/28 		IRM Validation K.W. Hamlen, M.M. Jones, and M. Sridhar. Aspect-oriented Runtime Monitor Certification. In Proc. 18th Int. Conf. Tools and Algorithms for the Construction and Analysis of Systems (TACAS), pp. 126–140, March–April 2012.
Lecture 21:
Wed 10/30 		Web Scripting Security P.H. Phung, M. Monshizadeh, M. Sridhar, K.W. Hamlen, and V.N. Venkatakrishnan. Between Worlds: Securing Mixed JavaScript/ActionScript Multi-party Web Content. IEEE Transactions on Dependable and Secure Computing (TDSC), 12(4):44–457, July–August 2015. Project due 12/15
Current Research
Lecture 22:
Mon 11/4 		Binary Rewriting Compatibility Challenges X. Xu, M. Ghaffarinia, W. Wang, K.W. Hamlen, and Z. Lin. ConFIRM: Evaluating Compatibility and Relevance of Control-flow Integrity Protections for Modern Software. In Proc. USENIX Security Symposium, 2019.
Lecture 23:
Wed 11/6 		Object Flow Integrity W. Wang, X. Xu, and K.W. Hamlen. Object Flow Integrity. In Proc. ACM Computer and Communications Security (CCS), 2017.
Lecture 24:
Mon 11/11 		Cyber-deceptive Software Engineering F. Araujo, K.W. Hamlen, S. Biedermann, and S. Katzenbeisser. From Patches to Honey-Patches: Lightweight Attacker Misdirection, Deception, and Disinformation. In Proc. ACM Computer and Communications Security (CCS), 2014.
Lecture 25:
Wed 11/13 		Project/Coq/Picinæ Q&A no assigned reading
No Class:
Mon 11/18 		No class: Fall break
No Class:
Wed 11/20 		No class: Fall break
Conclusions
Lecture 26:
Mon 11/25 		Project Q&A, Assignment Solutions no assigned reading
Lecture 27:
Wed 11/27 		Course Wrap-up & Conclusions
Presentations 1:
Mon 12/2 		Project Presentations
Presentations 2:
Wed 12/4 		Project Presentations

发表评论

电子邮件地址不会被公开。 必填项已用*标注