Access control policies are often specified in declarative languages. In this paper, we propose a novel approach, called mutation verification, to assess the quality of properties specified for a policy and, in doing so, the quality of the verification itself. In our approach, given a policy and a set of properties, we first mutate the policy to generate various mutant policies, each with a single seeded fault. We then verify whether the properties hold for each mutant policy. If the properties still hold for a given mutant policy, then the quality of these properties is determined to be insufficient in guarding against the seeded fault, indicating that more properties are needed to augment the existing set of properties to provide higher confidence of the policy correctness. We have implemented Mutaver, a mutation verification tool for XACML, and applied it to policies and properties from a real-world software system.

Access control is one of the most fundamental and widely used security mechanisms. Access control mechanisms control which principals such as users or processes have access to which resources in a system. To facilitate managing and maintaining access control, access control policies are increasingly written in specification languages such as XACML. The specification of access control policies itself is often a challenging problem. Furthermore, XACML is intentionally designed to be generic: it provides the freedom in describing access control policies, which are well-known or invented ones. But the flexibility and expressiveness provided by XACML come at the cost of complexity, verbosity, and lack of desirable-property enforcement. Often common properties for specific access control policies may not be satisfied when these policies are specified in XACML, causing the discrepancy between what the policy authors intend to specify and what the actually specified XACML policies reflect. In this position paper, we propose an approach for conducting conformance checking of access control policies specified in XACML based on existing verification and testing tools for XACML policies.

Web services are a popular way of implementing a Service-Oriented Architecture (SOA), which has gained rapid adoption and support from leading companies in industry. Testing can be used to help assure both the corectness and robustness of a web service. Because manual testing is tedious, tools are needed to automate test generation and execution for web services. This paper presents a framework and its supporting tool for automaically generating and executing web-service requests and analyzing the subsequent request-response pairs. Given a service provider's Web Service Description Language (WSDL) specification, we first automatically generate neessary Java code to implement a client (service requestor). We then leverage automated unit test generation tools for Java to generate unit tests (including extreme, special, and random input values), and execute the generated unit tests, which in turn invoke the service under test. Finally we an alyze the large number of request-response pairs from the web service invocation and identify robustness problems. We have applied our framework to freely available web services and our experiences show that we can quickly gen erate and execute web-service requests that may reveal robustness problems with no knowledge of the underlying web service implementation.

To increase confidence in the correctness of specified policies, policy developers can conduct policy testing by supplying typical test inputs (requests) and subsequently checking test outputs (responses) against expected ones. Unfortunately, manual testing is tedious and few tools exist for automated testing of access control policies. We present a fault model for access control policies and a framework to explore it. The framework includes mutation operators used to implement the fault model, mutant generation, equivalentmutant detection, and mutant-killing determination. This framework allows us to investigate our fault model, evaluate coverage criteria for test generation and selection, and determine a relationship between structural coverage and fault-detection effectiveness. We have implemented the framework and applied it to various policies written in XACML. Our experimental results offer valuable insights into choosing mutation operators in mutation testing and choosing coverage criteria in test generation and selection.

In software systems, different software applications often interact with each other through specific interfaces by exchanging data in string format. For example, web services interact with each other through XML strings. Database applications interact with a database through strings of SQL statements. Sometimes these interfaces between different software applications are complex and distributed. For example, a table in a database can be accessed by multiple methods in a database application and a single method can access multiple tables. In this paper, we propose an approach to understanding software application interfaces through string analysis. The approach first performs a static analysis of source code to identify interaction points (in the form of interface-method-call sites). We then leverage existing string analysis tools to collect all possible string data that can be sent through these different interaction points. Then we manipulate collected string data by grouping similar data together. For example, we group together all collected SQL statements that access the same table. Then we associate various parts of aggregated data with interaction points in order to show the connections between entities from interacting applications. Our preliminary results show that the approach can help us understand the characteristics of interactions between database applications and databases. We also identify some challenges in this approach for our future work.

An automatic test-generation tool can produce a large number of test inputs to exercise the class under test. However, without specifications, developers cannot inspect the execution of each automatically generated test input practically. To address the problem, we have developed an automatic test abstraction tool, called Abstra, to extract high level object-state-transition information from unit-test executions, without requiring a priori specifications. Given a class and a set of its generated test inputs, our tool extracts object state machines (OSM): a state in an OSM represents an object state of the class and a transition in an OSM represents method calls of the class. When an object state in an OSM is concrete (being represented by the values of all fields reachable from the object), the size of the OSM could be too large to be useful for inspection. To address this issue, we have developed techniques in the tool to abstract object states based on returns of observer methods, branch coverage of methods, and individual object fields, respectively. The tool provides useful object-state-transition information for programmers to inspect unit-test executions effectively. In particular, the tool helps facilitate correctness inspection, program understanding, fault isolation, and test characterization.