263-2910-00L  Program Analysis

SemesterAutumn Semester 2013
LecturersM. Vechev
Periodicityyearly course
Language of instructionEnglish

AbstractThe principles of modern program analysis are key to enabling scalable and automated reasoning for a vast range of computations (e.g. mobile app security, high-performance algorithms, biological computing, device drivers).

This course is an in-depth introduction to the fundamental principles and applications of modern program analysis.

For more information: http://www.srl.inf.ethz.ch/pa.php
ObjectiveThe course has 3 main objectives:

* Understand the foundational principles behind program analysis techniques.

* Understand how to apply these principles to build practical, working analyzers. This will be helped by a hands-on programming project.

* Gain familiarity with the state-of-the-art in the research area.
ContentThe last decade has seen an explosion in modern program analysis techniques. These techniques are increasingly being used to reason about a vast range of computational paradigms including:

* finding security violations in web and mobile applications such as JavaScript and Android.
* establishing properties of biological systems (e.g. DNA computation)
* finding serious errors in systems software (e.g. Linux kernel, device drivers, file systems)
* automatic discovery of new algorithms (e.g. concurrent data structures, distributed algorithms) and end-user programming.
* compilers for domain specific languages
* architecture-driven reasoning of concurrent software (e.g. Intel's x86, ARM, IBM's Power).

This course will provide a comprehensive introduction to modern, state-of-the-art program analysis concepts and practical frameworks including:

* Dynamic Analysis:
- concepts: memory safety, typestate, concurrency analysis
- frameworks: Valgrind, FastTrack, EventRacer

* Static Analysis:
- concepts: abstract interpretation (domains, soundness, precision, fixed points)
- frameworks: Apron, PPL

* Security Analysis:
- concepts: static + dynamic combination
- example: malware detection

* Pointer analysis:
- concepts: Andersen's, Steensgaard's analysis
- frameworks: Soot, LLVM, WALA

* Program synthesis:
- concepts: L*, version spaces, PBE, CEGIS
- frameworks: Sketch, AGS, SmartEdit, ReSynth

* Predicate abstraction:
- concepts: Graf-Saidi, Boolean programs, lazy abstraction
- frameworks: Microsoft's SLAM for C programs, Fender

* Symbolic execution:
- concepts: SMT, concolic execution
- frameworks: S2E, KLEE, Sage

* Applications of Analysis & Synthesis:
- GPU programs, security errors, device drivers, concurrent algorithms, end-user programming.

To gain a deeper understanding of how to apply these techniques in practice, the course will involve a small hands-on programming project where based on the principles introduced in class, the students will build a program analyzer for a modern programming language.
Lecture notesThe lectures notes will be distributed in class.
LiteratureDistributed in class.
Prerequisites / NoticeThis course is aimed at both graduate (M.Sc., PhD) students as well as advanced undergraduate students.