Overview

The course introduces modern automated analysis and synthesis techniques (both, deterministic and probabilistic) and shows how to apply these methods to build reliable and secure systems spanning many different domains (e.g., blockchain, networks, machine learning).

Objectives

  1. Understand how classic automated analysis and synthesis techniques work, including discrete and probabilistic methods.
  2. Understand how to apply these methods to either attack or certify systems in various domains, e.g., blockchain, networks, machine learning models, etc.
  3. Understand the state-of-the-art in the area as well as future trends.

In terms of methods, we will cover the following comprehensive set:
  • Declarative methods for expressive fixed point computation via Datalog.
  • Iterative methods for computing fixed points of infinite-state systems via Abstract Interpretation.
  • Analysis methods for large-scale automated testing and reasoning via Symbolic Execution and Fuzzing.
  • SMT based symbolic reasoning for automatically deciding logical formulas.
  • Discrete Exact Probabilistic Inference for computing densities.
  • Counter-Example guided inductive synthesis (CEGIS) for discovering new specifications and programs.

We will also show how to apply these methods to build secure and reliable systems, across 3 application domains:

Part I: Computer Networks

  • Symbolic Reasoning about computer networks (e.g., Batfish): the goal will be to prove that networks satisfy key properties (e.g., reachability between hosts). We will look at how to apply the reasoning systems for both traditional networks and state-of-the-art software-defined networks (e.g., P4).
  • Synthesis for computer networks (e.g., SyNET): the goal will be to show how to apply SMT and CEGIS methods in order to automatically synthesize configurations which lead to desirable behaviors, thus automating the job of the network operator.
  • Probabilistic inference for computer networks: we will show how to apply modern discrete probabilistic inference (e.g., PSI: PSI Solver) so to reason about probabilistic properties of networks (e.g., probability of a packet reaching a destination if links fail).

Part II: Blockchain Security

  • We will cover existing blockchains (e.g., Ethereum), how they work, what the core security issues are, and how these can lead to massive financial losses.
  • We will then discuss the latest state-of-the-art automated reasoning tools (e.g., Securify) for ensuring that smart contracts running on top of blockchains are secure and reliable, and which ensure that such losses cannot happen. Concretely, we will study how to apply AI (Abstract Interpretation), Symbolic Execution and Fuzzing so to ensure correctness and discover critical bugs.
  • We will also study the latest automated deep verification systems (e.g., Dagger) for checking custom (temporal) properties of smart contracts. These systems are already used in production (based on symbolic execution and abstraction) and we will illustrate their operation on real-world use cases.

Part III: Security and Machine Learning

  • We will show how to use probabilistic inference to ensure the probabilistic security of systems, including differential privacy.
  • We will discuss how to use machine learning models (e.g., graphical models) for security applications, in particular de-obfuscation of binaries, Android APKs and JavaScript (e.g., based on DeGuard, JSNice, and Debin: DeBIN).
  • Finally, we will discuss adversarial Deep Learning and how to generate attacks on deep learning models which fool the neural network.
To gain a deeper understanding, the course will involve a hands-on programming project where the methods studied in the class will be applied.