Research Projects

  1. Mobile Privacy Policy Analysis and Compliance

    The advent of mobile phones has created a major data revolution. Mobile apps running on these phones are increasingly prevalent as they provide tailored, user-friendly services such as shopping, instant messaging, travel, and gaming in context and on-demand. To meet user needs and provide value, these services heavily depend on collecting and sharing sensitive personal information, such as user location, contact lists, and app usage patterns. This research will develop a novel, multidisciplinary framework to ensure that the collection, sharing, and retention of sensitive personal information performed by mobile apps complies with privacy policies. We map the relationship between privacy policies expressed in natural language and privacy-related functions implemented in the corresponding code. This mapping will provide the semantics needed to check code for misalignment with privacy policy, and to suggest where policy may be changed to fit the functional requirements of apps. Moreover, more precise and accurate privacy specification can be generated from source code based on results from our approach.

    This project has been funded by National Security Agency grant "CMU Science of Security: Composability and Usability", UTSA subaward amount $220,000, March 2014 - March 2017, UTSA PI, Jianwei Niu, PI, Travis Breaux (CMU).

  2. Healthcare Privacy Policy Analysis and Enforcement

    This research project will develop a methodology for ensuring that information systems comply with privacy policies. Information systems that handle personal information must adhere to legal regulations, corporate privacy policies, and contractual agreements designed to protect personal privacy in many sectors, including medical, governmental, and financial. The immediate focus of the project will be on the needs of the medical industry. As medical practice transitions to electronic medical records held in information systems, there is an acute need of a capability to verify that these systems comply with applicable privacy policies. The project will provide such a capability by creating a software development framework that uses novel techniques to provide assurance that software developed using the framework complies with formally-specified privacy policies that identify circumstances under which information can be shared and circumstances in which such sharing incurs certain future obligations. The framework will include policy analysis tools, a programming language, program analysis tools, and a runtime environment. These components will be able to be used in concert to produce distributed information systems and formally verify that the resulting systems handle personal information according to applicable policies.

    This project has been funded by National Science Foundation grant CNS-0964710, "TC: Medium: Privacy and Declassification Policy Enforcement Framework", total award amount $1,162,668, September 2011 - June 2016, PI, Jianwei Niu, Co-PI, Jeffery von Ronne. (July 2010 - August 2011, PI, William Winsborough)

  3. Security Requirement Pattern

    Secure software depends upon the ability of software developers to respond to security risks early in the software development process. Despite a wealth of security requirements, often called security controls, there is a shortfall in the adoption and implementation of these requirements. This shortfall is due to the extensive expertise and higher level cognitive skillsets required to comprehend, decompose and reassemble security requirements concepts in the context of an emerging system design. To address this shortfall, we propose to develop two empirical methods: (1) a method to derive security requirements patterns from requirements catalogues using expert knowledge; and (2) a method to empirically evaluate these patterns for their "usability" by novice software developers against a set of common problem descriptions, including the developer's ability to formulate problems, select and instantiate patterns. The study results will yield a framework for discovering and evaluating security requirements patterns and new scientific knowledge about the limitations of pattern-based approaches when applied by novice software developers.

    This project has been funded by National Security Agency grant "Improving the Usability of Security Requirements by Software Developers through Empirical Studies and Analysis", UTSA award amount $200,000, February 2012 - September 2014, UTSA PI, Jianwei Niu, PIs, Travis Breaux (CMU) and Laurie Williams (NCSU).

  4. Trust Management Policy Analysis

    The overarching goal of this project is to design and develop support for access control systems that are scalable and decentralized. Classical access control systems were monolithic and designed for use within a single organization in which goals were uniform and aligned with the organization's mission. With the advent of extensive collaboration and resource sharing across organizations have come access control policies that are not specified by a single entity or with a unique entity's security objectives in mind. Such policies can be very difficult to understand and define correctly. At the same time, the rate at which policies must be designed and reconfigured increases, as collaborations come and go more and more rapidly. This NHARP funded project has made contributions in several areas related to managing the resulting complexity. These include: designing systems with simple, easy to understand features; tools that leverage formal methods (including model checking and classical strategies for mitigating state-space explosion, such as reduction and abstraction) for the purpose of understanding whether an individual stakeholder's security objectives are met by the policy as a whole, as well as gaining insight about how to correct the problem when they are not; and experience with the implementation and performance analysis of policy decision engines.

    This project has been supported by Texas Higher Education Coordinating Board, ARP grant 010115-0037-2007, "Formal Methods in Access Control Policy Analysis and Design", May 2008 - January 2011, total award amount $145,999, PI, Jianwei Niu, Co-PI, William H. Winsborough.

  5. Information Sharing Policy Design and Enforcement

    The central objective of this project is to design a formal group-oriented access control environment (GoAce) to protect the confidentiality of resources, yet to facilitate the efficient and rigorous management of shared information. The need to share information while confining what an authorized recipient can do with that information is one of the oldest and most challenging problems in Access Control. Because of the dynamic nature of scenarios in which secure information sharing is desirable, authorization systems need to minimize the administrative efforts required both to establish information-sharing infrastructure, and to modify the users who have access and the information to which they have access. This project has contributed to the development of a group-centric secure information sharing (g-SIS) system. Authorization in g-SIS policy is defined by bringing users and information objects together in a group to facilitate agile sharing. Information can be brought in from external sources and new information can be created within the group by group members. The project also introduced stale safety in the design of enforcement mechanisms. Addiontionally, the small finite policy and enforcement specifications concerning one user and one object of one group---called small models---is verified to satisfy the security objectives, and policy specifications together with stale safeties, respectively, by using model checking. Then the verification results of the small models can be generalized to large policy and enforcement specifications, comprising an unbounded number of users and data, by using manu proofs.

    This project has been supported by the University of Texas at San Antonio, Tenure-Track Research Award Competition (TRAC), "Formal Analysis of Secure Information Sharing", November 2008 - August 2009, total award amount $22,000. PI, Jianwei Niu.

  6. Scenario-Based Modeling

    The objective of this work is to develop a logical framework to structure the semantics of UML sequence diagram, providing software engineers the ability to generate models that are suitable for verification. Sequence diagrams describe scenarios as the interactions among a system's objects. Users often construct multiple sequence diagrams that are complementary perspectives of a single system. However, the semantics of the sequence diagram, in particular, its control constructs (e.g., combined fragments), is not formally defined when compared to its precise syntax description. Instead, UML sequence diagram leaves aspects of the semantics open for interpretation for each application domain. The lack of a fully defined semantics makes it extremely difficult to determine whether a collection of sequence diagrams constitutes a correct, consistent specification. The contributions of this research work include: leveraging linear temporal logic (LTL) to represent the semantics of a sequence diagram to gain better theoretical understanding of it, enabling a user to express certain properties using sequence diagrams, and providing a user the ability to employ auto means, such as model checking, to check sequence diagrams.

    This project has been supported in part by an award from Microsoft Inc., "VSX: Scenario-Based Model-Driven Engineering Framework", July 2007- July 2008, total award amount $15,000, PI, Jianwei Niu.