TAKOS stands for Java Toolbox for Analyzing the K-Opacity of Systems. TAKOS is the implementation of the theoretical results presented in RR-7349 dedicated to the validation of several levels of opacity on systems. Opacity means the impossibility for an attacker to retrieve the value of a secret in a system of interest. Roughly speaking, ensuring opacity provides confidentiality of a secret on the system that must not leak to an attacker. Besides additional features, with TAKOS the user is able to: (i) to check offline (i.e. model-check) the opacity of a secret on a system, (ii) to synthesize a runtime verification monitor in order to check the opacity at system runtime, (iii) and to synthesize an enforcement monitor in order to ensure the opacity of a secret at system runtime.

References in zbMATH (referenced in 1 article )

Showing result 1 of 1.
Sorted by year (citations)

  1. Falcone, Yliès; Marchand, Hervé: Enforcement and validation (at runtime) of various notions of opacity (2015)