Towards verifying security policies for infinite-state systems
In Proceedings of the 16th international conference on verified software: Theories, tools, and experiments (VSTTE’24)
Abstract
Non-interference ensures no unauthorized data leaks during system execution. Verifying security policies is complex, requiring analysis of multiple execution paths. Hyperproperties provide a framework to describe security policies like non-interference. However, existing methods like HyperLTL are limited to finite-state models. This paper introduces a case study illustrating the use of HyperFOLTL, designed for infinite-state systems, and presents a formal approach to verify security policies in such systems.