Colloquium Details
Scalable and Precise Static Dataflow Analysis
Speaker: Karim Ali, University of Alberta
Location: Online
Date: December 8, 2021, noon
Host: Jinyang Li
Synopsis:
Attend via Zoom: https://nyu.zoom.us/j/97286314377
Precise detection of security vulnerabilities requires static analyses that are context-sensitive, field-sensitive, and flow-sensitive. Context-sensitivity and field-sensitivity can both be expressed as context-free language (CFL) reachability problems. However, solving both CFL problems along the same dataflow path is undecidable. Therefore, most flow-sensitive dataflow analyses over-approximate field-sensitivity by limiting the depth of successive field accesses (i.e., access path) to a certain threshold. Unfortunately, such representation does not scale very well when used to analyze complex programs, and usually produces many false positives in practice. In this talk, I will introduce the novel concept of synchronized pushdown systems (SPDS) that encodes procedure calls/returns and field stores/loads as separate but synchronized CFL reachability problems. I will show how this representation scales SPDS to large codebases, which allowed us to discover real-world security vulnerabilities due to misusing cryptography APIs in Android apps and Maven Central repositories.
Speaker Bio:
Karim Ali is an Assistant Professor in the Department of Computing Science at the University of Alberta. His research interests are in programming languages, particularly in scalability, precision, and usability of program analysis tools. His work ranges from developing new theories for scalable and precise program analyses to applications of program analysis in security and just-in-time compilers.