Overview
Security issues and privacy breaches in modern systems (blockchains, datacenters, AI, etc.) result in billions of losses due to hacks and system downtime. This course introduces the security issues in such modern systems and covers state-of-the-art automated techniques (developed in the past few years) that can are applied to build more secure and reliable systems. The course has a practical focus and covers systems build by successful ETH spin-offs (ChainSecurity, which was acquired by PwC, and DeepCode).
Objectives
- Learn about security issues in modern systems -- blockchains, smart contracts, data centers -- and why they are challenging to address.
- Understand how the latest automated analysis techniques work, both discrete and probabilistic.
- Understand how these techniques combine with machine-learning methods, both supervised and unsupervised.
- Understand how to use these methods to build reliable and secure modern systems.
- Learn about new open problems that if solved can lead to research and commercial impact.
Part I: Security of Blockchains
- We will cover existing blockchains (e.g., Ethereum, Bitcoin), how they work, what the core security issues are, and how these have led to massive financial losses.
- We will show how to extract useful information about smart contracts and transactions using interactive analysis frameworks for querying blockchains (e.g. Google's Ethereum BigQuery).
- We will discuss the state-of-the-art security tools (e.g., Securify) for ensuring that smart contracts are free of security vulnerabilities.
- We will study the latest automated reasoning systems (e.g., VerX) for checking custom (temporal) properties of smart contracts and illustrate their operation on real-world use cases.
Part II: Security of Datacenters and Networks
- We will show how to ensure that datacenters and ISPs are secured using declarative reasoning methods (e.g., Datalog). We will also see how to automatically synthesize secure configurations (e.g. using SyNET and NetComplete) which lead to desirable behaviors, thus automating the job of the network operator and avoiding critical errors.
- We will discuss how to apply modern discrete probabilistic inference (e.g., PSI and Bayonet) so to reason about probabilistic network properties (e.g., the probability of a packet reaching a destination if links fail).
Part III: Machine Learning for Security
- We will discuss how machine learning models for structured prediction are used to address security tasks, including de-obfuscation of binaries (DeBIN), Android APKs (DeGuard) and JavaScript (JSNice).
- We will study to leverage program abstractions in combination with clustering techniques to learn security rules for cryptography APIs from large codebases.
- We will study how to automatically learn to identify security vulnerabilities related to the handling of untrusted inputs (cross-Site scripting, SQL injection, path traversal, remote code execution) from large codebases.
Course Project
The course involve a hands-on programming project where the methods studied in the class will be applied. You can work on the project in a group consisting of at most 2 students. Registration is closed.The description of the course project can be found here.
Answers to common student questions can be found here.
Deadlines:
| Group registration | 6PM CEST, April 2, 2020 |
| Project announcement | 6PM CEST, April 6, 2020 |
| Preliminary deadline (optional) | 6PM CEST, May 17, 2020 |
| Preliminary feedback | 6PM CEST, May 25, 2020 |
| Final deadline | 6PM CEST, May 31, 2020 |
Lectures
| No. | Date | Content | Slides | Exercises | Solutions | Recording |
|---|---|---|---|---|---|---|
| 1 | Feb 17 | Introduction |  |
No Exercise | ||
| 2 | Feb 24 | Blockchain basics and Bitcoin | |
 |
|
|
| 3 | Mar 02 | Ethereum and smart contracts | |
|
|
|
| 4 | Mar 09 | Fuzzing | |
|
|
  |
| 5 | Mar 16 | Datalog and static analysis | |
|
|
|
| 6 | Mar 23 | Functional specification | |
|
|
|
| 7 | Mar 30 | Formal verification | |
|
|
|
| 8 | Apr 6 | Formal verification wrap-up \& Project announcement | |
|
||
| 9 | Apr 27 | Network verification | |
|
|
|
| 10 | May 4 | Network synthesis | |
|
|
|
| 11 | May 11 | Big code | |
No Exercise | |
|
| 12 | May 18 | Summary lecture | |
No Exercise | |