Schedule

Required Readings:

• How to read a scientific paper

Required Readings:

• Galios Connection
• Undecidability of Program Analysis

Suggested Readings:

• Crash course on notations in PL papers
• Improving Integer Security for Systems with KINT
• All You Ever Wanted to Know About Dynamic Taint Analysis and Forward Symbolic Execution
• DR. CHECKER: A Soundy Analysis for Linux Kernel Drivers
• What developers want and need from Program Analysis tools

Required Readings:

• Galios Connection
• Undecidability of Program Analysis

Suggested Readings:

• Crash course on notations in PL papers
• Improving Integer Security for Systems with KINT
• All You Ever Wanted to Know About Dynamic Taint Analysis and Forward Symbolic Execution
• DR. CHECKER: A Soundy Analysis for Linux Kernel Drivers
• What developers want and need from Program Analysis tools

Required Readings:

• AFL Technical Details
• The Art, Science, and Engineering of Fuzzing: A Survey

Suggested Readings:

• Driller: Fuzzing and symbolic execution
• DIFUZE: Interface Aware Fuzzing for Kernel Drivers
• Angora: Efficient Fuzzing by Principled Search
• Be Sensitive and Collaborative: Analyzing Impact of Coverage Metrics in Greybox Fuzzing
• Not All Coverage Measurements Are Equal: Fuzzing by Coverage Accounting for Input Prioritization
• T-Fuzz: fuzzing by program transformation

Required Readings:

• AFL Technical Details
• The Art, Science, and Engineering of Fuzzing: A Survey

Suggested Readings:

• Driller: Fuzzing and symbolic execution
• DIFUZE: Interface Aware Fuzzing for Kernel Drivers
• Angora: Efficient Fuzzing by Principled Search
• Be Sensitive and Collaborative: Analyzing Impact of Coverage Metrics in Greybox Fuzzing
• Not All Coverage Measurements Are Equal: Fuzzing by Coverage Accounting for Input Prioritization
• T-Fuzz: fuzzing by program transformation

Recommended Readings:

• SOK: Sanitization for Security

Recommended Readings:

• SOK: Sanitization for Security

Required Readings:

• KLEE: Unassisted and Automatic Generation of High-Coverage Tests for Complex Systems Programs
• Symbolic Execution for Software Testing: Three Decades Later

Suggested Readings:

• SAGE: Automated Whitebox Fuzzing
• Under-constrained symbolic execution
• Target-Driven Compositional Concolic Testing
• Chopped Symbolic Execution
• QSYM: A Practical Concolic Execution Engine Tailored for Hybrid Fuzzing
• Symbolic Execution with SymCC
• Neuro-Symbolic Execution: Augmenting Symbolic Execution with Neural Constraints

Required Readings:

• A Few Billion Lines of Code Later: Using Static Analysis to Find Bugs in the Real World

Recommended Readings:

• Sys: a Static/Symbolic Tool for Finding Good Bugs in Good (Browser) Code
• μVulDeePecker: A Deep Learning-Based System for Multiclass Vulnerability Detection
• Automatic Inference of Search Patterns for Taint-Style Vulnerabilities
• Bran: Reduce Vulnerability Search Space by Learning Bug Symptoms
• ARBITRAR: User-Guided API Misuse Detection

Suggested Readings:

• Using Programmer-Written Compiler Extensions to Catch Security Holes
• How to Build Static Checking Systems Using Orders of Magnitude Less Code
• Modeling and Discovering Vulnerabilities with Code Property Graphs

Required Readings:

• SoftBound: Highly Compatible and Complete Spatial Memory Safety for C
• Preventing Use-after-free with Dangling Pointers Nullification

Suggested Readings:

• Heap Bounds Protection with Low Fat Pointers
• Backwards-Compatible Array Bounds Checking for C with Very Low Overhead
• Preventing Use-after-free with Dangling Pointers Nullification

Required Readings:

• SoftBound: Highly Compatible and Complete Spatial Memory Safety for C
• Preventing Use-after-free with Dangling Pointers Nullification

Suggested Readings:

• Heap Bounds Protection with Low Fat Pointers
• Backwards-Compatible Array Bounds Checking for C with Very Low Overhead
• Preventing Use-after-free with Dangling Pointers Nullification

Required Readings:

• SoftBound: Highly Compatible and Complete Spatial Memory Safety for C
• Preventing Use-after-free with Dangling Pointers Nullification

Suggested Readings:

• Heap Bounds Protection with Low Fat Pointers
• Backwards-Compatible Array Bounds Checking for C with Very Low Overhead
• Preventing Use-after-free with Dangling Pointers Nullification

Required Readings:

• CCured: Type-Safe Retrofitting of Legacy Code
• Dependent Types for Low-Level Programming
• Checked C: Making C Safe by Extension

Suggested Readings:

• Heap Bounds Protection with Low Fat Pointers
• Backwards-Compatible Array Bounds Checking for C with Very Low Overhead
• Preventing Use-after-free with Dangling Pointers Nullification

Required Readings:

• Automatically Finding Patches Using Genetic Programming
• The strength of random search on automated program repair
• Talos: Neutralizing Vulnerabilities with Security Workarounds for Rapid Response
• Using Safety Properties to Generate Vulnerability Patches
• SAVER: scalable, precise, and safe memory-error repair

Suggested Readings:

• An Analysis of Patch Plausibility and Correctness for Generate-and-Validate Patch Generation Systems
• Essay on the Problem Statement and the Evaluation of Automatic Software Repair
• Staged Program Repair
• How Different Is It Between Machine-Generated and Developer-Provided Patches

Required Readings:

• Automatically Finding Patches Using Genetic Programming
• The strength of random search on automated program repair
• Talos: Neutralizing Vulnerabilities with Security Workarounds for Rapid Response
• Using Safety Properties to Generate Vulnerability Patches
• SAVER: scalable, precise, and safe memory-error repair

Suggested Readings:

• An Analysis of Patch Plausibility and Correctness for Generate-and-Validate Patch Generation Systems
• Essay on the Problem Statement and the Evaluation of Automatic Software Repair
• Staged Program Repair
• How Different Is It Between Machine-Generated and Developer-Provided Patches

Required Readings:

• Automatically Finding Patches Using Genetic Programming
• The strength of random search on automated program repair
• Talos: Neutralizing Vulnerabilities with Security Workarounds for Rapid Response
• Using Safety Properties to Generate Vulnerability Patches
• SAVER: scalable, precise, and safe memory-error repair

Suggested Readings:

• An Analysis of Patch Plausibility and Correctness for Generate-and-Validate Patch Generation Systems
• Essay on the Problem Statement and the Evaluation of Automatic Software Repair
• Staged Program Repair
• How Different Is It Between Machine-Generated and Developer-Provided Patches

Required Readings:

• Large scale study of security patches
• The Attack of the Clones: A Study of the Impact of Shared Code on Vulnerability Patching
• SPIDER: Enabling Fast Patch Propagation in Related Software Repositories

Suggested Readings:

• Precisely Characterizing Security Impact in a Flood of Patches via Symbolic Rule Comparison
• Learning to Catch Security Patches
• Applicable Micropatches and Where to Find Them: Finding and Applying New Security Hot Fixes to Old Software

Required Readings:

• Large scale study of security patches
• The Attack of the Clones: A Study of the Impact of Shared Code on Vulnerability Patching
• SPIDER: Enabling Fast Patch Propagation in Related Software Repositories

Suggested Readings:

• Precisely Characterizing Security Impact in a Flood of Patches via Symbolic Rule Comparison
• Learning to Catch Security Patches
• Applicable Micropatches and Where to Find Them: Finding and Applying New Security Hot Fixes to Old Software

Required Readings:

• Large scale study of security patches
• The Attack of the Clones: A Study of the Impact of Shared Code on Vulnerability Patching
• SPIDER: Enabling Fast Patch Propagation in Related Software Repositories

Suggested Readings:

• Precisely Characterizing Security Impact in a Flood of Patches via Symbolic Rule Comparison
• Learning to Catch Security Patches
• Applicable Micropatches and Where to Find Them: Finding and Applying New Security Hot Fixes to Old Software