Spotlight on Lablet Research #15 - Reasoning about Accidental and Malicious Misuse via Formal Methods
Spotlight on Lablet Research #15 -
Project: Reasoning about Accidental and Malicious Misuse via Formal Methods
Lablet: North Carolina State University
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.
Led by Principal Investigator (PI) Munindar Singh and Co-PIs William Enck and Laurie Williams, this research project deals with accidental and malicious misuse case discovery in sociotechnical systems. System misuse is conceptually a violation of a stakeholder's expectation of how a system should operate. Whereas existing tools make security decisions using the context of usage, including environment, time, and execution state, they lack an ability to reason about the underlying stakeholder expectations, which are often crucial to identifying misuses. The researchers believe that if existing tools making security decisions could reason about expectations, they could automatically prevent, discover, and mitigate misuse. Unfortunately, the automatic extraction of stakeholder expectations remains ineffective. This led the researchers to identify the following research questions: What are the key components of stakeholders' expectations, and how may they be represented computationally? How would we identify the relevant stakeholder expectations? In what ways can we employ reasoning about expectations to inform the specification of sociotechnical systems to promote security?
The NCSU research team has studied these research questions through case studies on mobile applications as a basis for studying accidental and malicious misuse in a practical setting. Through manual collection and examination of app reviews that describe spying activities with apps, they have determined the necessity of considering app reviews for identifying apps that can aid spying, either explicitly or through misuses. Specifically, they are concerned about intimate partner surveillance spying. Based on this understanding, they are developing a computational framework for spotting such apps, in which they first identify apps that can potentially be misused for spying based on their metadata (e.g., their descriptions and permissions), collect their reviews, and determine their spying capability based on user-reported stories.
The research team started building a computational framework which, by analyzing app reviews, identifies if that app facilitates spying activity; they then conducted a preliminary investigation to identify app reviews that were relevant to spying. They observed that relevant app reviews differ greatly in terms of the severity of the problem leading them to investigate how they can automatically determine the severity of the app's spying capability described in an app review. They are designing an annotation scheme for crowdsourcing the annotation of reviews based on their severity.
As part of their research, they performed a systematic analysis of the network protocol exchanges used by Payment Service Providers (PSPs), and, through formal modeling using the Tamarin Prover, identified four vulnerabilities in these Software Development Toolkits (SDKs) and demonstrated proof-of-concept exploits for four payment service providers. The vulnerabilities have been reported to the providers. The researchers continued the analysis of PSP Application Programming Interfaces (APIs), developing models for analyzing the security of code in SDKs. They also completed a systematic literature review of research works on mining threat intelligence from unstructured textual data.
The team extended their scope from spying to Unexpected Information Gathering (UIG) in mobile apps and identified 124 UIG-enabling apps from their current dataset of apps. They identified an additional 131 UIG-enabling apps in a snowball fashion.
Healthcare professionals use mobile apps to store patient information and communicate with their patients, but not all such apps are HIPAA compliant. The NCSU team began investigating HIPAA compliance of medical mobile apps on the Apple App Store. In a preliminary investigation, they identified 899 medical apps that were potentially relevant but did not mention HIPAA compliance in their descriptions, and they are investigating these 899 medical apps further to determine their compliance with HIPAA.
Background on this project can be found here.