CISPA
Browse
FFHL23.pdf (463.27 kB)

Automata-Based Software Model Checking of Hyperproperties

Download (463.27 kB)
conference contribution
posted on 2024-03-25, 13:15 authored by Bernd Finkbeiner, Hadar Frenkel, Jana Hofmann, Janine Lohse
We develop model checking algorithms for Temporal Stream Logic (TSL) and Hyper Temporal Stream Logic (HyperTSL) modulo theories. TSL extends Linear Temporal Logic (LTL) with memory cells, functions and predicates, making it a convenient and expressive logic to reason over software and other systems with infinite data domains. HyperTSL further extends TSL to the specification of hyperproperties – properties that relate multiple system executions. As such, HyperTSL can express information flow policies like noninterference in software systems. We augment HyperTSL with theories, resulting in HyperTSL(T), and build on methods from LTL software verification to obtain model checking algorithms for TSL and HyperTSL(T). This results in a sound but necessarily incomplete algorithm for specifications contained in the fragment of HyperTSL(T). Our approach constitutes the first software model checking algorithm for temporal hyperproperties with quantifier alternations that does not rely on a finite-state abstraction.

History

Primary Research Area

  • Reliable Security Guarantees

Name of Conference

NASA Formal Methods Symposium (NFM)

Journal

CoRR

Volume

13903

Page Range

361-379

Publisher

Springer Nature

Open Access Type

  • Green

BibTeX

@inproceedings{Finkbeiner:Frenkel:Hofmann:Lohse:2023, title = "Automata-Based Software Model Checking of Hyperproperties", author = "Finkbeiner, Bernd" AND "Frenkel, Hadar" AND "Hofmann, Jana" AND "Lohse, Janine", year = 2023, month = 6, journal = "CoRR", pages = "361--379", publisher = "Springer Nature", issn = "1611-3349", doi = "10.1007/978-3-031-33170-1_22" }