Program Analysis for System Security and Reliability

Spring 2018
Prof. Dr. Martin Vechev
Dr. Petar Tsankov
Dr. Dana Drachsler Cohen
Timon Gehr
Gagandeep Singh
EDoz Link
EDoz link
Lecture Time and Place
CAB G61, Monday, 1-3pm
Exercise Time and Place
CAB G61, Monday, 3-4pm

The course introduces program analysis techniques (discrete and probabilistic) and shows how to apply these to build more secure and reliable systems across several application domains and scenarios, including blockchain, computer networks, and deep learning.


  1. Understand how classic program analysis and synthesis techniques work, including discrete and probabilistic methods.
  2. Understand how to apply the methods to generate attacks and create defenses against applications in blockchains, computer networks, and deep learning.
  3. Understand the state-of-the-art in the area as well as future trends.

Part I: Computer Networks
  • Verification: Stratified Datalog (LogicBlox), network-wide configuration analysis (Batfish)
  • Synthesis: Network-wide configuration synthesis (SyNET), counter-example guided inductive synthesis (OSPF)
  • Probabilistic: Discrete distributions, analysis of probabilistic networks (Bayonet)

Part II: Security of Blockchains
  • Introduction: Bitcoin, Ethereum, and smart contracts (Solidity)
  • Static analysis: Security issues in smart contracts, Securify

Part III: Machine Learning Attacks and Defences
  • Introduction: Basics, common neural networks (affine transforms, ReLU)
  • Attacks: Adversarial examples, attacks on neural networks
  • Analysis and Defenses: Abstract interpretation, robustness analysis of neural networks (AI2)

Part IV: Machine Learning based Security and Privacy
  • Probabilistic Privacy: Spire, Differential privacy (DP-Finder)
  • De-obfuscation: Conditional random fields, JSNice, DeGuard, DeBIN

Lectures (Tentative Schedule):

No. DateContentSlides Exercises Solutions
1 Feb 19Introduction PDF
2 Feb 26Verification: Datalog, network-wide configuration analysis PDF ZIP PDF PDF
3 Mar 5Network-wide configuration synthesis PDF ZIP PDF
4 Mar 12Probabilistic Network Analysis PDFPDF PDF

Readings (Optional):