Research
Linear Functional Fixed-points
Nikolaj Bjorner, Joe Hendrix
We introduce a logic of functional fixed-points. It is suitable for analyzing heap-manipulating programs and can encode several of the logics recently introduced for reasoning with transitive closures. While full fixed-point logic remains undecidable, several subsets admit decision procedures. In particular, for the logic of linear functional fixed-points, we develop an abstraction refinement integration of the SMT solver Z3 and a satisfiability checker for propositional linear-time temporal logic. The integration refines the temporal labstraction by generating safety formulas until the temporal abstraction is unsatisfiable or a model for it is also a model for the functional fixed-point formula.
29 Jan. 2009
Type: TechReport
Yuri Gurevich, Itay Neeman UCLA
Infons are pieces of information. In our work DKAL (Distributed Knowledge Authorization Language), we discovered that logic of infons is a conservative extension of intuitionistic logic by means of connectives $p said$ and $p put$ where $p$ ranges over principals. Here we investigate infon logic and a emph{primal fragment} of it. In both cases, we formulate an infon calculus, develop a Kripke-type model theory, prove soundness and completeness, and prove the subformula property that is important for computational complexity. We stratify primal logic by quotation depth. In applications, quotation depth is small. Our most involved technical result is this: The derivability problem for any bounded-depth fragment of primal logic is solvable in linear time. One consequence is that the (ground) derivability problem (whether a given query follows form the given ground hypotheses) for SecPAL is solvable in linear time. SecPAL is a precursor of DKAL and expresses many important access control scenarios.
18 Jan. 2009
Type: TechReport
SybilInfer: Detecting Sybil Nodes using Social Networks
George Danezis, Prateek Mittal
SybilInfer is an algorithm for labelling nodes in a social network as honest users or Sybils controlled by an adversary. At the heart of SybilInfer lies a probabilistic model of honest social networks, and an inference engine that returns potential regions of dishonest nodes. The Bayesian inference approach to Sybil detection comes with the advantage label has an assigned probability, indicating its degree of certainty. We prove through analytical results as well as experiments on simulated and real-world network topologies that, given standard constraints on the adversary, SybilInfer is secure, in that it successfully distinguishes between honest and dishonest nodes and is not susceptible to manipulation by the adversary. Furthermore, our results show that SybilInfer outperforms state of the art algorithms, both in being more widely applicable, as well as providing vastly more accurate results.
Microsoft · 12 Jan. 2009
Type: TechReport
Practical Data Location Obfuscation
Bertrand Anckaert, Mariusz H. Jakubowski, Ramarathnam Venkatesan, Nick Saw
Software running on an open architecture, such as the PC, is vulnerable to inspection and modification. This is a concern, as software may consist of or provide access to valuable information. As a result, several defenses against program understanding and modification have been proposed in literature. The approach discussed in this paper complements existing work and focuses on hiding the actual location of data throughout the execution of the program. To achieve this, we combine three techniques: (i) periodic reordering of the heap, (ii) migrating local variables from the stack to the heap and (iii) pointer scrambling. The techniques serve to complicate static data flow analysis and dynamic data tracking. Our prototype implementation compiles C programs into a binary for which every access to the heap is redirected through a memory management unit. In order to protect traditionally stack-based variables as well, a mechanism is provided to migrate them to the heap and to adapt all accesses to those variables. Finally, an option is provided to enable pointer scrambling. If this is turned on, the program can no longer operate directly on the pointers; therefore, pointer arithmetic is intercepted as well. Experimental evaluation on benchmarks from the SPEC CPU2006 benchmark suite illustrates the type of trade-off that needs to be made for this type of protection. Balance must be struck between comprehensive protection and cost in terms of execution time and (to a lesser extent) static and dynamic memory footprint.
8 Jan. 2009
Type: TechReport
Compositional May-Must Program Analysis: Unleashing The Power of Alternation
Patrice Godefroid, Aditya V. Nori, Sriram K. Rajamani, SaiDeep Tetali
Program analysis tools typically compute two types of information: (1) may information is true of all program executions and is used to prove the absence of bugs in the program, and (2) must information is true of some program executions and is used to prove the existence of bugs in the program. In this paper, we propose a new algorithm, dubbed SMASH, which computes both may and must information compositionally. At each procedure boundary, may and must information is represented and stored as may and must summaries, respectively. Those summaries are computed in a demand-driven manner and possibly using summaries of the opposite type. We have implemented SMASH using predicate abstraction (as in SLAM) for the may part and using dynamic test generation (as in DART) for the must part. Results of experiments with 69 Microsoft Windows Vista device drivers show that SMASH can significantly outperform may-only, must-only and non compositional may-must algorithms. Indeed, intuitively, most complex code fragments in large programs are actually often either easy to prove irrelevant to the specific property of interest using may analysis or easy to traverse using directed testing. The fined-grained coupling and alternation of may (universal) and must (existential) summaries allow SMASH to easily navigate through these code fragments while traditional may-only, must-only or non-compositional may-must algorithms are stuck in their specific analyses.
Jan. 2009
Type: TechReport
Simon Scarle
In the arsenal of tools that a computational modeller can bring to bare on the study of cardiac arrhythmias, the most widely used and arguably the most successful is that of an excitable medium, a special case of a reaction-diffusion model. These are used to simulate the internal chemical reactions of a cardiac cell and the diffusion of their membrane voltages. Via a number of different methodologies it has previously been shown that reaction-diffusion systems are at multiple levels Turing complete. That is, they are capable of computation in the same manner as a universal Turing machine. However, all such computational systems are subject to a limitation know as the Halting problem. By constructing a universal logic gate using a cardiac cell model, we highlight how the Halting problem therefore could limit what it is possible to predict about cardiac tissue, arrhythmias and re-entry. All Simulations for this work were carried out on the GPU of an XBox 360 development console, and we also highlight the great gains in computational power and efficiency produced by such general purpose processing on a GPU for cardiac simulations.
2009
Type: TechReport
Predictive Models of Form Filling
Alnur Ali, Christopher Meek
In this paper we investigate predictive models of form filling. A predictive model of form filling aims to reduce the amount of time a user spends filling out a form by predicting the values of fields on the form and using these predictions to make suggestions to the form filler. Existing predictive models ignore both the values of other fields on the form and the values previously entered by users other than the current form filler when predicting the value of a target field. We introduce a novel model of predictive form filling named the Collaborative and Contextually Frequently Used model that utilizes these sources of information. We demonstrate that our model outperforms the existing, standard models of predictive form filling using a real-world collection of forms. We also demonstrate that using the values used by other form fillers can significantly improve the performance of the existing models.
Jan. 2009
Type: TechReport
Ranking through Random Sampling
Dinkar Vasudevan, Milan Vojnovic
We consider ranking of items with respect to their frequencies or values based on random sampling of items. The ranking by frequency includes variants such as identifying a set of top-k most frequent items, identifying and ranking the top-k most frequent items, and identifying the top-k most frequent items and estimating their frequencies. For the ranking by value, we consider creation of a histogram based on the values associated to items. We show how much sampling is needed to guarantee given ranking objective with the probability of error bounded by given parameter. We also identify sequential sampling algorithms that enable on-line deciding about the needed sample size, without a prior information about the underlying distribution from which the sampling is done. To the best of our knowledge, our results for ranking by frequency are novel and those for ranking by value extend the previously-known result by Chaudhuri et al (1998) to histograms of arbitrarily given widths, a case of interest in practice. Our results are applicable in the context of querying large-scale data sets.
Microsoft · Jan. 2009
Type: TechReport
Comments
- Anonymous
February 24, 2009
PingBack from http://www.anith.com/?p=13223