Gray-box monitoring of hyperproperties with an application to privacy

DOI10.1007/S10703-020-00358-WMaRDI QIDQ2147690zbMATH OpenOpenAlexFDO

Authors Sandro Stucki, César Sánchez, Gerardo Schneider, Borzoo Bonakdarpour

Publication date 20 June 2022

Published in Formal Methods in System Design (Search for Journal in Brave)

Copyright license Creative Commons Attribution 4.0 International

Full work available at URL https://doi.org/10.1007/s10703-020-00358-w

zbMATH Keywords

securityruntime verificationprivacyLTLmonitorabilitydata minimizationhyperLTLhyperproperty

Mathematics Subject Classification ID

Specification and verification (program logics, model checking, etc.) (68Q60) Temporal logic (03B44) Privacy of data (68P27)

Recommendations

• Monitoring hyperproperties
• Runtime enforcement of hyperproperties
• Rewriting-based runtime verification for alternation-free HyperLTL
• Time-triggered runtime verification
• Symbolic runtime verification for monitoring under uncertainties and assumptions

Cites work

• A brief account of runtime verification
• A survey of challenges for runtime verification from advanced application domains (beyond software)
• Rewriting-based runtime verification for alternation-free HyperLTL
• Symbolic execution and program testing

Cited in

(3)

• Efficient loop conditions for bounded model checking hyperproperties
• Monitorable hyperproperties of nonterminating systems
• Gray-box monitoring of hyperproperties

Describes a project that uses

Uses Software

• GitHub
• KeY
• z3
• JML

This page was built for publication: Gray-box monitoring of hyperproperties with an application to privacy

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q2147690)