- Instructor: Kihong Heo (허기홍, kihong.heo@kaist.ac.kr)
- TAs: Changhoon Song (송창훈, songch@kaist.ac.kr), Myojoon Kil (길묘준, myojoonkil@kaist.ac.kr)
- Time: Mon/Wed 09:00-10:15
- Office hour: by appointment
- Location: Zoom
This course covers advanced topics in software security. Students will be exposed to techniques that are gaining increasing attention in the software security research communities through research papers and programming assignments. Students will have opportunities to develop their scientific communication skills through writing their own project proposals and presenting their solutions.
- Homework: 40%
- Paper Presentation: 30%
- Project: 30%
- Lecture slides will be provided
- Paul C. van Oorschot, Computer Security and the Internet: Tools and Jewels, Springer, 2020
- Andreas Zeller et al., The Fuzzing Book
- Benjamin C. Pierce, Types and Programming Languages, MIT Press, 2002
- Aaron R. BradleyZohar Manna, The Calculus of Computation, Springer, 2007
- 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 dynamic and static 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 togit, see this book. All submissions will be managed using Github. For each assignment, a unique invitation URL for Github Classroom will be posted in this page. 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 yourmasterbranch. 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 use the OCaml programming language for the assignments. For more details of OCaml, see the following meterials:
-
Students will use the LLVM infrastructure and implement various tools that analyze programs written in LLVM IR code. LLVM IR code can be generated from many source languages such as C/C++/Obj-C, Swift, Rust, Scala, Haskell, etc. For more details of LLVM, see this document.
-
Students will use the Z3 theorem prover that automatically prove logical contraints (e.g., safety conditions) generated by your analyzer from LLVM IR.
Students who violates academic integrity will get an F.
Project