ABSTRACT. 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 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 tutorial, I will discuss novel techniques for detecting and quantifying information leakage in computer systems. In particular, I will discuss how symbolic execution, combined with a model counting constraint solver, can be used for detecting and quantifying side-channel leakage in programs, and also for identifying input sequences that can be used to recover secrets. I will also discuss how we implemented this approach as an extension to the symbolic execution tool SPF using our model counting constraint solver ABC.

Bio:

Tevfik Bultan is a Professor and the Chair of the Department of Computer Science at the University of California, Santa Barbara (UCSB). His research interests are in software verification, program analysis, software engineering, and computer security. He co-chaired the program committees of several conferences including the 20th International Symposium on the Foundations of Software Engineering (FSE 2012) which is the flagship conference of ACM SIGSOFT, the 28th IEEE/ACM International Conference on Automated Software Engineering (ASE 2013) and the 41st ACM/IEEE International Conference on Software Engineering (ICSE 2019) which is the premier software engineering conference in the world. He was the general chair of the 2017 ACM SIGSOFT International Symposium on Software Testing and Analysis (ISSTA 2017). He was an associate editor of the IEEE Transactions of Software Engineering (TSE) from 2014 to 2018 and he is currently an associate editor of the ACM Transactions on Software Engineering and Methodology (TOSEM). He received a NATO Science Fellowship from the Scientific and Technical Research Council of Turkey (TUBITAK) in 1993, a Regents' Junior Faculty Fellowship from the University of California, Santa Barbara in 1999, a Faculty Early Career Development (CAREER) Award from the National Science Foundation in 2000, the ACM SIGSOFT Distinguished Paper Award and the Best Paper Award at the 20th IEEE/ACM International Conference on Automated Software Engineering (ASE 2005), the ACM SIGSOFT Distinguished Paper Award at the 29th IEEE/ACM International Conference on Automated Software Engineering (ASE 2014), and the UCSB Academic Senate Outstanding Graduate Mentor Award in 2016. He was recognized as an ACM Distinguished Scientist in 2016.

ABSTRACT. This tutorial introduces the basic ideas behind probabilistic programming --- a form of machine learning that combines the systematic specification of stochastic models as programs that manipulate probability distributions, while incorporating observational data in the form of conditioning.   The objectives of this tutorial are threefold: (a) provide the learner with the big picture of what probabilistic programming is (and is not); (b) enable a hands-on look at some of the concepts underlying probabilistic programming with some non-trivial examples; and (c) describe some of the open research problems of most interest to the CAV community.

The first part of the tutorial will motivate probabilistic programming starting  from the basic forms of probabilistic models  that include Bayes nets and hierarchical models. Ideas  that are closely related to probabilistic programming have been studied by the control theory community in the form of state estimation and filtering. 

Next, we motivate probabilistic programming through a few ``hands-on''  exercises, wherein we will specify various models for biological and physical processes. We show how inference techniques can incorporate observational data in these models in order to compute posterior distributions for the model parameters. In this process, we demonstrate a few ways in which probabilistic programming can enable applications to "data-driven" formal verification, wherein the models being verified are defined by probabilistic programs. 

The last part of the tutorial will focus briefly  on existing verification of properties for probabilistic programs: how do we argue about invariance, termination, and various other properties of these programs; synthesis of probabilistic programs: how do we find an "appropriate" probabilistic program that generates/explains the data we see; systematic inference: how do we perform inference with guarantees  and many other open problems of potential interest to the CAV community.

This tutorial involves contributions from students at the University of Colorado, Boulder including Michael Dresser, Souradeep Dutta, Taisa Kushner and Chou Yi.

Bio:

Sriram Sankaranarayanan is an S.J. Archuleta endowed associate professor of Computer Scienceat the University of Colorado, Boulder. His research interests include automatic techniques forreasoning about the behavior of cyber-physical systems.  Sriram obtained a PhD in 2005 from Stanford University where he was  advised by Zohar Manna and Henny Sipma. Subsequently he worked as a  research staff member at NEC research labs in Princeton, NJ.He has been on the faculty at CU Boulder since 2009. Sriram has been the recipient of awards including the President's Gold Medal from IIT Kharagpur (2000), Siebel Scholarship(2005), the CAREER award from NSF (2009) and various teaching/research awards from the University of Colorado.