ACG

Keeping Secrets in Resource Aware Components

This talk will describe one of the analysis tools that we have been developing for the Trust4all project. It is an extension of the work on Q-automata that has previously been at an AGC talk. Members of SEN2 have helped implement some of this work in mCRL.

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 mCRL process algebraic verification toolset.

Other presentations

Analysing the MUTE Anonymous File-Sharing System Using the Pi-calculus

Published: di 05 september 2006
By Tom Chothia (CWI)

In presentations.

We give details of a formal analysis of the MUTE system for anonymous file-sharing. We build pi-calculus models of a node that is innocent of sharing files, a node that is guilty of file-sharing and of the network environment. We then test to see if an attacker can distinguish between …
read more
Q Automata: Modelling the Resource Usage of Concurrent Components

Published: do 24 augustus 2006
By Tom Chothia (CWI)

In presentations.

This is mainly a practice talk for a presentation I will give at the FOCLASA workshop the week after next, with the follow abstract:

We introduce Q-automata to model quality aspects of component-based software. We propose Q-algebras as a general framework that allows us to combine and choose between quality …
read more
Type-based access control: for distributed systems, for components and under attack

Published: di 18 april 2006
By Tom Chothia (CWI)

In presentations.

This talk will cover some of my previous work that may now be applicable to the Trust4all project. I will start with an overview of some type-based information flow work, including the "decentralised label model" of Myers and Liskov and the JIF programming language. I will then show how local …
read more

Page 1 / 1