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).
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)
Security Requirement PatternSecure 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).
Trust Management Policy AnalysisThe 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.
Information Sharing Policy Design and EnforcementThe 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.
Scenario-Based ModelingThe 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.