Gray-box monitoring of hyperproperties with an application to privacy

DOI10.1007/S10703-020-00358-WzbMATH Open1502.68187OpenAlexW3126303719MaRDI QIDQ2147690FDOQ2147690

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)

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

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

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)

Cites Work

• A brief account of runtime verification
• Symbolic execution and program testing
• A survey of challenges for runtime verification from advanced application domains (beyond software)
• Rewriting-Based Runtime Verification for Alternation-Free HyperLTL

Cited In (2)

• Efficient loop conditions for bounded model checking hyperproperties
• Monitorable hyperproperties of nonterminating systems

Uses Software

• JML
• z3
• KeY
• GitHub

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)