Reasoning about Accidental and Malicious Misuse via Formal Methods

PI(s), Co-PI(s), Researchers:

PI: Munindar Singh; Co-PIs: William Enck, Laurie Williams; Researchers: Vaibhav Garg, Hui Guo, Samin Yaseer Mahmud, Md Rayhanur Rahman

HARD PROBLEM(S) ADDRESSED
This refers to Hard Problems, released November 2012.

• Policy

This project seeks to aid security analysts in identifying and protecting against accidental and malicious actions by users or software through automated reasoning on unified representations of user expectations and software implementations to identify misuses sensitive to usage and machine context.

PUBLICATIONS

KEY HIGHLIGHTS

Each effort should submit one or two specific highlights. Each item should include a paragraph or two along with a citation if available. Write as if for the general reader of IEEE S&P.
The purpose of the highlights is to give our immediate sponsors a body of evidence that the funding they are providing (in the framework of the SoS lablet model) is delivering results that "more than justify" the investment they are making.

We identified a set of 13 security requirements to detect ways in which Android applications can misuse Payment Service Provider (PSP) SDKs

We conducted an empirical study to evaluate our Ember framework, an automated approach to suggest actions mitigating HIPAA violations for an input breach description. Through this study, we are examining (1) Ember's action extraction performance in comparison to human annotators and (2) how relevant the suggested actions are to the input breach descriptions.

We revised the iRogue paper to explain the differences between IPS and rogue apps, and stress the importance of the alarmingness score in our approach. We have prepared a list of 239 developers whose apps still contain rogue functionalities to serve as a basis for a further study.

COMMUNITY ENGAGEMENTS

None.

EDUCATIONAL ADVANCES:

We involved one female graduate student in our research this quarter.