Runtime Verification of Hyperproperties for Deterministic Programs

July 9, 2018

Gerardo Schneider


Runtime Verification of Hyperproperties for Deterministic Programs

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

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.