Visible to the public Reasoning about Accidental and Malicious Misuse via Formal MethodsConflict Detection Enabled

Submitted by najmeri on Tue, 06/23/2020 - 2:32pm

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

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

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 conducted a preliminary investigation in which we identified app reviews that were relevant to spying (binary classification). We found that relevant app reviews differ greatly in terms of the severity of the problem leading us to investigate how we can automatically determine the severity of the app's spying capability described in an app review.

  • We performed a systematic analysis of the network protocol exchanges used by Payment Service Providers (PSPs). We identified and generalized the protocol exchanges into generic classes, formally modeling them using the Tamarin Prover. Using Tamarin, we identified generalized vulnerabilities in the protocol classes and created proof-of-concept exploits for several PSPs. The work is currently under submission.

COMMUNITY ENGAGEMENTS

EDUCATIONAL ADVANCES:

Groups: