strategFTO: Untimed control for timed opacity

TL;DR

This paper presents strategFTO, a tool for verifying timed opacity in critical software systems by controlling allowed actions to ensure attacker uncertainty about secret information based on execution time.

Contribution

It introduces an untimed control approach for timed opacity verification in timed automata, with a practical algorithm implementation and evaluation.

Findings

The untimed control problem for timed opacity is not more complex than the full problem.

The proposed algorithm effectively verifies timed opacity in practice.

strategFTO successfully demonstrates control synthesis for security properties.

Abstract

We introduce a prototype tool strategFTO addressing the verification of a security property in critical software. We consider a recent definition of timed opacity where an attacker aims to deduce some secret while having access only to the total execution time. The system, here modeled by timed automata, is deemed opaque if for any execution time, there are either no corresponding runs, or both public and private corresponding runs. We focus on the untimed control problem: exhibiting a controller, i.e., a set of allowed actions, such that the system restricted to those actions is fully timed-opaque. We first show that this problem is not more complex than the full timed opacity problem, and then we propose an algorithm, implemented and evaluated in practice.