COMP6131 Software Security Analysis
Course Outline
Course Details
Course Code | COMP6131 |
Course Title | Software Security Analysis |
Lecturer | A/Prof. Yulei Sui |
Units of Credit | 6 |
Course Website |
https://webcms3.cse.unsw.edu.au/COMP6131/24T2 |
Handbook Entry |
https://www.handbook.unsw.edu.au/undergraduate/courses/2024/COMP6131 (UG) https://unsw-production-internal-handbook.factor5-... (PG) |
Course Summary
This course is designed to provide a systematic exploration of automated source code analysis and verification techniques, to gain hands-on experience in implementing code analysis tools to identify common yet important software vulnerabilities in software systems. By taking this course, students can put static analysis <ins>and verification </ins>theories and advanced techniques into practice. They will be able to build source code analysis tools (e.g., written in C/C++) based on modern compilers and popular open-source frameworks to scan, comprehend and detect programming mistakes and vulnerabilities to enhance code quality and security.
This is a project-based course (no examination is required) that gives a practical opportunity to implement your own source code check to scan real-world programs. In labs, students will get hands-on experience with vulnerability assessment, compiler intermediate representation, graph representation of code, control flow and data-flow analysis. We have three major assignments (1) tainted flow tracking, (2) symbolic execution and (3) abstract execution assertion, which each builds on top of another one.
We will be using the SVF (Static Value-Flow Analysis Framework) tool as a library to perform our implementation.
Course Aim
The primary goal of this course is to familiarize students with a variety of source code analysis techniques and algorithms, ranging from fundamental to state-of-the-art. Students will be encouraged to develop their tools based on an open-source framework that uses a compiler, and they will learn how these techniques and tools can be applied to detect real-world code vulnerabilities, including tainted information flow, buffer overflow and assertion errors. Upon completing the course, students will have a comprehensive understanding of compiler-based static analysis, graph representation of source code, the current mainstream code analysis and verification techniques used, and the future challenges that must be addressed in this field.
Course Timetable
The official course timetable is available here . Please note that the timetables for postgraduates and undergraduates enrolled in COMP6131 are the same. All labs are in person .
Assessment
This is a project-based course. Assessments include lab work (30%) and three assignments (70%). Each student is required to submit work individually, and assessments will be marked on an individual basis. The details of the assessments will be explained during the lecture and lab sessions in Week 1. We aim to provide marking results approximately 1-2 weeks after each assignment deadline.
Assessment Type | Assessment Name | % |
Lab work | Coding exercises and quizzes | 30 |
Assignment 1 | Static taint tracking | 20 |
Assignment 2 | Symbolic execution | 25 |
Assignment 3 | Abstract interpretation | 25 |
Teaching Rationale
The lectures in this course provide a foundation and techniques for static code analysis and verification techniques, which aim to detect and defend against software vulnerabilities that can result in unexpected behaviors or exploitation by attackers. The lectures also explain how to apply these techniques to create practical tools for detecting and reporting common software vulnerabilities and proving the absence of bugs in system code (such as code written in C/C++).
The tutorials build upon the lectures to solidify students' conceptual understanding of software vulnerabilities, static analysis algorithms, and associated tools, including modern compilers, low-level intermediate representation of code, and constraint-solving techniques. The tutorials also provide practical knowledge relevant to the week's lab exercises.
The laboratory exercises give students a concrete understanding of compiler-based source code analysis and verification. They develop automatic auditing tools, identify vulnerabilities, and develop security analysis and testing methods to improve code quality and protect systems against cyber-attacks, which are the core conceptual outcomes of this course.
Programming assignments expand upon the skills and knowledge developed in laboratory exercises by tackling substantial practical problems. Each assignment builds upon the previous one to finally create a tool that is ready to be used for source code scanning and vulnerability detection.
Teaching Strategy
There is no single textbook that covers all the topics with the appropriate level of detail for this course, so we do not have a designated textbook. However, there are recommended references and an abundance of online materials available, including the SVF framework and its learning resources. This is a hands-on, project-based coding course; thus, we will not have exams or project reports. All evaluations will be based on your lab work and coding assignments.
Assumed Knowledge
This course is open to both undergraduate and postgraduate students who have completed COMP2521/COMP9024 the 'Data Structures and Algorithms' course with a minimum grade of 70. Waivers may be considered on a case-by-case basis. Students enrolled in this course are expected to be proficient in programming with C/C++. Lab exercises will be provided to help you acquire the necessary C++ skills for completing the assignments.
While not formal prerequisites or co-requisites, students are encouraged to enroll in COMP6771 (Advanced C++), COMP3131/COMP9131 (Compiler Courses) if they wish to gain a deeper understanding of the inner workings of compilers, and in COMP6447 for those interested in vulnerability exploitation
Academic Honesty and Plagiarism
UNSW and the School of Computer Science and Engineering (CSE) consider plagiarism a form of academic misconduct, subject to penalties as severe as exclusion from further study at UNSW. Online resources are available to help you understand what constitutes plagiarism and how it is addressed at UNSW, such as 'MyUNSW: Plagiarism and Academic Misconduct.' It is imperative that you read and comprehend these materials. Ignorance will not be accepted as an excuse for plagiarism.
Course Schedule
Week 1 | Lecture: Introduction to Software Security Analysis |
Lab: C++ practices, graph algorithms, vulnerability | |
Week 2 | Lecture: Compiler and Intermediate Representation of Code |
Lab: LLVM compiler, SVF, code graphs | |
Week 3 | Lecture: Control and data dependence |
Lab: Code graphs, constraints solving | |
Week 4 | Lecture: Pointer Aliasing and Taint Tracking |
Lab: Tainted information flow tracking | |
Week 5 |
Lecture: Code Verification Basis |
Lab: Verification concepts, predicate logic | |
Week 6 |
Lecture: Automated Theorem Proving |
Lab: Z3 theorem prover | |
Week 7 | Lecture: Code Verification using Symbolic Execution |
Lab: Symbolic execution using Z3 | |
Week 8 |
Lecture: Abstract Interpretation/Execution Foundations |
Lab: Basic concepts and examples | |
Week 9 | Lecture: Abstract Execution for Code |
Lab: Implementation of algorithms | |
Week 10 | Lecture: Buffer Overflow Detection using Abstract Execution |
Lab: Implementation and testing |