Shapley values have emerged as a critical tool for explaining which features impact the decisions made by machine learning models. However, computing exact Shapley values is difficult, generally requiring an exponential (in the feature dimension) number of model evaluations. To address this, many model-agnostic randomized estimators have been developed, the most influential and widely used being the KernelSHAP method (Lundberg & Lee, 2017). While related estimators such as unbiased KernelSHAP (Covert & Lee, 2021) and LeverageSHAP (Musco & Witter, 2025) are known to satisfy theoretical guarantees, bounds for KernelSHAP have remained elusive. We describe a broad and unified framework that encompasses KernelSHAP and related estimators constructed using both with and without replacement sampling strategies. We then prove strong non-asymptotic theoretical guarantees that apply to all estimators from our framework. This provides, to the best of our knowledge, the first theoretical guarantees for KernelSHAP and sheds further light on tradeoffs between existing estimators. Through comprehensive benchmarking on small and medium dimensional datasets for Decision-Tree models, we validate our approach against exact Shapley values, consistently achieving low mean squared error with modest sample sizes. Furthermore, we make specific implementation improvements to enable scalability of our methods to high-dimensional datasets. Our methods, tested on datasets such MNIST and CIFAR10, provide consistently better results compared to the KernelSHAP library.

We study quantum algorithms based on quantum (sub)gradient estimation using noisy function evaluation oracles, and demonstrate the first dimension-independent query complexities (up to poly-logarithmic factors) for zeroth-order convex optimization in both smooth and nonsmooth settings. Interestingly, only using noisy function evaluation oracles, we match the first-order query complexities of classical gradient descent, thereby exhibiting exponential separation between quantum and classical zeroth-order optimization. We then generalize these algorithms to work in non-Euclidean settings by using quantum (sub)gradient estimation to instantiate mirror descent and its variants, including dual averaging and mirror prox. By leveraging a connection between semidefinite programming and eigenvalue optimization, we use our quantum mirror descent method to give a new quantum algorithm for solving semidefinite programs, linear programs, and zero-sum games. We identify a parameter regime in which our zero-sum games algorithm is faster than any existing classical or quantum approach.

In recent years, immense progress have been made in quantum optimization techniques. In this position paper, we share our opinion on some of the challenges facing the quantum optimization community and highlight opportunities which we believe would benefit from increased attention of researchers.

Quantum Approximate Optimization Algorithm (QAOA) is one of the most promising quantum heuristics for combinatorial optimization. While QAOA has been shown to perform well on small-scale instances and to provide an asymptotic speedup over state-of-the-art classical algorithms for some problems, fault-tolerance is understood to be required to realize this speedup in practice. The low resource requirements of QAOA make it particularly suitable to benchmark on early fault-tolerant quantum computing (EFTQC) hardware. However, the performance of QAOA depends crucially on the choice of the free parameters in the circuit. The task of setting these parameters is complicated in the EFTQC era by the large overheads, which preclude extensive classical optimization. In this paper, we summarize recent advances in parameter setting in QAOA and show that these advancements make EFTQC experiments with QAOA practically viable.

The growing richness of large-scale datasets has been crucial in driving the rapid advancement and wide adoption of machine learning technologies. The massive collection and usage of data, however, pose an increasing risk for people’s private and sensitive information due to either inadvertent mishandling or malicious exploitation. Besides legislative solutions, many technical approaches have been proposed towards data privacy protection. However, they bear various limitations such as leading to degraded data availability and utility, or relying on heuristics and lacking solid theoretical bases. To overcome these limitations, we propose a formal information-theoretic definition for this utility-preserving privacy protection problem, and design a data-driven learnable data transformation framework that is capable of selectively suppressing sensitive attributes from target datasets while preserving the other useful attributes, regardless of whether or not they are known in advance or explicitly annotated for preservation. We provide rigorous theoretical analyses on the operational bounds for our framework, and carry out comprehensive experimental evaluations using datasets of a variety of modalities, including facial images, voice audio clips, and human activity motion sensor signals. Results demonstrate the effectiveness and generalizability of our method under various configurations on a multitude of tasks. Our source code is available at this URL.

Introducing additional tunable parameters to quantum circuits is a powerful way of improving per-formance without increasing hardware requirements. A recently introduced multiangle extension of the quantum approximate optimization algorithm (ma-QAOA) signifi-cantly improves the solution quality compared with QAOA by allowing the parameters for each term in the Hamilto-nian to vary independently. Prior results suggest, however, considerable redundancy in parameters, the removal of which would reduce the cost of parameter optimization. In this work we show numerically the connection between the problem symmetries and the parameter redundancy by demonstrating that symmetries can be used to reduce the number of parameters used by ma-QAOA without decreasing the solution quality. We study Max-Cut on all 7,565 connected, non-isomorphic 8-node graphs with a nontrivial symmetry group and show numerically that in 67.4% of these graphs, symmetry can be used to reduce the number of parameters with no decrease in the objective, with the average ratio of parameters reduced by 28.1%. Moreover, we show that in 35.9% of the graphs this reduction can be achieved by simply using the largest symmetry. For the graphs where reducing the number of parameters leads to a decrease in the objective, the largest symmetry can be used to reduce the parameter count by 37.1% at the cost of only a 6.1% decrease in the objective. We demonstrate the central role of symmetries by showing that a random parameter reduction strategy leads to much worse performance.

Quantum computers are expected to surpass the computational capabilities of classical computers during this decade, and achieve disruptive impact on numerous industry sectors, particularly finance. In fact, finance is estimated to be the first industry sector to benefit from Quantum Computing not only in the medium and long terms, but even in the short term. This review paper presents the state of the art of quantum algorithms for financial applications, with particular focus to those use cases that can be solved via Machine Learning.

Numerical optimization has been extensively used in many real-world applications related to Scientific Computing, Artificial Intelligence and, more recently, Quantum Computing. However, existing optimizers conduct their internal computations sequentially, which affects their performance. We observed a general pattern that enabled us to parallelize such internal computations and achieve significant speedup. We designed a novel parallelization algorithm for optimizers, which consists of pattern detection, prediction, precomputation, and caching. Importantly, our design does not require any change to the optimizers. Instead, it simply modifies the function to be optimized, thereby leading to several engineering advantages, including simplicity, modularity and portability. We implemented this solution and included it in the Qiskit Aqua open-source project. In this paper, we present an evaluation on both standard benchmarks and real-world quantum-computing applications. The evaluation results confirm that our approach (1) incurs negligible overhead, (2) effectively speeds up optimization, and (3) does not affect the accuracy of the results or the convergence of the optimizers.

Quantum computing has increasingly drawn interest and investments from the academic, industrial, and governmental research communities worldwide. Among quantum algorithms, Quantum Search is important for its quadratic speedup over its classical-computing counterpart. A key ingredient in its implementation is the Multi-Control Toffoli (MCT) gate, which creates a Boolean product of control variables and XORs it into the target. On an idealized quantum computer, all-to-all connectivity would eliminate the need to use SWAP gates to communicate information. This is, however, not affordable in the current Noisy Intermediate-Scale Quantum (NISQ) computing era. In this work, we discuss how to efficiently implement MCT gates on 2D Square Lattices (2DSL), suitable for superconducting circuits, by taking advantage of relative-phase Toffoli gates and H-tree layouts to drastically reduce resulting circuits' depths and the amount of SWAPping required.

Current state-of-the-art models for video action recognition are mostly based on expensive 3D ConvNets. This results in a need for large GPU clusters to train and evaluate such architectures. To address this problem, we present an lightweight and memory-friendly architecture for action recognition that performs on par with or better than current architectures by using only a fraction of resources. The proposed architecture is based on a combination of a deep subnet operating on low-resolution frames with a compact subnet operating on high-resolution frames, allowing for high efficiency and accuracy at the same time. We demonstrate that our approach achieves a reduction by 3~4 times in FLOPs and ~2 times in memory usage compared to the baseline. This enables training deeper models with more input frames under the same computational budget. To further obviate the need for large-scale 3D convolutions, a temporal aggregation module is proposed to model temporal dependencies in a video at very small additional computational costs. Our models achieve strong performance on several action recognition benchmarks including Kinetics, Something-Something and Moments-in-time. The code and models are available at \url{https://github.com/IBM/bLVNet-TAM}.

We propose sparse-complementary convolution (SC-Conv) to improve model utilization of convolution neural networks (CNNs). The networks with SC-Conv achieve better accuracy than the regular convolution under similar computations and parameters. The proposed SC-Conv is paired with two deterministic sparse kernels, and one of kernels is complementary to the other one at in either spatial or channel domain or both; the deterministic sparsity increases the computational speed theoretically and practically; furthermore, by having the complementary characteristic, SC-Conv retains the same receptive field to the conventional convolution. This insightful but straightforward SC-Conv reuses of modern network architectures (ResNet and DenseNet), and at the same FLOPs and parameters, SC-Conv improves top-1 classification accuracy on ImageNet by 0.6 points for ResNet-101 and keep the same model complexity. Furthermore, SC-Conv also outperforms recent sparse networks by 1.3 points at top-1 accuracy for ImageNet, and after integrating SC-Conv with the sparse network, we further improve another 1.8 points accuracy at similar FLOPs and parameters.

Many designs have been proposed to improve the automated mobile testing. Despite these improvements, providing appropriate text inputs remains a prominent obstacle, which hinders the large-scale adoption of automated testing approaches. The key challenge is how to automatically produce the most relevant text in a use case context. For example, a valid website address should be entered in the address bar of a mobile browser app to continue the testing of the app, a singer's name should be entered in the search bar of a music recommendation app. Without the proper text inputs, the testing would get stuck. We propose a novel deep learning based approach to address the challenge, which reduces the problem to a minimization problem. Another challenge is how to make the approach generally applicable to both the trained apps and the untrained apps. We leverage the Word2Vec model to address the challenge. We have built our approaches as a tool and evaluated it with 50 iOS mobile apps including Firefox and Wikipedia. The results show that our approach significantly outperforms existing automatic text input generation methods.

User Interface/eXperience (UI/UX) significantly affects the lifetime of any software program, particularly mobile apps. A bad UX can undermine the success of a mobile app even if that app enables sophisticated capabilities. A good UX, however, needs to be supported of a highly functional and user friendly UI design. In spite of the importance of building mobile apps based on solid UI designs, UI discrepancies---inconsistencies between UI design and implementation---are among the most numerous and expensive defects encountered during testing. This paper presents UI X-Ray, an interactive UI testing system that integrates computer-vision methods to facilitate the correction of UI discrepancies---such as inconsistent positions, sizes and colors of objects and fonts. Using UI X-Ray does not require any programming experience; therefore, UI X-Ray can be used even by non-programmers---particularly designers---which significantly reduces the overhead involved in writing tests. With the feature of interactive interface, UI testers can quickly generate defect reports and revision instructions---which would otherwise be done manually. We verified our UI X-Ray on 4 developed mobile apps of which the entire development history was saved. UI X-Ray achieved a 99.03% true-positive rate, which significantly surpassed the 20.92% true-positive rate obtained via manual analysis. Furthermore, evaluating the results of our automated analysis can be completed quickly (< 1 minute per view on average) compared to hours of manual work required by UI testers. On the other hand, UI X-Ray received the appreciations from skilled designers and UI X-Ray improves their current work flow to generate UI defect reports and revision instructions. The proposed system, UI X-Ray, presented in this paper has recently become part of a commercial product.

Although Information Foraging Theory (IFT) research for desktop environments has provided important insights into numerous information foraging tasks, we have been unable to locate IFT research for mobile environments. Despite the limits of mobile platforms, mobile apps are increasingly serving functions that were once exclusively the territory of desktops - and as the complexity of mobile apps increases, so does the need for foraging. In this paper we investigate, through a theory-based, dual replication study, whether and how foraging results from a desktop IDE generalize to a functionally similar mobile IDE. Our results show ways prior foraging research results from desktop IDEs generalize to mobile IDEs and ways they do not, and point to challenging open research questions for foraging on mobile environments.

Mobile devices are rich in sensors, such as a Global Positioning System (GPS) tracker, microphone and camera, and have access to numerous sources of personal information, including the device ID, contacts and social data. This richness increases the functionality of mobile apps, but also creates privacy threats. As a result, different solutions have been proposed to verify or enforce privacy policies. A key limitation of existing approaches is that they reason about privacy at a coarse level, without accounting for declassification rules, such that the location for instance is treated as a single unit of information without reference to its many fields. As a result, legitimate app behaviors --- such as releasing the user's city rather than exact address --- are perceived as privacy violations, rendering existing analyses overly conservative and thus of limited usability.

Program analysis has become an essential tool to verify the correctness of programs before these are deployed to end users' computers and devices. Detecting security problems in today's mobile applications by just relying on manual code inspection is unrealistic. Testing is also limited because there is often no guarantee that all the possible paths of execution of an application are tested under all the possible inputs, and so false negatives may arise. Static analysis is a very promising solution but suffers from the dual problem of false positives. A combination of static and dynamic analysis mitigates the disadvantages that arise when static and dynamic analysis are executed individually and is, therefore, the recommended solution to detect and correct application-level cyber security attacks in mobile applications. This tutorial presents both static and dynamic analysis approaches to enforce privacy of mobile applications, and includes a hands-on lab that teaches the audience how to use create a static-analysis solution that verifies the integrity and confidentiality of the data managed by the program itself.

Modern software development and run-time environments, such as Java and the Microsoft .NET Common Language Runtime (CLR), have adopted a declarative form of access control. Permissions are granted to code providers, and during execution, the platform verifies compatibility between the permissions required by a security-sensitive operation and those granted to the executing code. While convenient, configuring the access-control policy of a program is not easy. If a code component is not granted sufficient permissions, authorization failures may occur. Thus, security administrators tend to define overly permissive policies, which violate the Principle of Least Privilege (PLP). A considerable body of research has been devoted to building program-analysis tools for computing the optimal policy for a program. However, Java and the CLR also allow executing code under the authority of a subject (user or service), and no program-analysis solution has addressed the challenges of determining the policy of a program in the presence of subjects. This paper introduces Subject Access Rights Analysis (SARA), a novel analysis algorithm for statically computing the permissions required by subjects at run time. We have applied SARA to 348 libraries in IBM WebSphere Application Server - a commercial enterprise application server written in Java that consists of >2 million lines of code and is required to support the Java permission- and subject-based security model. SARA detected 263 PLP violations, 219 cases of policies with missing permissions, and 29 bugs that led code to be unnecessarily executed under the authority of a subject. SARA corrected all these vulnerabilities automatically, and additionally synthesized fresh policies for all the libraries, with a false-positive rate of 5% and an average running time of 103 seconds per library. SARA also implements mechanisms for mitigating the risk of false negatives due to reflection and native code; according to a thorough result evaluation based on testing, no false negative was detected. SARA enabled IBM WebSphere Application Server to receive the Common Criteria for Information Technology Security Evaluation Assurance Level 4 certification.

A main aspect of the Android platform is Inter-Application Communication (IAC), which enables reuse of functionality across apps and app components via message passing. While a powerful feature, IAC also constitutes a serious attack surface. A malicious app can embed a payload into an IAC message, thereby driving the recipient app into a potentially vulnerable behavior if the message is processed without its fields first being sanitized or validated. We present what to our knowledge is the first comprehensive testing algorithm for Android IAC vulnerabilities. Toward this end, we first describe a catalog, stemming from our field experience, of 8 concrete vulnerability types that can potentially arise due to unsafe handling of incoming IAC messages. We then explain the main challenges that automated discovery of Android IAC vulnerabilities entails, including in particular path coverage and custom data fields, and present simple yet surprisingly effective solutions to these challenges. We have realized our testing approach as the IntentDroid system, which is available as a commercial cloud service. IntentDroid utilizes lightweight platform-level instrumentation, implemented via debug breakpoints (to run atop any Android device without any setup or customization), to recover IAC-relevant app-level behaviors. Evaluation of IntentDroid over a set of 80 top-popular apps has revealed a total 150 IAC vulnerabilities — some already fixed by the developers following our report — with a recall rate of 92% w.r.t. a ground truth established via manual auditing by a security expert.

Mobile devices have revolutionized many aspects of our lives. We use smartphones and tablets as portable computers and, often without realizing it, we run various types of security-sensitive programs on them, such as personal and enterprise email and instant-messaging applications, as well as social, banking, insurance and retail programs. These applications access and transmit over the network numerous pieces of private information, including our geographical location, device ID, contacts, calendar events, passwords, and health records, as well as credit-card, social-security, and bank-account numbers. Guaranteeing that no private information is exposed to unauthorized observers is very challenging given the level of complexity that these applications have reached. Furthermore, using program-analysis tools with out-of-the-box configurations in order to detect confidentiality violations may not yield the desired results because only a few pieces of private data, such as the device's ID and geographical location, are obtained from standard sources. The majority of confidentiality sources (such as credit-card and bank-account numbers) are application-specific and require careful configuration. This paper presents Labyrinth, a run-time privacy enforcement system that automatically detects leakage of private data originating from standard as well as application-specific sources. Labyrinth features several novel contributions: (i) it allows for visually configuring, directly atop the application's User Interface (UI), the fields that constitute custom sources of private data, (ii) it does not require operating-system instrumentation, but relies only an application-level instrumentation and on a proxy that intercepts the communication between the mobile device and the back-end servers, and (iii) it performs an enhanced form of value-similarity analysis to detect data leakage even when sensitive data (such as a password) has been encoded or hashed. Labyrinth supports both Android and iOS. We have evaluated Labyrinth experimentally, and in this paper we report results on production-level applications.

Given a program whose functionality depends on access to certain external resources, we investigate the question of how to gracefully degrade functionality when a subset of those resources is unavailable. The concrete setting motivating this problem statement is mobile applications, which rely on contextual data (e.g., device identifiers, user location and contacts, etc.) to fulfill their functionality. In particular, we focus on the Android platform, which mediates access to resources via an installation-time permission model. On the one hand, granting an app the permission to access a resource (e.g., the device ID) entails privacy threats (e.g., releasing the device ID to advertising servers). On the other hand, denying access to a resource could render the app useless (e.g., if inability to read the device ID is treated as an error state). Our goal is to specialize an existing Android app in such a way that it is disabled from accessing certain sensitive resources (or contextual data) as specified by the user, while still being able to execute functionality that does not depend on those resources. We present ShamDroid, a program transformation algorithm, based on specialized forms of program slicing, backwards static analysis and constraint solving, that enables the use of Android apps with partial permissions. We rigorously state the guarantees provided by ShamDroid w.r.t. functionality maximization. We provide an evaluation over the top 500 Google Play apps and report on an extensive comparative evaluation of ShamDroid against three other state-of-the-art solutions (APM, XPrivacy, and Google App Ops) that mediate resource access at the system (rather than app) level. ShamDroid performs better than all of these tools by a significant margin, leading to abnormal behavior in only 1 out of 27 apps we manually investigated, compared to the other solutions, which cause crashes and abnormalities in 9 or more of the apps. This demonstrates the importance of performing app-sensitive mocking.

The scale and complexity of modern software systems complicate manual security auditing. Automated analysis tools are gradually becoming a necessity. Specifically, static security analyses carry the promise of efficiently verifying large code bases. Yet, a critical usability barrier, hindering the adoption of static security analysis by developers, is the excess of false reports. Current tools do not offer the user any direct means of customizing or cleansing the report. The user is thus left to review hundreds, if not thousands, of potential warnings, and classify them as either actionable or spurious. This is both burdensome and error prone, leaving developers disenchanted by static security checkers.

This paper addresses the problem of detecting JavaScript security vulnerabilities in the client side of Web applications. Such vulnerabilities are becoming a source of growing concern due to the rapid migration of server-side business logic to the client side, combined with new JavaScript-backed Web technologies, such as AJAX and HTML5. Detection of client-side vulnerabilities is challenging given the dynamic and event-driven nature of JavaScript. We present a hybrid form of JavaScript analysis, which augments static analysis with (semi-)concrete information by applying partial evaluation to JavaScript functions according to dynamic data recorded by the Web crawler. The dynamic component rewrites the program per the enclosing HTML environment, and the static component then explores all possible behaviors of the partially evaluated program (while treating user-controlled aspects of the environment conservatively).

We propose a novel technique for statically verifying the strings generated by a program. The verification is conducted by encoding the program in Monadic Second-order Logic (M2L). We use M2L to describe constraints among program variables and to abstract built-in string operations. Once we encode a program in M2L, a theorem prover for M2L, such as MONA, can automatically check if a string generated by the program satisfies a given specification, and if not, exhibit a counterexample. With this approach, we can naturally encode relationships among strings, accounting also for cases in which a program manipulates strings using indices. In addition, our string analysis is path sensitive in that it accounts for the effects of string and Boolean comparisons, as well as regular-expression matches. We have implemented our string analysis algorithm, and used it to augment an industrial security analysis for Web applications by automatically detecting and verifying sanitizers —methods that eliminate malicious patterns from untrusted strings, making these strings safe to use in security-sensitive operations. On the 8 benchmarks we analyzed, our string analyzer discovered 128 previously unknown sanitizers, compared to 71 sanitizers detected by a previously presented string analysis.

In recent years, there has been significant interest in fault-localization techniques that are based on statistical analysis of program constructs executed by passing and failing executions. This paper shows how the Tarantula, Ochiai, and Jaccard fault-localization algorithms can be enhanced to localize faults effectively in web applications written in PHP by using an extended domain for conditional and function-call statements and by using a source mapping. We also propose several novel test-generation strategies that are geared toward producing test suites that have maximal fault-localization effectiveness. We implemented various fault-localization techniques and test-generation strategies in Apollo, and evaluated them on several open-source PHP applications. Our results indicate that a variant of the Ochiai algorithm that includes all our enhancements localizes 87.8 percent of all faults to within 1 percent of all executed statements, compared to only 37.4 percent for the unenhanced Ochiai algorithm. We also found that all the test-generation strategies that we considered are capable of generating test suites with maximal fault-localization effectiveness when given an infinite time budget for test generation. However, on average, a directed strategy based on path-constraint similarity achieves this maximal effectiveness after generating only 6.5 tests, compared to 46.8 tests for an undirected test-generation strategy.

Many enterprises perform data-center transformation, consolidation, and migration in order to improve the efficiency of their IT infrastructures. These transformation projects begin with the discovery of the existing infrastructure, in particular the dependencies between applications. These dependencies are needed in planning, in order to determine how components influence one another, and in relinking, so that the component names and addresses can be updated. Typically, dependency discovery is done by network monitoring and middleware configuration analysis. These existing approaches will often fail to detect dependencies expressed in the application code. In this paper, we present the first method and tool for automatically identifying code-embedded external dependencies in Java Enterprise Edition applications. In addition, our tool can automatically alter the application code to update the dependencies, or externalize them to configuration files. We analyzed over 1000 Java EE applications from three enterprise environments. The results demonstrate the prevalence of code-embedded dependencies that would otherwise have to be identified manually, often causing failures during user-acceptance testing.

JavaScript is the most popular client-side scripting language for Web applications. Exploitable JavaScript code exposes end users to integrity and confidentiality violations. Client-side vulnerabilities can cost an enterprise money and reputation, and cause serious damage to innocent users of the Web application. In spite of all this, recent research in the area of information-flow security has focused more on other languages that are more suitable for server-side programming, such as Java.

We propose a novel technique for statically verifying the strings generated by a program. The verification is conducted by encoding the program in Monadic Second-Order Logic (M2L). We use M2L to describe constraints among program variables and to abstract built-in string operations. Once we encode a program in M2L, a theorem prover for M2L, such as MONA, can automatically check if a string generated by the program satisfies a given specification, and if not, exhibit a counterexample. With this approach, we can naturally encode relationships among strings, accounting also for cases in which a program manipulates strings using indices. In addition, our string analysis is path sensitive in that it accounts for the effects of string and Boolean comparisons, as well as regular-expression matches.

This paper presents F4F (Framework For Frameworks), a system for effective taint analysis of framework-based web applications. Most modern web applications utilize one or more web frameworks, which provide useful abstractions for common functionality. Due to extensive use of reflective language constructs in framework implementations, existing static taint analyses are often ineffective when applied to framework-based applications. While previous work has included ad hoc support for certain framework constructs, adding support for a large number of frameworks in this manner does not scale from an engineering standpoint.

We leverage combined concrete and symbolic execution and several fault-localization techniques to create a uniquely powerful tool for localizing faults in PHP applications. The tool automatically generates tests that expose failures, and then automatically localizes the faults responsible for those failures, thus overcoming the limitation of previous fault-localization techniques that a test suite be available upfront. The fault-localization techniques we employ combine variations on the Tarantula algorithm with a technique based on maintaining a mapping between statements and the fragments of output they produce. We implemented these techniques in a tool called Apollo, and evaluated them by localizing 75 randomly selected faults that were exposed by automatically generated tests in four PHP applications. Our findings indicate that, using our best technique, 87.7% of the faults under consideration are localized to within 1% of all executed statements, which constitutes an almost five-fold improvement over the Tarantula algorithm.

Fault-localization techniques that apply statistical analyses to execution data gathered from multiple tests are quite effective when a large test suite is available. However, if no test suite is available, what is the best approach to generate one? This paper investigates the fault-localization effectiveness of test suites generated according to several test-generation techniques based on combined concrete and symbolic (concolic) execution. We evaluate these techniques by applying the Ochiai fault-localization technique to generated test suites in order to localize 35 faults in four PHP Web applications. Our results show that the test-generation techniques under consideration produce test suites with similar high fault-localization effectiveness, when given a large time budget. However, a new, "directed" test-generation technique, which aims to maximize the similarity between the path constraints of the generated tests and those of faulty executions, reaches this level of effectiveness with much smaller test suites. On average, when compared to test generation based on standard concolic execution techniques that aims to maximize code coverage, the new directed technique preserves fault-localization effectiveness while reducing test-suite size by 86.1% and test-suite generation time by 88.6%.

In modern software systems, programs are obtained by dynamically assembling components. This has made it necessary to subject component providers to access-control restrictions. What permissions should be granted to each component? Too few permissions may cause run-time authorization failures, too many constitute a security hole. We have designed and implemented a composite algorithm for precise static permission analysis for Java and the CLR. Unlike previous work, the analysis is modular and fully integrated with a novel slicing-based string analysis that is used to statically compute the string values defining a permission and disambiguate permission propagation paths. The results of our research prototype on production-level Java code support the effectiveness, practicality, and precision of our techniques, and show outstanding improvement over previous work.

Taint analysis, a form of information-flow analysis, establishes whether values from untrusted methods and parameters may flow into security-sensitive operations. Taint analysis can detect many common vulnerabilities in Web applications, and so has attracted much attention from both the research community and industry. However, most static taint-analysis tools do not address critical requirements for an industrial-strength tool. Specifically, an industrial-strength tool must scale to large industrial Web applications, model essential Web-application code artifacts, and generate consumable reports for a wide range of attack vectors.

We present a novel approach to client-side mining of temporal API specifications based on static analysis. Specifically, we present an interprocedural analysis over a combined domain that abstracts both aliasing and event sequences for individual objects. The analysis uses a new family of automata-based abstractions to represent unbounded event sequences, designed to disambiguate distinct usage patterns and merge similar usage patterns. Additionally, our approach includes an algorithm that summarizes abstract traces based on automata clusters, and effectively rules out spurious behaviors. We show experimental results mining specifications from a number of Java clients and APIs. The results indicate that effective static analysis for client-side mining requires fairly precise treatment of aliasing and abstract event sequences. Based on the results, we conclude that static client-side specification mining shows promise as a complement or alternative to dynamic approaches.

Given a large component-based program, it may be very complex to identify an optimal access-control policy, allowing the program to execute with no authorization failures and no violations of the principle of least privilege. This paper presents a novel combination of static and dynamic analysis for automatic determination of precise access-control policies for programs that will be executed on stack-based access control systems, such as Java and the Common Language Runtime (CLR). The static analysis soundly models the execution of the program taking into account native methods, reflection, and multi-threaded code. The dynamic analysis interactively refines the potentially conservative results of the static analysis, with no need for writing or generating test cases or for restarting the system if an authorization failure occurs during testing, and no risk of corrupting the underlying system on which the analysis is performed. We implemented the analysis framework presented by this paper in an analysis tool for Java programs, called Access-Control Explorer (ACE). ACE allows for automatic, safe, and precise identification of access-right requirements and library-code locations that should be made privilege-asserting to prevent client code from requiring unnecessary access rights. This paper presents experimental results obtained on large production-level applications.

Modern multiuser software systems have adopted role-based access control (RBAC) for authorization management. This paper presents a formal model for RBAC policy validation and a static-analysis model for RBAC systems that can be used to (i) identify the roles required by users to execute an enterprise application, (ii) detect potential inconsistencies caused by principal-delegation policies, which are used to override a user's role assignment, (Hi) report if the roles assigned to a user by a given policy are redundant or insufficient, and (iv) report vulnerabilities that can result from unchecked intra-component accesses. The algorithms described in this paper have been implemented as part of IBM's enterprise security policy evaluator (ESPE) tool. Experimental results show that the tool found numerous policy flaws, including ten previously unknown flaws from two production-level applications, with no false-positive reports.

We present a novel approach to client-side mining of temporal API specifications based on static analysis. Specifically, we present an interprocedural analysis over a combined domain that abstracts both aliasing and event sequences for individual objects. The analysis uses a new family of automata-based abstractions to represent unbounded event sequences, designed to disambiguate distinct usage patterns and merge similar usage patterns. Additionally, our approach includes an algorithm that summarizes abstract traces based on automata clusters, and effectively rules out spurious behaviors.

Modern component-based systems, such as Java and Microsoft .NET common language runtime (CLR), have adopted stack-based access control (SBAC). Its purpose is to use stack inspection to verify that all the code responsible for a security-sensitive action is sufficiently authorized to perform that action. Previous literature has shown that the security model enforced by SBAC is flawed in that stack inspection may allow unauthorized code no longer on the stack to influence the execution of security-sensitive code. A different approach, history-based access control (HBAC), is safe but may prevent authorized code from executing a security-sensitive operation if less trusted code was previously executed. In this paper, we formally introduce information-based access control (IBAC), a novel security model that verifies that all and only the code responsible for a security-sensitive operation is sufficiently authorized. Given an access-control policy a, we present a mechanism to extract from it an implicit integrity policy i, and we prove that IBAC enforces i. Furthermore, we discuss large-scale application code scenarios to which IBAC can be successfully applied.

Modern enterprise systems support Role-Based Access Control (RBAC). Although RBAC allows restricting access to privileged operations, a deployer may actually intend to restrict access to privileged data. This paper presents a theoretical foundation for correlating an operation-based RBAC policy with a data-based RBAC policy. Relying on a location consistency property, this paper shows how to infer whether an operation-based RBAC policy is equivalent to any databased RBAC policy. We have built a static analysis tool for Java Platform, Enterprise Edition (Java EE) called Static Analysis for Validation of Enterprise Security (SAVES). Relying on interprocedural pointer analysis and dataflow analysis, SAVES analyzes Java EE bytecode to determine if the associated RBAC policy is location consistent, and reports potential security flaws where location consistency does not hold. The experimental results obtained by using SAVES on a number of production-level Java EE codes have identified several security flaws with no false positive reports.

Static analysis has gained much attention over the past few years in applications such as bug finding and program verification. As software becomes more complex and componentized, it is common for software systems and applications to be implemented in multiple languages. There is thus a strong need for developing analysis tools for multi-language software. We introduce a technique called Analysis Preserving Language Transformation (aplt) that enables the analysis of multi-language software, and also allows analysis tools for one language to be applied to programs written in another. aplt preserves data and control flow information needed to perform static analyses, but allows the translation to deviate from the original program's semantics in ways that are not pertinent to the particular analysis. We discuss major technical difficulties in building such a translator, using a C-to-Java translator as an example. We demonstrate the feasibility and effectiveness of aplt using two usage cases: analysis of the Java runtime native methods and reuse of Java analysis tools for C. Our preliminary results show that a control- and data-flow equivalent model for native methods can eliminate unsoundness and produce reliable results, and that aplt enables seamless reuse of analysis tools for checking high-level program properties.

Java 2 has a security architecture that protects systems from unauthorized access by mobile or statically configured code. The problem is in manually determining the set of security access rights required to execute a library or application. The commonly used strategy is to execute the code, note authorization failures, allocate additional access rights, and test again. This process iterates until the code successfully runs for the test cases in hand. Test cases usually do not cover all paths through the code, so failures can occur in deployed systems. Conversely, a broad set of access rights is allocated to the code to prevent authorization failures from occurring. However, this often leads to a violation of the "Principle of Least Privilege"This paper presents a technique for computing the access rights requirements by using a context sensitive, flow sensitive, interprocedural data flow analysis. By using this analysis, we compute at each program point the set of access rights required by the code. We model features such as multi-threading, implicitly defined security policies, the semantics of the Permission.implies method and generation of a security policy description. We implemented the algorithms and present the results of our analysis on a set of programs. While the analysis techniques described in this paper are in the context of Java code, the basic techniques are applicable to access rights analysis issues in non-Java-based systems.