Till sidans topp

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

Tipsa en vän
Utskriftsversion

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

Monitoring Hyperproperties by Combining Static Analysis and Runtime Verification

Paper i proceeding
Författare Borzoo Bonakdarpour
Cesar Sanchez
Gerardo Schneider
Publicerad i ISoLA'18, part II, vol. 11245 of LNCS, pages 8-27.
ISSN 03029743
Publiceringsår 2018
Publicerad vid Institutionen för data- och informationsteknik, datavetenskap (GU)
Språk en
Ämneskategorier Datavetenskap (datalogi), Data- och informationsvetenskap

Sammanfattning

© Springer Nature Switzerland AG 2018. Hyperproperties are properties whose reasoning involve sets of traces. Examples of hyperproperties include information-flow security properties, properties of coding/decoding systems, linearizability and other consistency criteria, as well as privacy properties like data minimality. We study the problem of runtime verification of hyperproperties expressed as HyperLTL formulas that involve quantifier alternation. We first show that even for a simple class of temporal formulas, virtually no ∀∃ property can be monitored, independently of the observations performed. To manage this problem, we propose to use a combination of static analysis with runtime verification. By using static analysis/verification, one typically obtains a model of the system that allows to limit the source of “hypothetical” traces to a sound over-approximation of the traces of the system. This idea allows to extend the effective monitorability of hyperproperties to a larger class of systems and properties. We exhibit some examples where instances of this idea have been exploited, and discuss preliminary work towards a general method. A second contribution of this paper is the idea of departing from the convention that all traces come from executions of a single system. We show cases where traces are extracted from the observed traces of agents, from projections of a single global trace, or from executions of different (but related) programs.

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?