TAKOS is the implementation of the theoretical results presented in our paper published in Discrete Dynamic Event Systems. TAKOS is dedicated to the validation 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. More specifically, this toolbox allows to synthesize monitors for the verification and enforcement, at system runtime, of several levels of opacity.
The main features offered by TAKOS are:
- to check offline (i.e., model-check) the opacity of a secret on a system,
- to synthesize a runtime verification monitor in order to check the opacity at system runtime, and
- to synthesize an enforcement monitor in order to ensure the opacity of a secret at system runtime.
See the figure below for an overview.
