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 |