Parametric non-interference in timed automata
This addresses security verification for real-time systems, but appears incremental as it builds on existing parametric timed automata techniques.
The paper tackles the problem of quantifying attack frequency in timed automata by inferring minimal time intervals between consecutive attacker actions that preserve system behavior, and synthesizes parameter valuations to guarantee non-interference, with preliminary results applied to a Fischer mutual exclusion protocol model.
We consider a notion of non-interference for timed automata (TAs) that allows to quantify the frequency of an attack; that is, we infer values of the minimal time between two consecutive actions of the attacker, so that (s)he disturbs the set of reachable locations. We also synthesize valuations for the timing constants of the TA (seen as parameters) guaranteeing non-interference. We show that this can reduce to reachability synthesis in parametric timed automata. We apply our method to a model of the Fischer mutual exclusion protocol and obtain preliminary results.