IS593: Language-based Security

Logistics

• Instructor: Kihong Heo ([email protected])
• TAs: Changhoon Song ([email protected]) , Hyunsoo Shin ([email protected])
• Time: Mon/Wed 09:00 - 10:30
• Office hour: Mon 10:30 - 11:30, N5 #2321
• Location: N1 #114

Course Description

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.

Grading

• Homework: 50%
• Project: 30%
• Midterm: 0% (due to the COVID-19 outbreak)
• Final: 20%

Textbook

• Lecture slides will be provided
• Xavier Rival and Kwangkeun Yi, Introduction to Static Analysis: an Abstract Interpretation Perspective, MIT Press, 2020

Homework

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 the student developer pack benefits. Moreover, student should 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 private 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

Project

Students will propose their own project topics in the middle of the semester and present their final results at the end. See the guidelines for the details. Here are a selected list of research papers that use static analysis for interesting problems in different area:

• Security
  • Airbus Controller SW Verification
  • API Misuse Detection
  • Side-channel Attack Detection
  • Android Malware Detection
  • Smart Contract Program Analysis
  • Web Security Analysis
• Software Engineering
  • Code Clone Detection
• Operating Systems
  • Filesystem Bug Detection
  • Linux Kernel Malicious Extension Detection
• Architecture
  • Cache Behavior Analysis

This tool will be useful when you run your LLVM analyzer for realword programs.

Academic Integrity Violation

Students who violates academic integrity will get an F.

Schedule

#	Topics		Reading	Homework
0	Functional Programming in OCaml
1	Introduction	1	[Chap. 1]	HW0: Hello-world
2	Operational Semantics	2-1, 2-2, 2-3, 2-4, 2-5		HW1: OCaml Programming
3	Denotational Semantics	3-1, 3-2, 3-3, 3-4, 3-5, 3-6
4	Concepts in Language-based Security	4-1, 4-2, 4-3, 4-4	[Chap. 2], [Chap. 9]	HW2: SmaLLVM Interpreter
5	Abstract Interpretation	5-1, 5-2, 5-3, 5-4	[Chap. 3]
6	Design and Implementation of Static Analysis	6-1, 6-2, 6-3, 6-4, 6-5	[Chap. 4]	HW3: SmaLLVM Analyzer
7	Static Analysis for Advanced Programming Features	7-1, 7-2, 7-3, 7-4, 7-5	[Chap. 8.1], [Chap. 8.2]
-	Midterm Exam			HW4 : ThriLLVM Analyzer
8	Advanced Static Analysis Techniques (1): Iteration Techniques	8-1, 8-2	[Chap. 5.2]
9	Advanced Static Analysis Techniques (2): Sparse Analysis	9-1, 9-2	[Chap. 5.3], [PLDI12]
10	Advanced Static Analysis Techniques (3): Selective X-sensitivity	10-1, 10-2	[PLDI14]
11	Advanced Static Analysis Techniques (4): Modular Analysis	11-1, 11-2	[Chap. 5.4], [InferBo]
12	New Wave in Language-based Security (1): Program Analysis with AI	12-1, 12-2, 12-3, 12-4	[PLDI18], [PLDI19], [ICSE19]
13	New Wave in Language-based Security (2): Program Debloating	13-1, 13-2, 13-3]	[TSE2002], [ICSE18], [CCS18	HW5: ThriLLVM Debloater
14	New Wave in Language-based Security (3): Program Synthesis	14-1, 14-2, 14-3]	[Book], [PLDI18], [IJCAI19	HW6: SmaLLVM Synthesizer
-	Project Presentation (6/17, 6/22, 6/24)
-	Final Exam