Control and Synthesis of Non-Interferent Timed Systems

TL;DR

This paper investigates the synthesis of secure timed automata systems ensuring non-interference properties, proposing methods to verify and compute maximal non-interferent sub-systems.

Contribution

It introduces techniques for checking and synthesizing maximal non-interferent sub-systems in timed automata based on various non-interference notions.

Findings

Algorithms for verifying non-interference in timed automata

Methods to synthesize largest non-interferent sub-systems

Formal analysis of non-interference notions in timed systems

Abstract

In this paper, we focus on the synthesis of secure timed systems which are modelled as timed automata. The security property that the system must satisfy is a non-interference property. Intuitively, non-interference ensures the absence of any causal dependency from a high-level domain to a lower-level domain. Various notions of non-interference have been defined in the literature, and in this paper we focus on Strong Non-deterministic Non-Interference (SNNI) and two (bi)simulation based variants thereof (CSNNI and BSNNI). We consider timed non-interference properties for timed systems specified by timed automata and we study the two following problems: (1) check whether it is possible to find a sub-system so that it is non-interferent; if yes (2) compute a (largest) sub-system which is non-interferent.