Verification of temporal-epistemic properties of access control systems

Koleini, Masoud (2012). Verification of temporal-epistemic properties of access control systems. University of Birmingham. Ph.D.

Preview

Koleini12PhD.pdf
PDF
Download (1MB)

Abstract

Verification of access control systems against vulnerabilities has always been a challenging problem in the world of computer security. The complication of security policies in large- scale multi-agent systems increases the possible existence of vulnerabilities as a result of mistakes in policy definition. This thesis explores automated methods in order to verify temporal and epistemic properties of access control systems. While temporal property verification can reveal a considerable number of security holes, verification of epistemic properties in multi-agent systems enable us to infer about agents' knowledge in the system and hence, to detect unauthorized information flow. This thesis first presents a framework for knowledge-based verification of dynamic access control policies. This framework models a coalition-based system, which evaluates if a property or a goal can be achieved by a coalition of agents restricted by a set of permissions defined in the policy. Knowledge is restricted to the information that agents can acquire by reading system information in order to increase time and memory efficiency. The framework has its own model-checking method and is implemented in Java and released as an open source tool named \(\char{cmmi10}{0x50}\)\(\char{cmmi10}{0x6f}\)\(\char{cmmi10}{0x6c}\)\(\char{cmmi10}{0x69}\)\(\char{cmmi10}{0x56}\)\(\char{cmmi10}{0x65}\)\(\char{cmmi10}{0x72}\). In order to detect information leakage as a result of reasoning, the second part of this thesis presents a complimentary technique that evaluates access control policies over temporal-epistemic properties where the knowledge is gained by reasoning. We will demonstrate several case studies for a subset of properties that deal with reasoning about knowledge. To increase the efficiency, we develop an automated abstraction refinement technique for evaluating temporal-epistemic properties. For the last part of the thesis, we develop a sound and complete algorithm in order to identify information leakage in Datalog-based trust management systems.

Type of Work:

Thesis (Doctorates > Ph.D.)

Award Type:

Doctorates > Ph.D.

Supervisor(s):