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 and verification 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 labs 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: SVFIR, Control and Data Flows
	Lab: Code graphs, constraints solving
Week 3	Lecture: Pointer Aliasing and Taint Tracking
	Lab: Tainted information flow tracking
Week 4	Lecture: Code Verification Basis
	Lab: Verification concepts, predicate logic
Week 5	Lecture: Automated Theorem Proving
	Lab: Z3 theorem prover
Week 6	Study break
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

Online Resources:

• Software Security Analysis - Labs and Assignments Specs and Coding Templates
• SVF: Static Value-Flow Analysis Framework for Source Code and its doxygen
• Compilers: Principles, Techniques, and Tools Hardcover
• LLVM Compiler
• Anders Møller and Michael I. Schwartzbach, Static Program Analysis