IMDEA Software

IMDEA initiative

Home > Events > Invited Talks > 2018 > Runtime Verification of Hyperproperties for Deterministic Programs

Gerardo Schneider

Monday, July 9, 2018

10:45am Meeting room 302 (Mountain View), level 3

Gerardo Schneider, Research Professor, University of Gothenburg, Sweden

Runtime Verification of Hyperproperties for Deterministic Programs

Abstract:

In this talk I will present some results concerning the runtime monitoring of safety hyperproperties for deterministic programs. Several security and information-flow policies such as data minimality, non-interference, integrity, and software doping are naturally expressed formally as safety hyperproperties. Although there are monitoring results for hyperproperties, the algorithms are very complex since these are properties over set of traces, and not over single traces. For the deterministic input-output programs that we consider, and the specific safety hyperproperties we are interested in, the problem can be reduced to monitoring of trace properties. I will present a simpler monitoring approach for safety hyperproperties of deterministic programs. The approach involves transforming the given safety hyperproperty into a trace property, extracting a characteristic predicate for the given hyperproperty, and providing a parametric monitor taking such predicate as parameter.