Searcharxiv⌕ Search

arXiv subjects

Deepak Garg

Publications and source records attributed to Deepak Garg.

52 records · Page 3Linked to original sources
arXiv2017

WebPol: Fine-grained Information Flow Policies for Web Browsers

In the standard web browser programming model, third-party scripts included in an application execute with the same privilege as the application's own code. This leaves the application's confidential data vulnerable to theft and leakage by malicious code and inadvertent bugs in the third-party scripts. Security mechanisms in modern browsers (the same-origin policy, cross-origin resource sharing and content security policies) are too coarse to suit this programming model. All these mechanisms (and their extensions) describe whether or not a script can access certain data, whereas the meaningful requirement is to allow untrusted scripts access to confidential data that they need and to prevent the scripts from leaking data on the side. Motivated by this gap, we propose WebPol, a policy mechanism that allows a website developer to include fine-grained policies on confidential application data in the familiar syntax of the JavaScript programming language. The policies can be associated with any webpage element, and specify what aspects of the element can be accessed by which third-party domains. A script can access data that the policy allows it to, but it cannot pass the data (or data derived from it) to other scripts or remote hosts in contravention of the policy. To specify the policies, we expose a small set of new native APIs in JavaScript. Our policies can be enforced using any of the numerous existing proposals for information flow tracking in web browsers. We have integrated our policies into one such proposal that we use to evaluate performance overheads and to test our examples.

cs.CR↗
arXiv2017

A Relational Logic for Higher-Order Programs

Relational program verification is a variant of program verification where one can reason about two programs and as a special case about two executions of a single program on different inputs. Relational program verification can be used for reasoning about a broad range of properties, including equivalence and refinement, and specialized notions such as continuity, information flow security or relative cost. In a higher-order setting, relational program verification can be achieved using relational refinement type systems, a form of refinement types where assertions have a relational interpretation. Relational refinement type systems excel at relating structurally equivalent terms but provide limited support for relating terms with very different structures. We present a logic, called Relational Higher Order Logic (RHOL), for proving relational properties of a simply typed $λ$-calculus with inductive types and recursive definitions. RHOL retains the type-directed flavour of relational refinement type systems but achieves greater expressivity through rules which simultaneously reason about the two terms as well as rules which only contemplate one of the two terms. We show that RHOL has strong foundations, by proving an equivalence with higher-order logic (HOL), and leverage this equivalence to derive key meta-theoretical properties: subject reduction, admissibility of a transitivity rule and set-theoretical soundness. Moreover, we define sound embeddings for several existing relational type systems such as relational refinement types and type systems for dependency analysis and relative cost, and we verify examples that were out of reach of prior work.

cs.PL↗
arXiv2016

Causally consistent dynamic slicing

We offer a lattice-theoretic account of dynamic slicing for π-calculus, building on prior work in the sequential setting. For any run of a concurrent program, we exhibit a Galois connection relating forward slices of the start configuration to backward slices of the end configuration. We prove that, up to lattice isomorphism, the same Galois connection arises for any causally equivalent execution, allowing an efficient concurrent implementation of slicing via a standard interleaving semantics. Our approach has been formalised in the dependently-typed language Agda.

cs.PL↗
arXiv2015

Equivalence-based Security for Querying Encrypted Databases: Theory and Application to Privacy Policy Audits

Motivated by the problem of simultaneously preserving confidentiality and usability of data outsourced to third-party clouds, we present two different database encryption schemes that largely hide data but reveal enough information to support a wide-range of relational queries. We provide a security definition for database encryption that captures confidentiality based on a notion of equivalence of databases from the adversary's perspective. As a specific application, we adapt an existing algorithm for finding violations of privacy policies to run on logs encrypted under our schemes and observe low to moderate overheads.

cs.CR↗
arXiv2015

Generalizing Permissive-Upgrade in Dynamic Information Flow Analysis

Preventing implicit information flows by dynamic program analysis requires coarse approximations that result in false positives, because a dynamic monitor sees only the executed trace of the program. One widely deployed method is the no-sensitive-upgrade check, which terminates a program whenever a variable's taint is upgraded (made more sensitive) due to a control dependence on tainted data. Although sound, this method is restrictive, e.g., it terminates the program even if the upgraded variable is never used subsequently. To counter this, Austin and Flanagan introduced the permissive-upgrade check, which allows a variable upgrade due to control dependence, but marks the variable "partially-leaked". The program is stopped later if it tries to use the partially-leaked variable. Permissive-upgrade handles the dead-variable assignment problem and remains sound. However, Austin and Flanagan develop permissive-upgrade only for a two-point (low-high) security lattice and indicate a generalization to pointwise products of such lattices. In this paper, we develop a non-trivial and non-obvious generalization of permissive-upgrade to arbitrary lattices. The key difficulty lies in finding a suitable notion of partial leaks that is both sound and permissive and in developing a suitable definition of memory equivalence that allows an inductive proof of soundness.

cs.CR↗
arXiv2015

Program Actions as Actual Causes: A Building Block for Accountability

Protocols for tasks such as authentication, electronic voting, and secure multiparty computation ensure desirable security properties if agents follow their prescribed programs. However, if some agents deviate from their prescribed programs and a security property is violated, it is important to hold agents accountable by determining which deviations actually caused the violation. Motivated by these applications, we initiate a formal study of program actions as actual causes. Specifically, we define in an interacting program model what it means for a set of program actions to be an actual cause of a violation. We present a sound technique for establishing program actions as actual causes. We demonstrate the value of this formalism in two ways. First, we prove that violations of a specific class of safety properties always have an actual cause. Thus, our definition applies to relevant security properties. Second, we provide a cause analysis of a representative protocol designed to address weaknesses in the current public key certification infrastructure.

cs.CR↗
arXiv2015

System M: A Program Logic for Code Sandboxing and Identification

Security-sensitive applications that execute untrusted code often check the code's integrity by comparing its syntax to a known good value or sandbox the code to contain its effects. System M is a new program logic for reasoning about such security-sensitive applications. System M extends Hoare Type Theory (HTT) to trace safety properties and, additionally, contains two new reasoning principles. First, its type system internalizes logical equality, facilitating reasoning about applications that check code integrity. Second, a confinement rule assigns an effect type to a computation based solely on knowledge of the computation's sandbox. We prove the soundness of system M relative to a step-indexed trace-based semantic model. We illustrate both new reasoning principles of system M by verifying the main integrity property of the design of Memoir, a previously proposed trusted computing system for ensuring state continuity of isolated security-sensitive applications.

cs.CR↗
arXiv2014

Information Flow Control in WebKit's JavaScript Bytecode

Websites today routinely combine JavaScript from multiple sources, both trusted and untrusted. Hence, JavaScript security is of paramount importance. A specific interesting problem is information flow control (IFC) for JavaScript. In this paper, we develop, formalize and implement a dynamic IFC mechanism for the JavaScript engine of a production Web browser (specifically, Safari's WebKit engine). Our IFC mechanism works at the level of JavaScript bytecode and hence leverages years of industrial effort on optimizing both the source to bytecode compiler and the bytecode interpreter. We track both explicit and implicit flows and observe only moderate overhead. Working with bytecode results in new challenges including the extensive use of unstructured control flow in bytecode (which complicates lowering of program context taints), unstructured exceptions (which complicate the matter further) and the need to make IFC analysis permissive. We explain how we address these challenges, formally model the JavaScript bytecode semantics and our instrumentation, prove the standard property of termination-insensitive non-interference, and present experimental results on an optimized prototype.

cs.CR↗
arXiv2012

Comparative Analysis of dynamic graph techniques and data strucutre

Dynamically changing graphs are used in many applications of graph algorithms. The scope of these graphs are in graphics, communication networks and in VLSI designs where graphs are subjected to change, such as addition and deletion of edges and vertices. There is a rich body of the algorithms and data structures used for dynamic graphs. The paper overview the techniques and data structures used in various dynamic algorithms. The effort is tried to find out the comparison in these techniques namely the hierarchical decomposition of graphs and highlighting the ingenuity used in designing these algorithms.

cs.DS↗
arXiv2012

Information Retrieval on the web and its evaluation

Internet is one of the main sources of information for millions of people. One can find information related to practically all matters on internet. Moreover if we want to retrieve information about some particular topic we may find thousands of Web Pages related to that topic. But our main concern is to find relevant Web Pages from among that collection. So in this paper I have discussed that how information is retrieved from the web and the efforts required for retrieving this information in terms of system and users efforts.

cs.IR↗
arXiv2012

Online Financial Algorithms Competitive Analysis

Analysis of algorithms with complete knowledge of its inputs is sometimes not up to our expectations. Many times we are surrounded with such scenarios where inputs are generated without any prior knowledge. Online Algorithms have found their applicability in broad areas of computer engineering. Among these, an online financial algorithm is one of the most important areas where lots of efforts have been used to produce an efficient algorithm. In this paper various Online Algorithms have been reviewed for their efficiency and various alternative measures have been explored for analysis purposes.

cs.CE↗
arXiv2012

Comparison of Advance Tree Data Structures

Btree and Rtree are two basic index structures; many different variants of them are proposed after them. Different variants are used in specific application for the performance optimization. In this paper different variants of Btree and Rtree are discussed and compared. Index structures are different in terms of structure, query support, data type support and application. Index structures are discussed first. Btree and its variants are discussed and them Rtree and its variants are discussed. Some structures example is also shown for the more clear idea. Then comparison is made between all structure with respect to complexity, query type support, data type support and application.

cs.DS↗
arXiv2012

Vulnerability Management for an Enterprise Resource Planning System

Enterprise resource planning (ERP) systems are commonly used in technical educational institutions(TEIs). ERP systems should continue providing services to its users irrespective of the level of failure. There could be many types of failures in the ERP systems. There are different types of measures or characteristics that can be defined for ERP systems to handle the levels of failure. Here in this paper, various types of failure levels are identified along with various characteristics which are concerned with those failures. The relation between all these is summarized. The disruptions causing vulnerabilities in TEIs are identified .A vulnerability management cycle has been suggested along with many commercial and open source vulnerability management tools. The paper also highlights the importance of resiliency in ERP systems in TEIs.

cs.OH↗
arXiv2012

A New Middle Path Approach For Alignements In Blast

This paper deals with a new middle path approach developed for reducing alignment calculations in BLAST algorithm. This is a new step which is introduced in BLAST algorithm in between the ungapped and gapped alignments. This step of middle path approach between the ungapped and gapped alignments reduces the number of sequences going for gapped alignment. This results in the improvement in speed for alignment up to 30 percent.

cs.DS↗
arXiv2011

A Logical Method for Policy Enforcement over Evolving Audit Logs

We present an iterative algorithm for enforcing policies represented in a first-order logic, which can, in particular, express all transmission-related clauses in the HIPAA Privacy Rule. The logic has three features that raise challenges for enforcement --- uninterpreted predicates (used to model subjective concepts in privacy policies), real-time temporal properties, and quantification over infinite domains (such as the set of messages containing personal information). The algorithm operates over audit logs that are inherently incomplete and evolve over time. In each iteration, the algorithm provably checks as much of the policy as possible over the current log and outputs a residual policy that can only be checked when the log is extended with additional information. We prove correctness and termination properties of the algorithm. While these results are developed in a general form, accounting for many different sources of incompleteness in audit logs, we also prove that for the special case of logs that maintain a complete record of all relevant actions, the algorithm effectively enforces all safety and co-safety properties. The algorithm can significantly help automate enforcement of policies derived from the HIPAA Privacy Rule.

cs.LO↗