Solving a Constraint Satisfaction Problem (CSP) usually requires a model typically using existing basic constraints. The most flexible form of constraint, ad-hoc (generic) constraints defined with certain constraint representations, such as binary constraint tree (BCT) and decision diagrams, have been proposed where basic constraints in intensional form are insufficient. A modeller may wish to combine basic constraints using logic operators (and, or, negation). However, negation, a key logical operator for expressivity is not tractable in many existing constraint representations. This creates a dilemma, for modelling, we would desire more flexibility, but a model whose operations are intractable may in turn be impractical. In this paper, we give a framework which allows for a tractable negation operator on constraint representations. We apply the framework on the BCT and ordered decision diagram constraints, giving new subforms. These subforms can be strictly more succinct than ordered multi-valued decision diagrams (OMDD), while being as tractable as OMDD for logical combinations. We give applications to show effective propagators from logical combinations and in building large constraint models for configuration problems.

Abstract Knowledge compilation (KC) involves compiling propositional constraints into tractable target languages which in turn efficiently support multiple analyses or queries of the constraints. Solving these queries plays a crucial role in the synthesis and verification of hardware and software systems. Recently, we proposed the target language, Constrained Conjunction & Decision Diagrams (CCDD), experimentally shown to be promising for individual model counting queries. Here, we present the compiler, $$\textsf{Panini}$$ Panini , which compiles CNF into CCDD. $$\textsf{Panini}$$ Panini supports a range of queries. We present an empirical evaluation focusing on two fundamental queries, uniform sampling and (multiple) model counting, with a wide range of applications. While counting and sampling have witnessed significant performance improvements over the years, scalability still remains the primary challenge. Our evaluation over 600 instances from model counting competitions 2022–2024 show that $$\textsf{Panini}$$ Panini achieves state of art compilation by solving 322 instances, which is 183, 148, and 38 more than Dsharp, miniC2D, and D4 respectively. Secondly, on repetitive tasks, $$\textsf{Panini}$$ Panini solves 53 and 50 more instances than ExactMC and SharpSAT-TD for model counting, and 175 and 132 more instances than SPUR and KUS for uniform sampling, respectively.

Fairness in artificial intelligence (AI) has become a growing concern due to discriminatory outcomes in AI-based decision-making systems. While various methods have been proposed to mitigate bias, most rely on complete demographic information, an assumption often impractical due to legal constraints and the risk of reinforcing discrimination. This survey examines fairness in AI when demographics are incomplete, addressing the gap between traditional approaches and real-world challenges. We introduce a novel taxonomy of fairness notions in this setting, clarifying their relationships and distinctions. Additionally, we summarize existing techniques that promote fairness beyond complete demographics and highlight open research questions to encourage further progress in the field.

Memory errors continue to be a critical concern for programs written in low-level programming languages such as C and C++. Many different memory error defenses have been proposed, each with varying trade-offs in terms of overhead, compatibility, and attack resistance. Some defenses are highly compatible but only provide minimal protection, and can be easily bypassed by knowledgeable attackers. On the other end of the spectrum, capability systems offer very strong (unforgeable) protection, but require novel software and hardware implementations that are incompatible by definition. The challenge is to achieve both very strong protection and high compatibility.

The PHP interpreter, powering over 70% of web-sites on the internet, plays a crucial role in web development. Existing approaches to finding bugs in PHP primarily focus on detecting explicit security issues through crashes or sanitizer-based oracles, but fail to identify logic bugs that can silently lead to incorrect results. We observe that the introduction of Just-In-Time (JIT) compilation mode in PHP presents an opportunity for differential testing, as it provides an alternative implementation of the same language specification. We propose, ZendDiff, an automatic differential testing framework that effectively detects logic bugs in the PHP interpreter by comparing JIT and non-JIT execution results. Our differential testing incorporates three techniques: program state probing for fine-grained execution state comparison, JIT-aware program mutation to sufficiently exercise JIT functionality, and dual verification to handle non-deterministic behaviors in PHP programs. Our experimental results demonstrate that ZendDiffoutperforms the official test suite used in PHP’s continuous integration, achieving higher code coverage and executing more Zend opcodes. Through ablation studies, we validate the effectiveness of these techniques. To date, ZendDiffhas identified 51 previously unknown logic bugs in the PHP interpreter, with 37 already fixed and 3 confirmed by the PHP maintainers. ZendDiffhas been acknowledged by the PHP community and offers a practical tool for automatically discovering logic bugs in the PHP interpreter.

Graph Neural Networks (GNNs) have demonstrated remarkable capabilities across various domains. Despite the successes of GNN deployment, their utilization often reflects societal biases, which critically hinder their adoption in high-stake decision-making scenarios such as online clinical diagnosis, financial crediting, etc. Numerous efforts have been made to develop fair GNNs but they typically concentrate on either individual or group fairness, overlooking the intricate interplay between the two, resulting in the enhancement of one, usually at the cost of the other. In addition, existing individual fairness approaches using a ranking perspective fail to identify discrimination in the ranking. This paper introduces two innovative notions dealing with individual graph fairness and group-aware individual graph fairness, aiming to more accurately measure individual and group biases. Our Group Equality Individual Fairness (GEIF) framework is designed to achieve individual fairness while equalizing the level of individual fairness among subgroups. Preliminary experiments on several real-world graph datasets demonstrate that GEIF outperforms state-of-the-art methods by a significant margin in terms of individual fairness, group fairness, and utility performance.

Graph Database Management Systems (GDBMSs) store graphs as data. They are used naturally in applications such as social networks, recommendation systems and program analysis. However, they can be affected by logic bugs, which cause the GDBMSs to compute incorrect results and subsequently affect the applications relying on them. In this work, we propose injective and surjective Graph Query Transformation (GQT) to detect logic bugs in GDBMSs. Given a query Q, we derive a mutated query Q', so that either their result sets are: (i) semantically equivalent; or (ii) variant based on the mutation to be either a subset or superset of each other. When the expected relationship between the results does not hold, a logic bug in the GDBMS is detected. The key insight to mutate Q is that the graph pattern in graph queries enables systematic query transformations derived from injective and surjective mappings of the directed edge sets between Q and Q'. We implemented injective and surjective Graph Query Transformation (GQT) as a tool called GraphGenie and evaluated it on 6 popular and mature GDBMSs. GraphGenie has found 25 unknown bugs, comprising 16 logic bugs, 3 internal errors, and 6 performance issues. Our results demonstrate the practicality and effectiveness of GraphGenie in detecting logic bugs in GDBMSs which has the potential for improving the reliability of applications relying on these GDBMSs.

Model counting is a fundamental problem which has been influential in many applications, from artificial intelligence to formal verification. Due to the intrinsic hardness of model counting, approximate techniques have been developed to solve real-world instances of model counting. This paper designs a new anytime approach called PartialKC for approximate model counting. The idea is a form of partial knowledge compilation to provide an unbiased estimate of the model count which can converge to the exact count. Our empirical analysis demonstrates that PartialKC achieves significant scalability and accuracy over prior state-of-the-art approximate counters, including satss and STS. Interestingly, the empirical results show that PartialKC reaches convergence for many instances and therefore provides exact model counting performance comparable to state-of-the-art exact counters.

Ad-hoc constraints (also called generic constraints) are important for modelling Constraint Satisfaction Problems (CSPs). Many representations have been proposed to define ad-hoc constraints, such as tables, decision diagrams, binary constraint trees, automata and context-free grammars. However, prior works mainly focus on efficient Generalized Arc Consistency (GAC) propagators of ad-hoc constraints using the representations. In this paper, we ask a more fundamental question which bears on modelling constraints in a CSP as ad-hoc constraints, how the choice of constraints and operations affect tractability. Rather than ad-hoc constraints and their GAC propagators, our focus is on their expressive power in terms of succinctness (polysize) and cost of operations/queries (polytime). We use a large set of constraint families to investigate the expressive power of 14 existing ad-hoc constraints. We show a complete map of the succinctness of the ad-hoc constraints. We also present results on the tractability of applying various operations and queries on the ad-hoc constraints. Finally, we give case studies illustrating how our results can be useful for questions in the modelling of CSPs.

Many practical applications require synthesizing directed graphs that satisfy the acyclic constraint along with some side constraints. Several methods have been devised for encoding acyclicity of directed graphs into SAT, each of which is based on a cycle-detecting algorithm. The leaf-elimination encoding (LEE) repeatedly eliminates leaves from the graph, and judges the graph to be acyclic if the graph becomes empty at a certain time. The vertex-elimination encoding (VEE) exploits the property that the cyclicity of the resulting graph produced by the vertex-elimination operation entails the cyclicity of the original graph. While VEE is significantly smaller than the transitive-closure encoding for sparse graphs, it generates prohibitively large encodings for large dense graphs. This paper reports on a comparison study of four SAT encodings for acyclicity of directed graphs, namely, LEE using unary encoding for time variables (LEE-u), LEE using binary encoding for time variables (LEE-b), VEE, and a hybrid encoding which combines LEE-b and VEE. The results show that the hybrid encoding significantly outperforms the others.

Ordered Multi-valued Decision Diagram (MDD) is a compact representation used to model various constraints, such as regular constraints and table constraints. It can be particularly useful for representing ad-hoc problem specific constraints. Many algorithms have been proposed to enforce Generalized Arc Consistency (GAC) on MDD constraints. In this paper, we introduce a new compact representation called Binary Constraint Tree (BCT). We propose tree binary encodings to transform any MDD constraint into a BCT constraint. We also present a specialized algorithm enforcing GAC on the BCT constraint resulting from a MDD constraint. Experimental results on a large set of benchmarks show that the BCT GAC algorithm can significantly outperform state-of-the-art MDD as well as table GAC algorithms.

Many detection and defense mechanisms have been proposed to prevent and mitigate memory errors. A good understanding of the pros and cons of memory defense mechanisms is essential before practical deployment. However, the environment, compilers, and defenses change over time. Thus, a benchmark providing comprehensive evaluations of a range of compilation option choices and defenses is helpful to give developers guidance. The most well-known test suite for evaluating spatial memory errors and exploits is RIPE. However, we show that it is no longer applicable, and a new benchmark is needed. Furthermore, a benchmark should be extensible to evolve over time easily. We propose RecIPE, a new extensible and comprehensive benchmark for evaluating memory error defenses. For extensibility and customisability, RecIPE consists of two components. The TestGen component generates vulnerable code from configurable templates across various vulnerable attributes allowing easy changes through the templates. Measuring the attack and exploitation is with the DefEval component, serving as an attacker at runtime and can be updated with new exploitations. We present a comprehensive evaluation of compiler defenses and sanitizers on RecIPE with gcc and clang, showing the strengths and weaknesses of the various defenses. The results show pros and cons which may not be well known, including gaps between the in-principle guarantee and practical implementation. Our results also point out directions for further improvement in defenses.

Ordered Multi-valued Decision Diagrams (MDDs) have been shown to be useful to represent finite domain functions/relations. For example, various constraints can be modelled with MDD constraints. Recently, a new representation called Binary Constraint Tree (BCT), which is a (special) tree structure binary Constraint Satisfaction Problem, has been proposed to encode MDDs and shown to outperform existing MDD constraint propagators in Constraint Programming solvers. BCT is a compact representation, and it can be exponentially smaller than MDD for representing some constraints. Here, we also show that BCT is compact for representing non-deterministic finite state automaton (NFA) constraints. In this paper, we investigate how to encode BCT into CNF form, making it suitable for SAT solvers. We present and investigate five BCT CNF encodings. We compare the propagation strength of the BCT CNF encodings and experimentally evaluate the encodings on a range of existing benchmarks. We also compare with seven existing CNF encodings of MDD constraints. Experimental results show that the CNF encodings of BCT constraints can outperform those of MDD constraints on various benchmarks.

Memory errors, such as buffer overflows and use-after-free, remain the root cause of many security vulnerabilities in modern software. The use of closed source software further exacerbates the problem, as source-based memory error mitigation cannot be applied. While many memory error detection tools exist, most are based on a single error detection methodology with resulting known limitations, such as incomplete memory error detection (redzones) or false error detections (low-fat pointers). In this paper we introduce RedFat, a memory error hardening tool for stripped binaries that is fast, practical and scalable. The core idea behind RedFat is to combine complementary error detection methodologies---redzones and low-fat pointers---in order to detect more memory errors that can be detected by each individual methodology alone. However, complementary error detection also inherits the limitations of each approach, such as false error detections from low-fat pointers. To mitigate this, we introduce a profile-based analysis that automatically determines the strongest memory error protection possible without negative side effects.

The past two decades have seen the significant improvements of the scalability of practical model counters, which have been quite influential in many applications from artificial intelligence to formal verification. While most of exact counters fall into two categories, search-based and compilation-based, Huang and Darwiche's remarkable observation ties these two categories: the trace of a search-based exact model counter corresponds to a Decision-DNNF formula. Taking advantage of literal equivalences, this paper designs an efficient model counting technique such that its trace is a generalization of Decision-DNNF formula. We first propose a generalization of Decision-DNNF, called CCDD, to capture literal equivalences, then show that CCDD supports model counting in linear time, and finally design a model counter, called ExactMC, whose trace corresponds to CCDD. We perform an extensive experimental evaluation over a comprehensive set of benchmarks and conduct performance comparison of ExactMC vis-a-vis the state of the art counters, c2d, Dsharp, miniC2D, D4, ADDMC, and Ganak. Our empirical evaluation demonstrates ExactMC can solve 885 instances while the prior state of the art could solve only 843 instances, representing a significant improvement of 42 instances.

Constraint Programming is a powerful paradigm to model and solve combinatorial problems. While there are many kinds of constraints, the table constraint (also called a CSP) is perhaps the most significant—being the most well-studied and has the ability to encode any other constraints defined on finite variables. Thus, designing efficient filtering algorithms on table constraints has attracted significant research efforts. In turn, there have been great improvements in efficiency over time with the evolution and development of AC and GAC algorithms. In this paper, we survey the existing filtering algorithms for table constraint focusing on historically important ideas and recent successful techniques shown to be effective.

Effective and robust search heuristics are critical for solving constraint satisfaction or optimization problems. In this paper, we propose a new hybrid heuristic which uses the idea of reducing the dynamic arity of constraints, called Constraint-Arity-Reduction (CAR). The hybrid heuristic is formed with a base heuristic which switches to CAR using a switching heuristic. We experimented with hybrids of CAR combining existing state-of-the-art search heuristics. Experimental results on a variety of structured benchmarks show that hybrid CAR heuristics is an effective and competitive strategy, which can successfully reduce the search space and improve the performance of existing heuristics on a variety of problems.

Constraint Satisfaction Problems (CSPs) are typically solved with Generalized Arc Consistency (GAC). A general CSP can also be encoded into a binary CSP and solved with Arc Consistency (AC). The well-known Hidden Variable Encoding (HVE) is still a state-of-the-art binary encoding for solving CSPs. We propose a new binary encoding, called Bipartite Encoding (BE) which uses the idea of partitioning constraints. A BE encoded CSP can achieve a higher level of consistency than GAC on the original CSP. We give an algorithm for creating compact bipartite encoding for non-binary CSPs. We present a AC propagator on the binary constraints from BE exploiting their special structure. Experiments on a large set of non-binary CSP benchmarks with table constraints using the Wdeg, Activity and Impact heuristics show that BE with our AC propagator can outperform existing state-of-the-art GAC algorithms (CT, STRbit) and binary encodings (HVE with HTAC).

Symbolic execution is a powerful technique for bug finding and program testing. It is successful in finding bugs in real-world code. The core reasoning techniques use constraint solving, path exploration, and search, which are also the same techniques used in solving combinatorial problems, e.g., finite-domain constraint satisfaction problems (CSPs). We propose CSP instances as more challenging benchmarks to evaluate the effectiveness of the core techniques in symbolic execution. We transform CSP benchmarks into C programs suitable for testing the reasoning capabilities of symbolic execution tools. From a single CSP P, we transform P depending on transformation choice into different C programs. Preliminary testing with the KLEE, Tracer-X, and LLBMC tools show substantial runtime differences from transformation and solver choice. Our C benchmarks are effective in showing the limitations of existing symbolic execution tools. The motivation for this work is we believe that benchmarks of this form can spur the development and engineering of improved core reasoning in symbolic execution engines.

Effective solving of constraint problems often requires choosing good or specific search heuristics. However, choosing or designing a good search heuristic is non-trivial and is often a manual process. In this paper, rather than manually choosing/designing search heuristics, we propose the use of bandit-based learning techniques to automatically select search heuristics. Our approach is online where the solver learns and selects from a set of heuristics during search. The goal is to obtain automatic search heuristics which give robust performance. Preliminary experiments show that our adaptive technique is more robust than the original search heuristics. It can also outperform the original heuristics.

Low-level programming languages with weak/static type systems, such as C and C++, are vulnerable to errors relating to the misuse of memory at runtime, such as (sub-)object bounds overflows, (re)use-after-free, and type confusion. Such errors account for many security and other undefined behavior bugs for programs written in these languages. In this paper, we introduce the notion of dynamically typed C/C++, which aims to detect such errors by dynamically checking the "effective type" of each object before use at runtime. We also present an implementation of dynamically typed C/C++ in the form of the Effective Type Sanitizer (EffectiveSan). EffectiveSan enforces type and memory safety using a combination of low-fat pointers, type meta data and type/bounds check instrumentation. We evaluate EffectiveSan against the SPEC2006 benchmark suite and the Firefox web browser, and detect several new type and memory errors. We also show that EffectiveSan achieves high compatibility and reasonable overheads for the given error coverage. Finally, we highlight that EffectiveSan is one of only a few tools that can detect sub-object bounds errors, and uses a novel approach (dynamic type checking) to do so.

Abstract Malformed data-structures can lead to runtime errors such as arbitrary memory access or corruption. Despite this, reasoning over data-structure properties for low-level heap manipulating programs remains challenging. In this paper we present a constraint-based program analysis that checks data-structure integrity, w.r.t. given target data-structure properties, as the heap is manipulated by the program. Our approach is to automatically generate a solver for properties using the type definitions from the target program. The generated solver is implemented using a Constraint Handling Rules (CHR) extension of built-in heap, integer and equality solvers. A key property of our program analysis is that the target data-structure properties areshape neutral, i.e., the analysis does not check for properties relating to a given data-structure graphshape, such as doubly-linked-lists versus trees. Nevertheless, the analysis can detect errors in a wide range of data-structure manipulating programs, including those that use lists, trees, DAGs, graphs, etc. We present an implementation that uses the Satisfiability Modulo Constraint Handling Rules (SMCHR) system. Experimental results show that our approach works well for real-world C programs.

Research in computer science (CS) is published mainly in conferences. We investigate the possibility of automatically categorizing CS conferences by using exemplars (influential conferences). We propose an automatic exemplars selection method. Our experiments show that categorizing by exemplars matches well with curated topic classification from the Chinese CCF conference list. The results also accord with manual judgement which show promise as a practical and robust method for categorizing CS conferences.

Many Android apps (applications) employ databases for managing sensitive data, thus, security of their databases is a concern. In this paper, we systematically study attacks targeting databases in benign Android apps. In addition to studying database vulnerabilities accessed from content providers, we define and study a new class of database vulnerabilities. We propose an analysis framework to find such vulnerabilities with a proof-of-concept exploit. Our analysis combines static dataflow analysis, symbolic execution with models for handling complex objects such as URIs and dynamic testing. We evaluate our analysis on popular Android apps, successfully finding many database vulnerabilities. Surprisingly, our analyzer finds new ways to exploit previously reported and fixed vulnerabilities. Finally, we propose a fine-grained protection mechanism extending the manifest to protect against database attacks.

The sybil problem is a fundamental problem in distributed systems and online social networks (OSNs). The basic problem is that an attacker can easily create multiple identities in a distributed or open online system. Popular and effective sybil defenses are usually based on properties of the network structure. However, most defenses assume that it is hard for the attacker to make many connections to honest users. However, this assumption can be invalid in real OSNs which decreases the effectiveness of many sybil defenses. We propose a graph transformation, the strong link graph, to mitigate such attacks by reducing the effect ofa large number of attack edges. Our preliminary experiments show indeed that when the attacker has many attack edges, existing algorithms such as SybilLimit, SybilRank and Gatekeeper are ineffective. After the strong link graph is applied, it deletes many of the attack edges, restoring the effectiveness of the sybil defenses.

Effective general-purpose search strategies are an important component in Constraint Programming. We introduce a new idea, namely, using correlations between variables to guide search. Variable correlations are measured and maintained by using domain changes during constraint propagation. We propose two variable heuristics based on the correlation matrix, crbs-sum and crbs-max. We evaluate our correlation heuristics with well known heuristics, namely, dom/wdeg, impact-based search and activity-based search. Experiments on a large set of benchmarks show that our correlation heuristics are competitive with the other heuristics, and can be the fastest on many series.

Android is designed such that Android applications (Apps) can provide functions to each other by providing a complex inter-component communication (ICC) model. While app interactions make it convenient and easy for one app to delegate functionality to another app, it also leads to permission re-delegation among Android apps which can cause privilege escalation . One approach taken by existing work tries to mitigate privilege escalation by enforcing tightened permissions. Unfortunately, preventing privilege escalation often renders the recipient apps unusable (for example, causing the app to crash). In this work, we propose another approach to address the privilege escalation problem from Android app ICC which intends to better preserve app functionality. We propose a context specific resource virtualization to eliminate privilege escalation by taking into account the interaction of ICCs among apps. We evaluated our prototype system, R opp D roid , on real-world Android apps and showed the effectiveness in providing robust protection for those apps. Our prototype also has low performance overheads.

Heap buffer overflow (underflow) errors are a common source of security vulnerabilities. One prevention mechanism is to add object bounds meta information and to instrument the program with explicit bounds checks for all memory access. The so-called "fat pointers" approach is one method for maintaining and propagating the meta information where native machine pointers are replaced with "fat" objects that explicitly store object bounds. Another approach is "low fat pointers", which encodes meta information within a native pointer itself, eliminating space overheads and also code compatibility issues. This paper presents a new low-fat pointer encoding that is fully compatible with existing libraries (e.g. pre-compiled libraries unaware of the encoding) and standard hardware (e.g. x86_64). We show that our approach has very low memory overhead, and competitive with existing state-of-the-art bounds instrumentation solutions.

Malware on Android has been reported to be on the rise. There are many anti-virus (AV) apps available on Android. However, most AVs are presented as black-boxes without details given about their workings. In this paper, we propose to determine the key elements used by the AVs, which we call inferring the AV detection logic, through a black-box testing methodology. We perform a large scale experiment on 57 Android AVs using 2000 malware variants to evaluate whether the detection logic can be found and whether the AVs can detect the malware. Our experiments show that a majority of AVs detect malware using simple static features. Such features can be easily obfuscated by renaming or encrypting strings and data, which can make it easy to evade some AVs. We also observe trends showing that AVs use common features to detect malware across all families.

This paper presents tagged-MapReduce, a general extension to MapReduce that supports secure computing with mixed-sensitivity data on hybrid clouds. Tagged-MapReduce augments each key-value pair in MapReduce with a sensitivity tag. This enables fine-grained dataflow control during execution to prevent data leakage as well as supporting expressive security policies and complex MapReduce computations. Security constraints for preventing data leakage impose restrictions on computation and data storage/transfer, hence, we present scheduling strategies that can exploit properties of the map and reduce functions to rearrange the computation for greater efficiency under these constraints while maintaining MapReduce correctness. We present a general security framework for analyzing MapReduce computations in the hybrid cloud which captures how dataflow can leak information through execution. Experiments on Amazon EC2 with our prototype in Hadoop show that we are able to obtain security while effectively outsourcing computation to the public cloud and reducing inter-cloud communication.

Binary loading is used extensively in many operating systems, e.g. Program execution usually involves loading dynamically linked libraries (binaries in DLL form). In Windows, binary loading is used heavily, but the process is complex and is affected by many factors - this flexibility turns out to be a rich source of attacks. When a typical Windows executable runs, many binaries are loaded, possibly from third parties. It is not uncommon for Windows programs to have binary loading vulnerabilities. However, it is difficult for software developers to identify if their programs have such vulnerabilities, how they arise, and how to fix them. We propose LDRSCOPE, to explain why binaries are loaded and detect the factors that affect the loading. This allows developers to better identify the problems and secure their code. We also deal with vulnerabilities arising from software configuration such as configuration files. Some vulnerabilities can also be due to third party libraries, we clearly identify and explain their effects.

The idea of a hybrid cloud is to combine a private cloud (e.g., an organization's in-house private datacenter) together with a public cloud (e.g., Amazon EC2). Hybrid cloud computing offers increased scalability and cost-effectiveness: the private cloud can be used for typical workloads, but when additional resources are needed during peak computations, the public cloud is harnessed. This hybrid cloud architecture has already gained adoption [1] and is still undergoing rapid development [4].

In this paper, we revisit the problem of the link privacy attack in online social networks. In the link privacy attack, it turns out that by bribing or compromising a small number of nodes (users) in the social network graph, it is possible to obtain complete link information for a much larger fraction of other non-bribed nodes in the graph. This can constitute a significant privacy breach in online social networks where the link information of nodes is kept private or accessible only to closely related nodes.

Modern business applications and scientific databases call for inherently dynamic data storage environments. Such environments are characterized by two challenging features: (a) they have little idle system time to devote on physical design; and (b) there is little, if any, a priori workload knowledge, while the query and data workload keeps changing dynamically. In such environments, traditional approaches to index building and maintenance cannot apply. Database cracking has been proposed as a solution that allows on-the-fly physical data reorganization, as a collateral effect of query processing. Cracking aims to continuously and automatically adapt indexes to the workload at hand, without human intervention. Indexes are built incrementally, adaptively, and on demand. Nevertheless, as we show, existing adaptive indexing methods fail to deliver workload-robustness ; they perform much better with random workloads than with others. This frailty derives from the inelasticity with which these approaches interpret each query as a hint on how data should be stored. Current cracking schemes blindly reorganize the data within each query's range, even if that results into successive expensive operations with minimal indexing benefit. In this paper, we introduce stochastic cracking , a significantly more resilient approach to adaptive indexing. Stochastic cracking also uses each query as a hint on how to reorganize data, but not blindly so; it gains resilience and avoids performance bottlenecks by deliberately applying certain arbitrary choices in its decision-making. Thereby, we bring adaptive indexing forward to a mature formulation that confers the workload-robustness previous approaches lacked. Our extensive experimental study verifies that stochastic cracking maintains the desired properties of original database cracking while at the same time it performs well with diverse realistic workloads.

Securing Windows is a challenge because of its large attack surface which can lead to many ways where binaries can be loaded and subsequently executed. Furthermore, the software in the system is itself dynamic as binaries need to be installed, updated and uninstalled. Binaries can also be created dynamically during software development as well as other situations. We present a new binary security model called BinInt which provides integrity for binaries and prevents the use of unauthorized binaries. We have implemented a BinInt prototype designed with usability in mind to be compatible with existing software in binary form. It has low overhead and thus can be permanently on.

The popularity and size of online social networks means the social graph contains valuable data about relationships. Such graph data may be sensitive. Thus, there is a need to protect the data from privacy leaks. On the other hand, public information and crawl ability are needed to support the basic utility and services on top of the social network. We propose policies where the owner of the social network can tradeoff between these two conflicting goals. We experiment with real world social network graphs and show that the owner of the graph can employ policies which can meet particular tradeoffs under different crawlers. Furthermore, the policies are efficient and scalable for the owner of the social network.

Maximum-flow algorithms are used to find spam sites, build content voting system, discover communities, etc., on graphs from the Internet. Such graphs are now so large that they have outgrown conventional memory-resident algorithms. In this paper, we show how to effectively parallelize a max-flow algorithm based on the Ford-Fulkerson method on a cluster using the MapReduce framework. Our algorithm exploits the property that such graphs are small-world networks with low diameter and employs optimizations to improve the effectiveness of MapReduce and increase parallelism. We are able to compute max-flow on a subset of the Face book social network graph with 411 million vertices and 31 billion edges using a cluster of 21 machines in reasonable time.

Abstract Functional constraints and bi-functional constraints are an important constraint class in Constraint Programming (CP) systems, in particular for Constraint Logic Programming (CLP) systems. CP systems with finite domain constraints usually employ Constraint Satisfaction Problem(s)-based solvers which use local consistency, for example, arc consistency. We introduce a new approach which is based instead on variable substitution. We obtain efficient algorithms for reducing systems involving functional and bi-functional constraints together with other nonfunctional constraints. It also solves globally any CSP where there exists a variable such that any other variable is reachable from it through a sequence of functional constraints. Our experiments on random problems show that variable elimination can significantly improve the efficiency of solving problems with functional constraints.

The problem of dividing a sequence of values into segments occurs in database systems, information retrieval, and knowledge management. The challenge is to select a finite number of boundaries for the segments so as to optimize an objective error function defined over those segments. Although this optimization problem can be solved in polynomial time, the algorithm which achieves the minimum error does not scale well, hence it is not practical for applications with massive data sets. There is considerable research with numerous approximation and heuristic algorithms. Still, none of those approaches has resolved the quality-efficiency tradeoff in a satisfactory manner. In (Halim, Karras, and Yap 2009), we obtain near linear time algorithms which achieve both the desired scalability and near-optimal quality, thus dominating earlier approaches. In this paper, we show how two ideas from artificial intelligence, an efficient local search and recombination of multiple solutions reminiscent of genetic algorithms, are combined in a novel way to obtain state of the art histogram construction algorithms.

Software often lives in a complex software eco-system with complex interactions and dependencies between different modules or components. In Windows, this problem is exacerbated both by the overall system complexity and its closed source nature. Even when source is available, there are still interactions with modules which are only in binary form.

Histogram construction or sequence segmentation is a basic task with applications in database systems, information retrieval, and knowledge management. Its aim is to approximate a sequence by line segments. Unfortunately, the quadratic algorithm that derives an optimal histogram for Euclidean error lacks the desired scalability. Therefore, sophisticated approximation algorithms have been recently proposed, while several simple heuristics are used in practice. Still, these solutions fail to resolve the efficiency-quality tradeoff in a satisfactory manner. In this paper we take a fresh view on the problem. We propose conceptually clear and scalable algorithms that efficiently derive high-quality histograms. We experimentally demonstrate that existing approximation schemes fail to deliver the desired efficiency and conventional heuristics do not fare well on the side of quality. On the other hand, our schemes match or exceed the quality of the former and the efficiency of the latter.

We propose a new main memory index structure for abstract regions (objects) which may heavily overlap, the RCtree. These objects are "dynamic" and may have short life spans. The novelty is that rather than representing an object by its minimum bounding rectangle (MBR), possibly with pre-processed segmentation into many small MBRs, we use the actual shape of the object to maintain the index. This saves significant space for objects with large spatial extents since pre-segmentation is not needed. We show that the query performance of RC-tree is much better than many indexing schemes on synthetic overlapping data sets. The performance is also competitive on real-life GIS nonoverlapping data sets.

Temporal constraint networks are embedded in many planning and scheduling problems. In dynamic problems, a fundamental challenge is to decide whether such a network can be executed as uncertainty is revealed over time. Very little work in this domain has been done in the probabilistic context. In this paper, we propose a temporal constraint network (TCN) model where durations of uncertain activities are represented by random variables. We wish to know whether such a network is robust controllable, i.e. can be executed dynamically within a given failure probability, and if so, how one might find a feasible schedule as the uncertainty variables are revealed dynamically. We present a computationally tractable and efficient approach to solve this problem. Experimentally, we study how the failure probability is affected by various network properties of the underlying TCN, and the relationship of failure rates between robust and weak controllability

NP-hard combinatorial optimization problems are common in real life. Due to their intractability, local search algorithms are often used to solve such problems. Since these algorithms are heuristic-based, it is hard to understand how to improve or tune them. We propose an interactive visualization tool, VIZ, meant for understanding the behavior of local search. VIZ uses animation of abstract search trajectories with other visualizations which are also animated in a VCR-like fashion to graphically playback the algorithm behavior. It combines generic visualizations applicable on arbitrary algorithms with algorithm and problem specific visualizations. We use a variety of techniques such as alpha blending to reduce visual clutter and to smooth animation, highlights and shading, automatically generated index points for playback, and visual comparison of two algorithms. The use of multiple viewpoints can be an effective way of understanding search behavior and highlight algorithm behavior which might otherwise be hidden.

In this paper, we show that there is a close relation between consistency in a constraint network and set intersection. A proof schema is provided as a generic way to obtain consistency properties from properties on set intersection. This approach not only simplifies the understanding of and unifies many existing consistency results, but also directs the study of consistency to that of set intersection properties in many situations, as demonstrated by the results on the convexity and tightness of constraints in this paper. Specifically, we identify a new class of tree convex constraints where local consistency ensures global consistency. This generalizes row convex constraints. Various consistency results are also obtained on constraint networks where only some, in contrast to all in the existing work,constraints are tight.

Logging and auditing is an important system facility for monitoring correct system operation and for detecting potential security problems. We present an architecture for implementing user-level auditing monitors which: (i) does not require superuser privileges; (ii) makes it simple to create user defined monitors which are transparent; and (iii) provides security guarantees such as mandatory and reliable monitoring while maintaining confidentiality of setuid processes. We avoid problems of self-referential monitoring. Monitor use policies can be specified to increase flexibility. We show that our framework can be tailored so that it is very efficient with low overhead on macro and micro benchmarks. This demonstrates that it is feasible to make use of arbitrary and programmable user-level monitors for system security and auditing applications.

We present a framework for the parallelization of depth-first combinatorial search algorithms on a network of computers. Our architecture is intended for a distributed setting and uses a work stealing strategy coupled with a small number of primitives for the processors (which we call workers) to obtain new work and to communicate to other workers. These primitives are a minimal imposition and integrate easily with constraint programming systems. The main contribution is an adaptive architecture, which allows workers to incrementally join and leave and has good scaling properties as the number of workers increases. Our empirical results illustrate that near-linear speedup for backtrack search is achieved for up to 61 workers. It suggests that near-linear speedup is possible with even more workers. The experiments also demonstrate where departures from linearity can occur for small problems, and also for problems where the parallelism can itself affect the search as in branch and bound.

10.1145/765568.765569

This paper describes a new programming system for writing Web applications with reactive agents, i.e. the agents can have complex responses which depend on how the environment changes. Our prototype system is based on the open constraint programming framework using the constraint logic programming language CLP(R). The benefit of reactive Web agents is that activities of agents can be coordinated and synchronized using a common store and the agents can themselves be written as a system of interacting rules. Our thesis is that such a system makes it easy to write powerful reactive applications. We use a stock trading system to illustrate our reactive agents. Some details of the implementation are also given.

Many web pages have implicit structure. In this paper, we show the feasibility of automatically extracting data from web pages by using approximate matching techniques. This can be applied to generate automatic wrappers or to notify/display web page differences, web page change monitoring, etc.

The task of programming concurrent systems is substantially more difficult than the task of programming sequential systems with respect to both correctness and efficiency. In this paper we describe a constraint-based methodology for writing concurrent applications. A system is modeled as: (a) a set of processes containing a sequence of "markers" denoting the processes points of interest; and (b) a constraint store. Process synchronization is specified by incrementally adding constraints on the markers execution order into the constraint store. The constraint store contains a declarative specification based on a temporal constraint logic program. The store, thus, acts as a coordination entity which on the one hand encapsulates the system synchronization requirements, and on the other hand, provides a declarative specification of the system concurrency issues. This provide great advantages in writing concurrent programs and manipulating them while preserving correctness.

Constraint Logic Programming (CLP) languages extend logic programming by allowing the use of constraints from different domains such as real numbers or Boolean functions. They have proved to be ideal for expressing problems that require interactive mathematical modeling and complex combinatorial optimization problems. However, CLP languages have mainly been considered as research systems, useful for rapid prototyping, by not really competitive with more conventional programming languages where efficiency is a more important consideration. One promising approach to improving the performance of CLP systems is the use of powerful program optimizations to reduce the cost of constraint solving. We extend work in this area by describing a new optimizing compiler for the CLP language CLP(ℛ). The compiler implements six powerful optimizations: reordering of constraints, removal of redundant variables, and specialization of constraints which cannot fail. Each program optimization is designed to remove the overhead of constraint solving when possible and keep the number of constraints in the store as small as possible. We systematically evaluate the effectiveness of each optimization in isolation and in combination. Our empirical evaluation of the compiler verifies that optimizing compilation can be made efficient enough to allow compilation of real-world programs and that it is worth performing such compilation because it gives significant time and space performance improvements.

An abstract machine is described for the CLP(ℜ) programming language. It is intended as a first step toward enabling CLP(ℜ) programs to be executed with efficiency approaching that of conventional languages. The core Constraint Logic Arithmetic Machine (CLAM) extends the Warren Abstract Machine (WAM) for compiling Prolog with facilities for handling real arithmetic constraints. The full CLAM includes facilities for taking advantage of information obtained from global program analysis.

In constraint logic programming (CLP) systems, the standard technique for dealing with hard constraints is to delay solving them until additional constraints reduce them to a simpler form.For example, the CLP (7?) system delays the solving of nonlinear equations until they become linear, when certain variables become ground.In a naive implement ation, the overhead of delaying and awakening constraints could render a CLP system impractical.