A Summary Function Model for the Validation of Interprocedural Analysis Results

Karsten Klohs

University of Paderborn, Germany

The validation of data flow results safely separates complex program analyses from the use of their results. This is useful in mobile code scenarios where a code consumer with limited computational capabilities wishes to enforce that the code exhibits properties described by the analysis results in order to check security policies or to safely apply optimisations to the program.

Any valid data flow solution has to solve the system of data flow equations which describes the data flow problem for the given program. We show how this general principle can be applied to the validation of summary functions and how this yields a validation strategy for interprocedural analysis results. An important requirement is that the consumer can compare summary functions with each other. We present a function model which provides a checkable order relation on summary functions as well as all other operations needed during the validation process. The model is based on expressions which establish the connection to the inducing data flow problem in a generic way.