Program Analysis for System Security and Reliability

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




Overview
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.

Objectives

  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, Souffle), 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

Project Description:

Please see the following link: Project Description Here

Lectures:

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 PDF ZIP
4 Mar 12Probabilistic Network Analysis PDFPDF PDF PDF PSI PSI
5 Mar 19Blockchains and smart contracts PDF PDF PDF
6 Mar 26Security of smart contracts PDF PDF ZIP PDF
7 Apr 9Neural Networks and adversarial examples I PDF PDF PDF
8 Apr 23Adversarial examples and robustness II PDF PDF
9 Apr 30AI2: Scalable Certification of Deep Learning PDF PDF
10 May 7Synthesis of probabilistic privacy enforcement PDF PDF PDF