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

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)

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.


N/A this quarter


Mobile applications frequently access sensitive personal information to meet user or business requirements. Because this information is sensitive, regulators increasingly require mobile app developers to publish privacy policies that describe what information is collected, for what purpose is the information used and with whom it is shared. Furthermore, regulators have fined companies when these policies are inconsistent with the actual data practices of mobile apps. To help app developers check their privacy policies against their apps for consistency, we propose a semi-automated framework that consists of a policy terminology-API map that links policy phrases to API functions that process sensitive information, and information flow analysis to detect misalignments. We present our results from a collection of API to policy phrase mappings followed by a case study of 501 top Android apps that discovered 63 potential privacy policy violations.

R. Slavin, X. Wang, M.B. Hosseini, W. Hester, R. Krishnan, J. Bhatia, T.D. Breaux, J. Niu. "Toward a Framework for Detecting Privacy Policy Violation in Android Application Code," ACM/IEEE 38th International Software Engineering Conference, Austin, Texas, 2016, pp. 25-36.

4) COMMUNITY ENGAGEMENTS (if applicable)

CMU and UTSA published a website and developer tools for mobile app developers and regulators to help detect and repair potential privacy violations in mobile app source code. The website is located:

5) EDUCATIONAL ADVANCES (if applicable)

N/A this quarter