Till sidans topp

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

Tipsa en vän
Utskriftsversion

Gray-box monitoring of hy… - Göteborgs universitet Till startsida
Webbkarta
Till innehåll Läs mer om hur kakor används på gu.se

Gray-box monitoring of hyperproperties

Paper i proceeding
Författare Sandro Stucki
César Sánchez
Gerardo Schneider
Borzoo Bonakdarpour
Publicerad i Formal Methods – The Next 30 Years. FM 2019. Lecture Notes in Computer Science, vol 11800
ISBN 978-3-030-30941-1
ISSN 0302-9743
Förlag Springer
Förlagsort Cham
Publiceringsår 2019
Publicerad vid Institutionen för data- och informationsteknik (GU)
Språk en
Länkar https://github.com/sstucki/minion
Ämnesord Run-time Verification Monitoring Hyperproperty Linear Temporal Logic Hyper LTL
Ämneskategorier Datavetenskap (datalogi), Programvaruteknik

Sammanfattning

Many important system properties, particularly in security and privacy, cannot be verified statically. Therefore, runtime verification is an appealing alternative. Logics for hyperproperties, such as HyperLTL, support a rich set of such properties. We first show that black-box monitoring of HyperLTL is in general unfeasible, and suggest a gray-box approach. Gray-box monitoring implies performing analysis of the system at run-time, which brings new limitations to monitorability (the feasibility of solving the monitoring problem). Thus, as another contribution of this paper, we refine the classic notions of monitorability, both for trace properties and hyperproperties, taking into account the computability of the monitor. We then apply our approach to monitor a privacy hyperproperty called distributed data minimality, expressed as a HyperLTL property, by using an SMT-based static verifier at runtime.

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?