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.
Current TAKOS Version