Institute of Computer Languages
Compilers and Languages Group

Talks 2016 - Dr. Gergö Barany

Der Arbeitsbereich für Programmiersprachen und Übersetzer am Institut für Computersprachen lädt zu folgendem Vortrag ein:

Dr. Gergö Barany

CEA LIST Software Reliability Laboratory, Paris, France
Datum: Dienstag, den 1. März 2016
Zeit: 14:00 Uhr c.t. *)
Ort: TU Wien, Bibliothek E185.1, Argentinierstr. 8, 4. Stock (Mitte).
*) Tee: 13:30 Uhr in der Bibliothek E185.1, Argentinierstr. 8, 4. Stock (Mitte).


Hybrid Information Flow Analysis for Programs with Arrays


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. ( )

Sie möchten auf diesen Vortrag durch Aushang hinweisen? Eine druckfertige Einladung im pdf-Format dafür finden Sie hier.

   About Us
      Talks 2017
      Talks 2016
      Talks 2015
      Talks 2014
      Talks 2013
      Talks 2012
      Talks 2011
      Talks 2010
      Talks 2009
      Talks 2008
      Talks 2007
      Talks 2006
      Talks 2005
      Talks 2004
Fast Access:
Previous Talk
Next Talk
Faculty of Informatics
Vienna University of Technology
top | HTML 4.01 | last update: 2017-02-13 (Webmaster)