Parametric Timed Model Checking for Guaranteeing Timed Opacity

TL;DR

This paper develops methods for analyzing and synthesizing execution timings in timed automata to prevent information leakage, enhancing system security by ensuring timed opacity against attackers.

Contribution

It introduces a novel approach for parametric timed model checking to synthesize secure internal timings, extending existing techniques to parametric automata and program analysis.

Findings

Provided a general solution for timed opacity verification.

Extended the approach to parametric timed automata for timing synthesis.

Demonstrated applicability to program analysis.

Abstract

Information leakage can have dramatic consequences on systems security. Among harmful information leaks, the timing information leakage is the ability for an attacker to deduce internal information depending on the system execution time. We address the following problem: given a timed system, synthesize the execution times for which one cannot deduce whether the system performed some secret behavior. We solve this problem in the setting of timed automata (TAs). We first provide a general solution, and then extend the problem to parametric TAs, by synthesizing internal timings making the TA secure. We study decidability, devise algorithms, and show that our method can also apply to program analysis.