New Lecture in Fall: Automated Code Analysis for Large Software Systems (ACA)

Posted on by

In Fall/Winter 2013 we will be offering a new lecture on automated code analyses for large software systems. We will be discussing the most important algorithms to solve static code analysis problems efficiently and precisely, and will be presenting novel extensions of these algorithms that we have recently developed to address important real-world analysis problems like automatically detecting vulnerabilities in the Java Runtime Library (e.g. CVE_2012_4681).

This is an integrated lecture with 2 SWS and 4 CP. The lecture will take place Thursdays on 9:50-11:30 in room 3.1.01 at CASED and will comprise about 1h of lecture and 30 minutes of discussion of the weekly “homework” exercises. Exercises will consist of practical programming exercises to be solved in small teams. Over the course of the lecture, students are expected to solve through these exercises practical program-analysis problems using different techniques, exploring their tradeoffs during this process.

Preliminary outline:

The good old monotone framework:

  • Intra-procedural dataflow analyses*
  • Off-the-shelve call-graph and pointer analyses
  • Inter-procedural dataflow analyses

Efficient Tabulation-based solvers:

  • IFDS and IDE
  • Weighted pushdown systems
  • More expressive frameworks

Dealing with pointers and aliasing:

  • Problem of context reification
  • Integration of demand-driven pointer analyses

Scalability through summaries:

  • Summarizing analysis information for frameworks and libraries
  • Modeling pointers through alloc sites vs. access paths

Current and “eternal” limitations:

  • Practical limitations to current client analyses
  • Reflection, dynamic loading, eval

*) by the term “dataflow analyses” we here refer to general static code analyses, not just analyses related to information-flow

Reading Material:

  • Thomas Reps, Susan Horwitz, and Mooly Sagiv. 1995. Precise interprocedural dataflow analysis via graph reachability. POPL ’95
  • Shmuel Sagiv, Thomas W. Reps, and Susan Horwitz. 1995. Precise Interprocedural Dataflow Analysis with Applications to Constant Propagation. TAPSOFT ’95
  • Akash Lal, Thomas Reps, and Gogul Balakrishnan. 2005. Extended weighted pushdown systems. CAV 2005
  • Nomair A. Naeem, Ondřej Lhoták, and Jonathan Rodriguez. 2010. Practical extensions to the IFDS algorithm. CC 2010
  • Yannis Smaragdakis, Martin Bravenboer, and Ondrej Lhoták. 2011. Pick your contexts well: understanding object-sensitivity. POPL 2011
  • Eric Bodden. 2012. Inter-procedural data-flow analysis with IFDS/IDE and Soot. SOAP 2012
  • Rohan Padhye, Uday P. Khedker. Interprocedural Data Flow Analysis in Soot using Value Contexts. SOAP 2013