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
- Understand how classic program 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 blockchains, computer networks, and deep learning.
- 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