A type system for complexity flow analysis

Jean-Yves Marion (1)

1 CARTE - Theoretical adverse computations, and safety

We propose a type system for an imperative programming language, which certifies program time bounds. This type system is based on secure flow information analysis. Each program variable has a level and we prevent information from flowing from low level to higher level variables. We also introduce a downgrading mechanism in order to delineate a broader class of programs. Thus, we propose a relation between security-typed language and implicit computational complexity. We establish a characterization of the class of polynomial time functions.

Domaines: Logique en informatique [cs.LO]

Jean-Yves Marion. A type system for complexity flow analysis. Twenty-Sixth Annual IEEE Symposium on Logic in Computer Science - LICS 2011, Jun 2011, Toronto, Canada. ⟨hal-00591853⟩