Keeping Secrets in Resource Aware Components

We present a powerful and flexible method for automatically checking the secrecy of values inside components. In our framework an attacker may monitor the external communication of a component, interact with it and monitor the components resource usage. We use an automata model of components in which each transition is tagged with resource usage information. We extend these automata to pass values and say that a value is kept secret if the observable behaviour of the automata is the same for all possible instantiations of that value. If a component leaks some, but not all of the information about its secret we use a notion of secrecy degree to quantify the worst-case leakage. We show how this secrecy degree can be automatically calculated, for values from a finite domain, using the μCRL process algebraic verification toolset.