Parametric non-interference in timed automata

TL;DR

This paper introduces a method for analyzing non-interference in timed automata by quantifying attack frequency and synthesizing parameter valuations to ensure security, demonstrated on a mutual exclusion protocol.

Contribution

It proposes a novel approach to measure and guarantee non-interference in timed automata using parametric synthesis techniques.

Findings

Quantifies attack frequency in timed automata.

Synthesizes timing parameters to ensure non-interference.

Applied to Fischer mutual exclusion protocol with promising results.

Abstract

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.