TAKOS: a Toolbox for Opacity

TAKOS stands for Toolbox for Analyzing the K-Opacity of Systems. TAKOS is the Java implementation of the theoretical results presented in [FM10] dedicated to the validation of several levels of opacity on systems..

Following the methodology introduced in [FM10], users of TAKOS can put into practice the validation of opacity, as it is described in the Figure above. Besides additional features, with TAKOS a user is able to:

1. to check offline (i.e., model-check) the opacity of a secret on a system (Fig. a),
2. to synthesize a runtime verification monitor in order to check online the opacity at system runtime (Fig. b),
3. and to synthesize an enforcement monitor in order to ensure the opacity of a secret at system runtime (Fig. c).

One may consult the dedicated website for more information on TAKOS.