Browsing by Author "Swamy, Nikhil"
Now showing 1 - 4 of 4
Results Per Page
Sort Options
Item Defeating Script Injection Attacks with Browser Enforced Embedded Policies(2006-11-02) Trevor, Jim; Swamy, Nikhil; Hicks, MichaelWeb sites that accept and display content such as wiki articles or comments typically filter the content to prevent injected script code from running in browsers that view the site. The diversity of browser rendering algorithms and the desire to allow rich content makes filtering quite difficult, however, and attacks such as the Samy and Yamanner worms have exploited filtering weaknesses. To solve this problem, this paper proposes a simple mechanism called Browser-Enforced Embedded Policies (BEEP). The idea is that a web site can embed a policy inside its pages that specifies which scripts are allowed to run. The browser, which knows exactly when it will run a script, can enforce this policy perfectly. We have added BEEP support to several browsers, and built tools to simplify adding policies to web applications. We found that supporting BEEP in browsers requires only small and localized modifications, modifying web applications requires minimal effort, and enforcing policies is generally lightweight.Item A Distributed Algorithm for Constructing a Generalization of de Bruijn Graphs(2006-04-06) Swamy, Nikhil; Frangiadakis, Nikolaos; Bitsakos, KonstantinosDe Bruijn graphs possess many characteristics that make them a suitable choice for the topology of an overlay network. These include constant degree at each node, logarithmic diameter and a highly-regular topology that permits nodes to make strong assumptions about the global structure of the network. We propose a distributed protocol that constructs an approximation of a de Bruijn graph in the presence of an arbitrary number of nodes. We show that the degree of each node is constant and that the diameter of the network is no worse than 2logN, where N is the number of nodes. The cost of the join and the departure procedures are O(logN) in the worst case. To the best of our knowledge, this is the first distributed protocol that provides such deterministic guarantees.Item Language-based Enforcement of User-defined Security Policies (As Applied to Multi-tier Web Programs)(2008-08-25) Swamy, Nikhil; Hicks, Michael; Computer Science; Digital Repository at the University of Maryland; University of Maryland (College Park, Md.)Over the last 35 years, researchers have proposed many different forms of security policies to control how information is managed by software, e.g., multi-level information flow policies, role-based or history-based access control, data provenance management etc. A large body of work in programming language design and analysis has aimed to ensure that particular kinds of security policies are properly enforced by an application. However, these approaches typically fix the style of security policy and overall security goal, e.g., information flow policies with a goal of noninterference. This limits the programmer's ability to combine policy styles and to apply customized enforcement techniques while still being assured the system is secure. This dissertation presents a series of programming-language calculi each intended to verify the enforcement of a range of user-defined security policies. Rather than ``bake in'' the semantics of a particular model of security policy, our languages are parameterized by a programmer-provided specification of the policy and enforcement mechanism (in the form of code). Our approach relies on a novel combination of dependent types to correctly associate security policies with the objects they govern, and affine types to account for policy or program operations that include side effects. We have shown that our type systems are expressive enough to verify the enforcement of various forms of access control, provenance, information flow, and automata-based policies. Additionally, our approach facilitates straightforward proofs that programs implementing a particular policy achieve their high-level security goals. We have proved our languages sound and we have proved relevant security properties for each of the policies we have explored. To our knowledge, no prior framework enables the enforcement of such a wide variety of security policies with an equally high level of assurance. To evaluate the practicality of our solution, we have implemented one of our type systems as part of the Links web-programming language; we call the resulting language SELinks. We report on our experience using SELinks to build two substantial applications, a wiki and an on-line store, equipped with a combination of access control and provenance policies. In general, we have found the mechanisms SELinks provides to be both sufficient and relatively easy to use for many common policies, and that the modular separation of user-defined policy code permitted some reuse between the two applications.Item Toward Specifying and Validating Cross-Domain Policies(2007-04-17) Hicks, Michael; Swamy, Nikhil; Tsang, SimonFormal security policies are extremely useful for two related reasons. First, they allow a policy to be considered in isolation, separate from programs under the purview of the policy and separate from the implementation of the policy's enforcement. Second, policies can be checked for compliance against higher-level security goals by using automated analyses. By contrast, ad hoc enforcement mechanisms (for which no separate policies are specified) enjoy neither benefit, and non-formal policies enjoy the first but not the second. We would like to understand how best to define (and enforce) multi-level security policies when information must be shared across domains that have varying levels of trust (the so-called "cross domain" problem). Because we wish to show such policies meet higher-level security goals with high assurance, we are interested in specifying cross domain policies formally, and then reasoning about them using automated tools. In this report, we briefly survey work that presents formal security policies with cross-domain concerns, in particular with respect to the problem of downgrading. We also describe correctness properties for such policies, all based on noninterference. Finally, we briefly discuss recently-developed tools for analyzing formal security policies; though no existing tools focus on the analysis of downgrading-oriented policies, existing research points the way to providing such support.