Visible to the public Formal Specification and Analysis of Security-Critical Norms and Policies - January 2016Conflict Detection Enabled

Submitted by drwright on Tue, 12/01/2015 - 3:09pm

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 Y. Chirkova, Jon Doyle, Munindar P. Singh
Researchers:  Nirav Ajmeri, Jiaming Jiang, Ozgur Kafali

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.

Amit K. Chopra and Munindar P. Singh. “From Social Machines to Social Protocols: Software Engineering Foundations for Sociotechnical Systems.” In: Proceedings of the 25th International World Wide Web Conference. Montreal: ACM, April 2016. To appear.

ACCOMPLISHMENT HIGHLIGHTS

  • We further extended Vitesse, our structured norm compliance framework, by refining its formal syntax and semantics. Vitesse can represent and reason about conflicts and dominance between conditional, directed norms. It  tackles important use cases of norms, for instance, in healthcare, by addressing scenarios in which norms conflict and what norm dominates another depends upon the situation.
  • We have developed a modeling language and tool for Vitesse, and have demonstrated its value on a healthcare scenario. This tool incorporates an implementation of Vitesse that uses logical inference to identify which norms govern each agent at each instant.
  • We developed a framework called CoNTraST that provides a principled approach for computing tradeoffs between liveness and safety properties in order to (i) understand whether an STS specification provides more liveness or safety than another STS specification, (ii) quantify the level of liveness or safety an STS specification provides, and (iii) revise an STS specification so that liveness or safety is improved.
  • We developed a formulation for social machines as social protocols based on norms that captures their sociotechnical nature. This formulation relates the collaboration that social machines support with our normative understanding of accountability and provides a basis for requirements engineering for STSs that support secure collaboration.
Groups: