Welcome to TAKOS !

image post

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.

Last Update


Current TAKOS Version