| Section |
Topic |
Selected?
|
| Introduction |
|
|
| Buffer Overflow (?) |
|
|
| Retlibc/ROP (?) |
|
|
| Format String(?) |
|
|
| Foundations of Software Analysis |
Proof system, soundness&completeness, program's semantics |
Model theory, real closed field |
| From Dataflow Analsyis to Abstract Interpretation |
Reaching definition, chaotic iteration, numerical domains |
Alias, symbolic abstraction, IFDS, CFL-reachability |
| Software Model Checking |
SMT, inductive loop invariant, predicate abstraction&refinement |
BMC&k-induction, PDR, trace abstraction |
| Software Testing |
Greybox fuzzing, symbolic execution, metamorphic testing |
Property-based testing, dynamic taint analysis |
| Protection? |
CFI/SFI, hardware-assisted protection |
AEG |