- Instructor: Kihong Heo
- Time: Mon/Wed 09:00 - 10:30
- Office hour: Mon 10:30 - 11:30, N5 #2321
- Location: N1 #114
This course teaches a series of topics to build safe software systems based on programming language theories and techniques. The course covers formal semantics of programming languages and state-of-the-art techniques to formally estimate software behavior to prevent security vulnerabilities beforehand. In addition, the course introduces new waves in language-based security, thereby encouraging students to imagine and realize secure and reliable programming systems.
- Homework: 30%
- Project: 30%
- Midterm: 30%
- Final: 10%
- Lecture slides will be provided
- Xavier Rival and Kwangkeun Yi, Introduction to Static Analysis: an Abstract Interpretation Perspective, MIT Press, 2020
This course includes programming assignments through which students will learn how to design
and implement program analyzers.
We will use Github/Github Classroom to provide skeleton code and manage submissions.
Make sure you have a Github account and get familiar with git
.
If you are new to git
, see this book.
Students will use the OCaml programming language for the assignments.
All submissions will be managed using Github.
For each assignment, a unique invitation URL for Github Classroom will be posted at KLMS.
Once you accept the invitation, a priviate repository for your assignment will be created.
You can push as many commits as you want before the deadline. We will grade the final commit of your master
branch.
The late homework policy is as follows:
- 80% credit for one day late
- 50% credit for two days late
- NO credit given after two days late
Students will propose their own project topics in the middle of the semester and present their final results at the end. The detailed notice will be announced after the mid term exam.
# | Topics | Reading |
---|---|---|
1 | Introduction | [Chap. 1] |
2 | Formal Semantics of Programming Languages (1): Operational Semantics | |
3 | Formal Semantics of Programming Languages (2): Denotational Semantics | |
4 | Concepts in Language-based Security | [Chap. 2] |
5 | Abstract Interpretation (1) | [Chap. 3] |
6 | Abstract Interpretation (2) | [Chap. 4] |
7 | Design and Implementation of Static Analysis | |
8 | Midterm Exam | |
9 | Static Analysis for Advanced Programming Features | [Chap. 8.1], [Chap. 8.2] |
10 | Advanced Static Analysis Techniques (1): Iteration Techniques | [Chap. 5.2] |
11 | Advanced Static Analysis Techniques (2): Sparse Analysis | [Chap. 5.3], [PLDI12] |
12 | Advanced Static Analysis Techniques (3): Modular Analysis | [Chap. 5.4], [InferBo] |
13 | New Wave in Language-based Security (1): Program Analysis with AI | [PLDI18], [PLDI19], [ICSE19] |
14 | New Wave in Language-based Security (2): Program Debloating | [CCS17] |
15 | New Wave in Language-based Security (3): Program Synthesis | [PLDI18], [IJCAI19] |
16 | Project Presentation | |
17 | Final Exam |