Introducing Asynchronicity to Probabilistic Hyperproperties

TL;DR

This paper introduces AHyperPCTL, an extension of HyperPCTL, adding asynchronicity to probabilistic hyperproperties by allowing delays in execution, enabling more expressive security policy specifications.

Contribution

It presents the first asynchronous extension of a probabilistic branching-time hyperlogic, enhancing the expressiveness for security and system analysis.

Findings

AHyperPCTL can express complex information-flow security policies.

A model checking algorithm for a decidable fragment is proposed.

The extension broadens the applicability of probabilistic hyperproperty analysis.

Abstract

Probabilistic hyperproperties express probabilistic relations between different executions of systems with uncertain behavior. HyperPCTL allows to formalize such properties, where quantification over probabilistic schedulers resolves potential non-determinism. In this paper we propose an extension named AHyperPCTL to additionally introduce asynchronicity between the observed executions by quantifying over stutter-schedulers, which may randomly decide to delay scheduler decisions by idling. To our knowledge, this is the first asynchronous extension of a probabilistic branching-time hyperlogic. We show that AHyperPCTL can express interesting information-flow security policies, and propose a model checking algorithm for a decidable fragment.