Keynote Talk: Program Analyses using Newton’s Method

Thomas Reps
University of Wisconsin (USA), GrammaTech, Inc.

Biography:

Thomas W. Reps is an American computer scientist known for his contributions to automatic program analysis. Dr. Reps is Professor of Computer Science in the Computer Sciences Department of the University of Wisconsin–Madison, which he joined in 1985. Reps is the author or co-author of four books and more than one hundred seventy-five papers describing his research. His work has covered a wide variety of topics, including program slicing, data-flow analysis, pointer analysis, model checking, computer security, instrumentation (computer programming), language-based program-development environments, the use of program profiling in software testing, software renovation, incremental algorithms, and attribute grammars.

Reps’s current work focuses on static analysis of stripped (binary) executables, and methods that—without relying on symbol-table or debugging information—recover intermediate representations that are similar to those the intermediate phases of a compiler creates for a program written in a high-level language. The goal is to provide a disassembler or decompiler platform that an analyst can use to understand the workings of COTS components, plugins, mobile code, and DLLs, as well as memory snapshots of worms and virus-infected code. Reps is President and Co-founder of GrammaTech, Inc.

Abstract:

Esparza et al. generalized Newton’s method — a numerical-analysis algorithm for finding roots of real-valued functions — to a method for finding fixed-points of systems of equations over semirings. Their method provides a new way to solve interprocedural dataflow-analysis problems. As in its real-valued counterpart, each iteration of their method solves a simpler « linearized » problem.
Because essentially all fast iterative numerical methods are forms of Newton’s method, this advance is exciting because it may provide the key to creating faster program-analysis algorithms.  However, there is an important difference between the dataflow-analysis and numerical-analysis contexts: when Newton’s method is used in numerical problems, commutativity of multiplication is relied on to rearrange an expression of the form « a * X * b + c * X * d » into « (a * b + c * d) * X. »
Equations with such expressions correspond to path problems described by regular languages. In contrast, when Newton’s method is used for interprocedural dataflow analysis, the « multiplication » operation involves function composition, and hence is non-commutative: « a * X * b + c * X * d » cannot be rearranged into « (a * b + c * d) * X. »
Equations with the former expressions correspond to path problems described by linear context-free languages (LCFLs).
This talk will present a surprising method for solving the LCFL sub-problems produced during successive rounds of Newton’s method. The method applies to predicate abstraction, on which most of today’s software model checkers rely, as well as to other abstract domains used in program analysis.
 Joint work with Emma Turetsky and Prathmesh Prabhu.

Dates (New)

February 04, 2018

Abstract submission deadline

February 11, 2018

Paper submission deadline

March 26, 2018

Acceptance notification

April 04, 2018

Camera ready copy due

Proceedings

SpringerLNCS

Revised selected papers will be published as a post-proceedings in Springer's LNCS "Lecture Notes in Computer Science"

Partners & Sponsors

SponsorsNETYS28