Many computer systems have access to sensitive information nowadays and, consequently, information leakage has become a significant security concern for users. Side-channel vulnerabilities that are based on information gained by observing non-functional properties of computer systems (such as execution time or memory usage) can enable attackers to infer the secret information that the system accesses. In this course, we will discuss static and dynamic analysis techniques for detecting information leakage in computer systems. In most practical settings, complete elimination of information leakage, where all observable outputs are independent of secrets (called noninterference), is not achievable. An alternative approach, called quantitative information flow analysis, is to quantify the amount of information that leaks from a given computer system using information theoretic concepts such as entropy. Quantitative information flow analysis enables detection of harmful side-channel vulnerabilities while minimizing false alarms that are due to benign information leakage.
In this course, we will discuss recent developments in detection of side-channel vulnerabilities and quantitative information flow analysis. The topics we will discuss in this course include:
* static and dynamic analysis techniques for side-channel detection,
* probabilistic symbolic execution,
* model counting constraint solvers,
* hyperproperties in temporal logics, and
* attack synthesis.