Institute of Computer Languages
Compilers and Languages Group
| Datum: | Dienstag, den 1. März 2016 |
|---|---|
| Zeit: | 14:00 Uhr c.t. *) |
| Ort: | TU Wien, Bibliothek E185.1, Argentinierstr. 8, 4. Stock (Mitte). |
über
Information flow analysis checks whether certain pieces of
(confidential) data may affect the results of computations in unwanted
ways and thus leak information. Dynamic information flow analysis adds
instrumentation code to the target software to track flows at run time
and raise alarms if a flow policy is violated; hybrid analyses combine
this with preliminary static analysis.
Using a subset of C as the target language, we extend previous work on
hybrid information flow analysis that handled pointers to scalars. Our
extended formulation handles arrays, pointers to array elements, and
pointer arithmetic. Information flow through arrays of pointers is
tracked precisely while arrays of non-pointer types are summarized
efficiently.
A prototype of our approach is implemented using the Frama-C program
analysis and transformation framework. Work on a full machine-checked
proof of the correctness of our approach using Isabelle/HOL is well
underway; we present the existing parts and sketch the rest of the
correctness argument.
(Paper accepted for VPT 2016, Workshop on Verification and Program
Transformation, colocated with ETAPS.)
Gergö Barany obtained MSc and PhD degrees from Vienna University of Technology, where he was a research assistant working on projects in program analysis, machine code generation, and interpreters. Since 2015 he is a postdoc at CEA LIST (France), working with the Frama-C framework for analysis of C programs. His interests include compilers, program verification, and static analysis. ( http://www-list.cea.fr/en/ )
Sie möchten auf diesen Vortrag durch Aushang hinweisen? Eine druckfertige Einladung im pdf-Format dafür finden Sie hier.