Lazy Security Controllers

A security controller follows the execution of a target to identify and prevent security violations. E ective controllers proactively observe a full execution of a target and, in case of a security violation, either interrupt or modify its original behaviour. Beyond the theoretical aspects, the assumption that a controller can observe the entire execution of its target might be restrictive in several practical cases. In this paper we de ne lazy controllers, a category of security controllers which can schedule observation points over the target execution. Finding an optimal scheduling strategy is non-trivial in general. Indeed, a lazy controller could miss security-sensitive observations. Also, we propose synthesis strategies applicable to (i) non-deterministic targets with non-instantaneous actions, (ii) probabilistic targets modelled as Discrete Time Markov Chains and (iii) stochastic targets modelled as Continuous Time Markov Chains. In each case we give an analytical characterization of the probability that the lazy controller misses the detection of a violation.