Detail

CostIt: A type theory for relational resource analysis

Many areas of computer science require an analysis of the relative use of resources (time, space, etc.) by two programs, or two instances of the same program with different inputs. Examples include: 1) Compiler optimizations, where we would like to prove that an optimized program uses fewer resources than the corresponding unoptimized program, 2) Timing leaks in cryptographic implementations, where we want to prove that the runtime of a decryption algorithm is independent of the decryption key, 3) Incremental computation, where the goal is to analyze the time it will take to run a program given an earlier trace of the program on different inputs, and 4) Sensitivity analysis: How sensitive is the runtime to small input changes? CostIt is a type theory to prove such properties. CostIt refines types for secure information flow control with resource annotations and, importantly, lightweight dependent types to allow simple proofs of relative resource consumption. It is proved sound relative to relational models of types with resources, and can be implemented using SMT solvers. The talk will primarily cover the application to incremental computation.

(This talk is based on a paper from ESOP’15 and subsequent work with Ezgi Cicek, Gilles Barthe, Marco Gaboardi, Jan Hoffmann and Zoe Paraskevapoulou.)