Till sidans topp

Sidansvarig: Webbredaktion
Sidan uppdaterades: 2012-09-11 15:12

Tipsa en vän
Utskriftsversion

Runtime Verification of H… - Göteborgs universitet Till startsida
Webbkarta
Till innehåll Läs mer om hur kakor används på gu.se

Runtime Verification of Hyperproperties for Deterministic Programs

Paper i proceeding
Författare Srinivas Pinisetty
Gerardo Schneider
David Sands
Publicerad i 6th Conference on Formal Methods in Software Engineering (FormaliSE@ICSE'18), pages 20-29. ACM
ISBN 978-1-4503-5718-0
ISSN 02705257
Förlag ACM
Publiceringsår 2018
Publicerad vid Institutionen för data- och informationsteknik, datavetenskap (GU)
Språk en
Ämnesord Information-flow, Monitoring, Runtime Verification, Security
Ämneskategorier Datavetenskap (datalogi)

Sammanfattning

© 2018 Association for Computing Machinery. 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.

Sidansvarig: Webbredaktion|Sidan uppdaterades: 2012-09-11
Dela:

På Göteborgs universitet använder vi kakor (cookies) för att webbplatsen ska fungera på ett bra sätt för dig. Genom att surfa vidare godkänner du att vi använder kakor.  Vad är kakor?