Institute of Computer Languages
Compilers and Languages Group
on
| Date: | Tuesday, December 4th, 2007 |
|---|---|
| Time: | 14:00 (s.t.) |
| Location: | TU Wien, Bibliothek E185.1, Argentinierstraße 8, 4. Stock, Mitte |
We consider a special incarnation of a mobile code scenario where a producer attaches results of interprocedural program analyses to a program and transmits the annotated code via an inherently insecure communication channel like the internet. The aim of a target device like a mobile phone is to check the validity of the analysis results even though its computational capabilities do not suffice to compute the results on its own. After validation the results can be safely used to check security policies or to 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 other operations like function composition and meet in a generic way. The model is based on expressions which establish the connection to the inducing data flow problem. Simple bit-vector analyses can be formulated solely in terms of basic expressions while additional function application expressions keep the model powerful enough to deal with more sophisticated analysis like integer constant propagation or simple type inference problems.
Furthermore, we provide a brief overview about more advanced issues like simplification of function representations, integration of local variables into the model for method invocation sites, dynamic method binding, and more sophisticated scenarios like incremental validation or validation for incomplete programs.
Karsten Klohs hat an der Universität Paderborn Informatik studiert, wo er zur Zeit im Fachgebiet Programmiersprachen und Übersetzer als wissenschaftlicher Mitarbeiter tätig ist und an seiner Dissertation arbeitet. Sein Forschungsschwerpunkt liegt im Bereich der Programmanalyse, wobei neben den grundlegenden Verfahren ihre spezialisierte Anwendung im Vordergrund steht. Von besonderem aktuellen Interesse sind dabei insbesondere folgende Themen: die effiziente Validierung der Ergebnisse von Programmanalysen, die speichereffiziente Bytecode Verifikation auf Java Karten und die automatische Verteilung nebenläufiger Java Programme.