Gray-box runtime enforcement of hyperproperties

DOI10.1007/S00236-025-00502-1MaRDI QIDQ6939170zbMATH OpenFDO

Authors Tzu-Han Hsu, Ana Oliveira da Costa, Andrew Wintenberg, Ezio Bartocci, Borzoo Bonakdarpour

Publication date 22 August 2025

Published in Acta Informatica (Search for Journal in Brave)

Copyright license Creative Commons Attribution 4.0 International

Full work available at URL https://doi.org/10.1007/S00236-025-00502-1

Mathematics Subject Classification ID

Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.) (68N30) Formal languages and automata (68Q45) Specification and verification (program logics, model checking, etc.) (68Q60)

Cites work

• A linear-time transformation of linear inequalities into conjunctive normal form
• Bounded model checking for hyperproperties
• CAQE and QuAbS: Abstraction Based QBF Solvers
• Efficient CNF encoding of Boolean cardinality constraints
• Finite-word hyperlanguages
• Formal methods for web security
• Multiple facets for dynamic information flow
• Predictive runtime enforcement
• Preserving Secrecy Under Refinement
• Runtime enforcement monitors: Composition, synthesis, and enforcement abilities
• Runtime enforcement of hyperproperties
• Runtime enforcement of security policies on black box reactive programs
• Shield synthesis
• Spot the difference: secure multi-execution and multiple facets
• Synthesis of obfuscation policies to ensure privacy and utility
• Theory and Applications of Satisfiability Testing
• Verification of quantitative hyperproperties using trace enumeration relations
• Which security policies are enforceable by runtime monitors? A survey

This page was built for publication: Gray-box runtime enforcement of hyperproperties

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