263-2925-00L  Program Analysis for System Security and Reliability

SemesterSpring Semester 2018
LecturersM. Vechev
Periodicityyearly course
Language of instructionEnglish

AbstractThe course introduces modern analysis and synthesis techniques (both, deterministic and probabilistic) and shows how to apply these methods to build reliable and secure systems spanning the domains of blockchain, computer networks and deep learning.
Objective* Understand how classic analysis and synthesis techniques work, including discrete and probabilistic methods.

* Understand how to apply the methods to generate attacks and create defenses against applications in blockchain, computer networks and deep learning.

* Understand the state-of-the-art in the area as well as future trends.
ContentThe course will illustrate how the methods can be used to create more secure and reliable systems across four application domains:

Part I: Analysis and Synthesis for Computer Networks:
1. Analysis: Datalog, Batfish
2. Synthesis: CEGIS, SyNET (http://synet.ethz.ch)
3. Probabilistic: (PSI: http://psisolver.org), its applications to networks (Bayonet)

Part II: Blockchain security
1. Introduction to space and tools.
2. Automated symbolic reasoning.
3. Applications: verification of smart contracts (http://www.securify.ch)

Part III: Security and Robustness of Deep Learning:
1. Basics: affine transforms, activation functions
2. Attacks: gradient based method to adversarial generation
3. Defenses: affine domains, AI2 (http://ai2.ethz.ch)

Part IV: Probabilistic Security:
1. Enforcement: PSI + Spire.
2. Graphical models: CRFs, Structured SVM, Pseudo-likelihood.
3. Practical statistical de-obfuscation: DeGuard: http://apk-deguard.com, JSNice: http://jsnice.org, and more.

To gain a deeper understanding, the course will involve a hands-on programming project.