| Title | Runtime Verification of Hyperproperties for Deterministic Programs |
| Publication Type | Conference Paper |
| Year of Publication | 2018 |
| Authors | Pinisetty, Srinivas, Schneider, Gerardo, Sands, David |
| Conference Name | 2018 IEEE/ACM 6th International FME Workshop on Formal Methods in Software Engineering (FormaliSE) |
| Date Published | June 2018 |
| Publisher | ACM |
| Keywords | data minimality, deterministic algorithms, deterministic input-output programs, Doping, finite element analysis, i-o systems security, i/o systems security, information-flow, information-flow policies, Monitoring, noninterference, parametric monitor, program verification, pubcrawl, Runtime, runtime verification, runtime verification monitors, runtime verification problem, Safety, safety hyperproperty, Scalability, security, security of data, security policies, Software, software doping, system monitoring |
| Abstract | In this paper, we consider the runtime verification problem 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. In this paper, we 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. For any hyperproperty in the considered subclass, we show how runtime verification monitors can be synthesised. We have implemented our approach in the form of a parameterised monitor for the given class, and have applied it to a number of hyperproperties including data minimisation, non-interference, integrity and software doping. We show results concerning both offline and online monitoring. |
| URL | https://dl.acm.org/doi/10.1145/3193992.3193995 |
| DOI | https://doi.org/10.1145/3193992.3193995 |
| Citation Key | pinisetty_runtime_2018 |
Runtime Verification of Hyperproperties for Deterministic Programs