Visible to the public Usable Formal Methods for the Design and Composition of Security and Privacy Policies (CMU/UTSA Collaborative Proposal) - October 2015Conflict Detection Enabled

Submitted by Jamie Presken on Thu, 09/17/2015 - 7:30am

Public Audience
Purpose: To highlight progress. Information is generally at a higher level which is accessible to the interested public.

PI(s): Travis Breaux (CMU), Jianwei Niu (UTSA)
Researchers:

1) HARD PROBLEM(S) ADDRESSED (with short descriptions)

This refers to Hard Problems, released November 2012.

Security-Metrics-Driven-Evaluation, Design, Development and Deployment. Our research evaluates how designers select and apply security patterns in response to attack patterns. The evaluation is based on metrics embodied in formal models of attack scenarios that will be used to measure security risk and promote risk reduction strategies based on assurance cases constructed by the analyst.

Understanding and Accounting for Human Behavior. Our research applies theory from psychology concerning how designers comprehend and interpret their environment, how they plan and project software-based solutions into the future, with the aim of better understanding how these activities exist in designing more secure systems. These are not typical models of attackers and defenders, but models of developer behavior, including our ability to influence that behavior with tool-based interventions.

2) 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.

  1. T. MacGahan, C. Johnson, A. L. Rodriguez, M. Appleby, J. Niu, J. von Ronne. "Towards Verified Privacy Policy Compliance of an Actor-based Electronic Medical Record Systems", extended abstract accepted to ACM SIGPLAN workshop AGERE! 2015.
  2. J. Shahen, J. Niu, M. Tripunitara. "Mohawk+T: Efficient Analysis of Administrative Temporal Role-Based Access Control (ATRBAC) Policies," To Appear: 20th ACM Symposium on Access Control Models and Technologies (SACMAT), pp. 15-26, June 2015.
  3. H. Hibshi, T. D. Breaux, S. B. Broomell, "Assessment of Risk Perception in Security Requirements Composition." To Appear: IEEE 23rd International Requirements Engineering Conference (RE'15), 2015.
  4. T. D. Breaux, D. Smullen, H. Hibshi. "Detecting Repurposing and Over-collection in Multi-Party Privacy Requirements Specifications." To Appear: IEEE 23rd International Requirements Engineering Conference (RE'15), Ottawa, Canada, Sep. 2015.
  5. Hui Shen, Ram Krishnan, Rocky Slavin, and Jianwei Niu. "Sequence Diagram Aided Privacy Policy Specification", Accept To: IEEE Transactions on Dependable and Secure Computing, Fall 2014.
  6. H. Hibshi, T. Breaux, M. Riaz, L. Williams. "Discovering Decision-Making Patterns for Security Novices and Experts", In Submission: IEEE Symposium on Security and Privacy, 2015.
  7. H. Hibshi, T. Breaux, M. Riaz, L. Williams. "A Framework to Measure Experts' Decision Making in Security Requirements Analysis," IEEE 1st International Workshop on Evolving Security and Privacy Requirements Engineering, pp. 13-18, 2014.
  8. R. Slavin, J.-M. Lehker, J. Niu, T. Breaux. "Managing Security Requirement Patterns Using Feature Diagram Hierarchies," IEEE 22nd International Requirements Engineering Conference, pp. 193-202, 2014.
  9. Slankas, J., Riaz, M. King, J., Williams, L. "Discovering Security Requirements from Natural Language," IEEE 22nd International Requirements Engineering Conference, 2014.
  10. Rao, H. Hibshi, T. Breaux, J-M. Lehker, J. Niu, "Less is More? Investigating the Role of Examples in Security Studies using Analogical Transfer," 2014 Symposium and Bootcamp on the Science of Security (HotSoS), Article 7.
  11. H. Hibshi, R. Slavin, J. Niu, T. Breaux, "Rethinking Security Requirements in RE Research," University of Texas at San Antonio, Technical Report #CS-TR-2014-001, January, 2014
  12. Riaz, M., Breaux, T., Williams, L. "On the Design of Empirical Studies to Evaluate Software Patterns: A Survey," Revision submitted for consideration: Information and Software Technology, 2014
  13. Breaux, T., Hibshi, H., Rao, A., Lehker, J.-M. "Towards a Framework for Pattern Experimentation: Understanding empirical validity in requirements engineering patterns." IEEE 2nd Workshop on Requirements Engineering Patterns (RePa'12), Chicago, Illinois, Sep. 2012, pp. 41-47.
  14. Slavin, R., Shen, H., Niu, J., "Characterizations and Boundaries of Security Requirements Patterns," IEEE 2nd Workshop on Requirements Engineering Patterns (RePa'12), Chicago, Illinois, Sep. 2012, pp. 48-53.

3) KEY HIGHLIGHTS

When software developers reuse existing libraries, frameworks, platforms or services, they often cannot assess the security requirements satisfied by those third-party programs. We developed techniques for expressing data flow requirements and checking whether these flows preserve the use and collection limitation principles from international privacy standards. The approach is based on Description Logic and supports verification across requirements compositions, which occur when mobile apps are run on mobile devices or other platforms, or when software employs remote services for storage, authentication, etc. The results will appear in the proceedings of the 23rd IEEE International Requirements Engineering Conference, and the source code and a demonstration have been made available online.

T. D. Breaux, D. Smullen, H. Hibshi. "Detecting Repurposing and Over-collection in Multi-Party Privacy Requirements Specifications." To Appear: IEEE 23rd International Requirements Engineering Conference, Ottawa, Canada, Sep. 2015.

Codifying privacy regulations to be consistent with the their high-level intuition can be difficult for security architects or application domain experts of information systems. We provide a formal framework to use UML sequence diagrams as a practical means to graphically express privacy regulations and policies to enable domain experts to verify and confirm the codification is valid. Once intuitively confirmed, our framework introduces an algorithmic approach to formalizing the semantics of sequence diagrams in terms of linear temporal logic (LTL) templates. In all the templates, different semantic aspects are expressed as separate, yet simple LTL formulas that can be composed to define the complex semantics of sequence diagrams. We leverage the analytical powers of automated decision procedures for LTL formulas to determine if a collection of sequence diagrams is consistent, and independent and also to verify if a system design conforms to the privacy policies. This work will appear in IEEE Transactions on Dependable and Secure Computing in 2015.

Hui Shen, Ram Krishnan, Rocky Slavin, and Jianwei Niu. "Sequence Diagrams Aided Privacy Policy Specification". To appear: IEEE Transactions on Dependable and Secure Computing (TDSC), 14 pages, 2015.

Security is based on defense-in-depth, which requires the satisfaction of multiple security requirements to mitigate security threats. However, the prevailing mechanism for information assurance is based on checklists, which assume a single threat context (often the union of all possible threats and mitigations). We developed a technique to measure the impact of composing security requirements on perceived security risk in the presence of changing threats. The technique is based on multi-level modeling, a statistical technique that can measure the correlation of multiple factors on a dependent variable, such as risk perception. As we scale this approach to an increasing number of threats, the results can be used to propose a minimal set of security requirements likely believed to mitigate the most relevant threats. The results will appear in the proceedings of the 23rd IEEE International Requirements Engineering

H. Hibshi, T. D. Breaux, S. B. Broomell, "Assessment of Risk Perception in Security Requirements Composition." To Appear: IEEE 23rd International Requirements Engineering Conference, 2015.

Groups: