Towards unifying semantic constraints and security constraints in distributed information systems

Abstract

Modern information systems must respect certain restrictions in order to guarantee the proper and desired functionality. Semantic constraints help to prevent inconsistencies in the stored data resulting from faulty updates. Security constraints are to maintain integrity, secrecy and availability over updates and over queries. This thesis designs a unifying framework for the specification of semantic constraints and security constraints in information systems in order to study interactions between them. We consider an information system as a distributed, reactive system in which each actor and each object acts autonomously and concurrently. Actors gain knowledge by performing read operations on objects and they may update the content of an object by performing update operations. To execute read or update operations, actors need execute rights that can be granted or revoked by other actors.This view of an information system is captured in a computational model.In this model, we consider each component of the information system, actors as well as objects, uniformly as a sequential agent that performs operations autonomously and jointly with other sequential agents. Each agent is alliated with a set of local propositions and a set of local operations as well as with relations that capture the agent's knowledge and belief. An agent's knowledge is determined completely by its local state. Change in knowledge of an agent is due to operations performed by the agent. Interaction between knowledge and operations is captured by the requirement that the enabling and the effect of an operation is completely determined by the knowledge of the acting agents. Knowledge of agents can be changed only byoperations in which they participate. We define a temporal and epistemic specification language with temporaland epistemic operators. The logic provides for each agent local next and until operators as temporal operators and local knowledge and belief operators as epistemic operators. We develop a modal tableau based proof system for a subset of the logic and show its soundness. Completeness can be shown only for a smaller, but still reasonable subset of the logic, decidability remains an open question. The main diffculty of the tableau system arises from the interaction requirement between knowledge and action.In a detailed example we demonstrate how the framework can be used for specifying semantic constraints and security constraints in information systems.