Formal Specification and Analysis of Security-Critical Norms and Policies - July 2015

Public Audience
Purpose: To highlight project progress. Information is generally at a higher level which is accessible to the interested public. All information contained in the report (regions 1-3) is a Government Deliverable/CDRL.

PI(s):  Rada Chirkova, Jon Doyle, Munindar Singh
Researchers:  Bennett Y. Narron, Vaira Selvakani, Nirav Ajmeri

HARD PROBLEM(S) ADDRESSED

• Policy-Governed Secure Collaboration - This project addresses how to specify and analyze norms (standards of correct collaborative behavior) and policies (ways of achieving different collaborative behaviors) to determine important properties, such as their mutual consistency.
• Scalability and Composability - This project can facilitate the composition of new collaborative systems by combining sets of norms and policies, and verifying whether such combinations satisfy desired properties.

PUBLICATIONS
Report papers written as a results of this research. If accepted by or submitted to a journal, which journal. If presented at a conference, which conference.

ACCOMPLISHMENT HIGHLIGHTS

• We have developed a formal model for conditional norms that includes a model of branching time and relates norms to primitives used for declarative information stores. This model provides a basis for deciding when a norm is satisfied or violated. In this manner, it supports an approach for model checking norms with respect to enactments of a system. In addition, it provides a basis for determining the consistency or otherwise of a set of norms.
• This model prepares us to study norm conflicts. Specifically, we are considering approaches to express situational preferences between norms so that the most preferred norms can be satisfied when they conflict with less preferred norms.
• We are investigating versions of the above setting that can be addressed via existing reasoning tools.