In the form of tools like EasyCrypt, relational program logics have been used for mechanizing formal proofs of various cryptographic constructions. With an eye towards scaling these successes towards end-to-end security proofs for implementations of distributed systems, we present rF*, a new extension of F*, a general-purpose higher-order stateful programming language with a verification system based on refinement types.

The distinguishing feature of rF* is a new probabilistic, relational Hoare logic, formalized in Coq---the first such logic for a higher-order, stateful language. We prove the soundness of this logic against a new denotational semantics for rF*, in contrast to prior operational formalizations of F*. Through careful language design, we adapt the F* typechecker to generate both classic and relational verification conditions, and to automatically discharge their proofs using an SMT solver. Thus, we are able to benefit from the existing features of F*, including, for example, its abstraction facilities that support modular reasoning about program fragments.

We evaluate F* experimentally by programming a series of cryptographic constructions and protocols, and by verifying their security properties, ranging from information flow to unlinkability, integrity, and privacy.

From their semantic origins to their use in structuring effectful computations, monads are now also used as a programming pattern to structure code in a number of important scenarios, including functional reactivity, information flow tracking and probabilistic computation. However, whilst these examples are inspired by monads they are not strictly speaking monadic but rather something more general. The first contribution of this paper is the definition of a new structure, the polymonad, which subsumes monads and encompasses the monad-like programming patterns that we have observed. A concern is that given such a general setting, a program would quickly become polluted with polymonadic coercions, making it hard to read and maintain. The second contribution of this paper is to build on previous work to define a polymorphic type inference algorithm that supports programming with polymonads using a direct style, e.g., as if computations of type $M\, \tau$ were expressions of type $\tau$. During type inference the program is rewritten to insert the necessary polymonadic coercions, a process that we prove is coherent---all sound rewritings produce programs with the same semantics. The resulting programming style is powerful and lightweight.

@techreport{polymonads,
 author={Nataliya Guts and Michael Hicks and Nikhil Swamy and Daan Leijen and Gavin Bierman},
 Institution={{UMD}}, 
 title={Polymonads},
 year=2012}

Modern programming languages, ranging from Haskell and ML, to JavaScript, C# and Java, all make extensive use of higher-order state. This paper advocates a new verification methodology for higher-order stateful programs, based on a new monad of predicate transformers called the Dijkstra monad.

Using the Dijkstra monad has a number of benefits. First, the monad naturally yields a weakest pre-condition calculus. Second, the computed specifications are structurally simpler in several ways, e.g., single-state post-conditions are sufficient (rather than the more complex two-state post-conditions). Finally, the monad can easily be varied to handle features like exceptions and heap invariants, while retaining the same type inference algorithm.

We implement the Dijkstra monad and its type inference algorithm for the F* programming language. Our most extensive case study evaluates the Dijkstra monad and its F* implementation by using it to verify JavaScript programs.

Specifically, we describe a tool chain that translates programs in a subset of JavaScript decorated with assertions and loop invariants to F*. Once in F*, our type inference algorithm computes verification conditions and automatically discharges their proofs using an SMT solver. We use our tools to prove that a core model of the JavaScript runtime in F* respects various invariants and that a suite of JavaScript source programs are free of runtime errors.

@InProceedings{dijkstramonad2013,
  author={Nikhil Swamy and Joel Weinberger and Cole Schlesinger and Juan Chen and Benjamin Livshits},
  title={Verifying Higher-order Programs with the Dijkstra Monad},
  MONTH = June,
  YEAR = 2013,
  BOOKTITLE = {In Proceedings of the ACM Conference on Programming Languages Design and Implementation (PLDI) 2013}
}

Many prior trust management frameworks provide authorization logics for specifying policies based on distributed trust. However, to implement a security protocol using these frameworks, one usually resorts to a general-purpose programming language. When reasoning about the security of the entire system, one must study both policies in the authorization logic as well as hard-to-analyze implementation code.

This paper proposes DKAL*, a language for constructing executable specifications of authorization protocols. Protocol and policy designers can use DKAL*'s authorization logic for expressing distributed trust relationships, and its small rule-based programming language to describe the message sequence of a protocol. Importantly, many low-level details of the protocol (e.g., marshaling formats, management of state consistency etc.) are left abstract in DKAL*, but sufficient details must be provided in order for the protocol to be executable.

We formalize the semantics of DKAL*, giving it both an operational semantics and a type system. We prove various properties of DKAL*, including type soundness and a decidability property for its underlying logic. We also present an interpreter for DKAL*, mechanically verified for correctness and security. We evaluate our work experimentally on several examples.

Using our semantics, DKAL* programs can be analyzed for various protocol-specific properties of interest. Using our interpreter, programmers obtain an executable version of their protocol which can readily be tested and then deployed.

@InProceedings{dkalstar2012,
  author={Jean-Baptiste Jeannin and Guido de Caso and Juan Chen and Yuri Gurevich and Prasad Naldurg and Nikhil Swamy},
  title={DKAL*: Constructing Executable Specifications of Authorization Protocols},
  MONTH = February,
  YEAR = 2013,
  BOOKTITLE = {In Proceedings of the International Symposium on Engineering Secure Software and Systems (ESSoS) 2013}
}

Programming language researchers can accelerate their ability to learn and explore new language ideas by exposing their new languages to users via web technologies, to observe and test the interactions between humans and compilers.

Many tools allow programmers to develop applications in high-level languages and deploy them in web browsers via compilation to JavaScript. While practical and widely used, these compilers are ad hoc. No guarantee is provided on their correctness for whole programs, nor their security for programs executed within arbitrary JavaScript contexts.

In this paper, we present a compiler with such positive guarantees. We compile an ML-like language with higher-order functions and references down to JavaScript, while preserving all source program properties. We evaluate our compiler on sample programs, including a series of secure libraries.

We illustrate the dangers of JavaScript contexts with a series of attacks against naive scripts. We then give a semantics to JavaScript by translation to F*, a variant of ML with richer types. Based on lambdaJS, this semantics reflects the main elements of the EcmaScript 5 standard, as well as our experimental findings on dangerous features in JavaScript implementations (implicit coercions, getters and setters, and special arguments, caller, and callee properties).

We present our compilation scheme, expressed as a type-preserving translation between fragments of F*: each source type is mapped to `dyn', the type of Javascript values, refined with a logical specification of its compiled representation.

For whole programs, we show that the translation is a forward simulation. For programs executed in untrusted Javascript contexts, we wrap our translation with defensive filters to import and export values while preserving the translation invariant. Relying on type-based invariants and a new notion of applicative bisimilarity, we show full abstraction: two programs are equivalent in all source contexts if and only if their wrapped translations are equivalent in all Javascript contexts. Thus, programmers can produce JavaScript and still rely on static scopes and types for reasoning about their programs.

@InProceedings{full-abs-js13,
  author={Cedric Fournet and Nikhil Swamy and Juan Chen and Pierre-Evariste Dagand and Pierre-Yves Strub and Ben Livshits}, 
  title={Fully Abstract Compilation to JavaScript},
  MONTH = January,
  YEAR = 2013,
  BOOKTITLE = {In Proceedings of the ACM Symposium on Principles of Programming Languages (POPL) (To appear)}
}

Well-established dependently-typed languages like Agda and Coq provide reliable ways to build and check formal proofs. Several other dependently-typed languages such as Aura, ATS, Cayenne, Epigram, F*, F7, Fine, Guru, PCML5, and Ur also explore reliable ways to develop and verify programs. All these languages shine in their own regard, but their implementations do not themselves enjoy the degree of safety provided by machine-checked verification.

We propose a general technique called self-certification that allows a typechecker for a suitably expressive language to be certified for correctness. We have implemented this technique for F*, a dependently typed language on the .NET platform. Self-certification involves implementing a typechecker for F* in F*, while using all the conveniences F* provides for the compiler-writer (e.g., partiality, effects, implicit conversions, proof automation, libraries). This typechecker is given a specification (in~F*) strong enough to ensure that it computes valid typing derivations. We obtain a typing derivation for the core typechecker by running it on itself, and we export it to Coq as a type-derivation certificate. By typechecking this derivation (in Coq) and applying the F* metatheory (also mechanized in Coq), we conclude that our type checker is correct. Once certified in this manner, the F* typechecker is emancipated from Coq.

Self-certification leads to an efficient certification scheme---we no longer depend on verifying certificates in Coq---as well as a more broadly applicable one. For instance, the self-certified F* checker is suitable for use in adversarial settings where Coq is not intended for use, such as run-time certification of mobile code.

@InProceedings{ssfc11bootstrap,
  AUTHOR = {Pierre-Yves Strub and Nikhil Swamy and Cedric Fournet and Juan Chen}, 
  TITLE = {Self-certification: Bootstrapping certified typechecekrs in F* with Coq}, 
  MONTH = January,
  YEAR = 2012,
  BOOKTITLE = {In Proceedings of the ACM Symposium on Principles of Programming Languages (POPL)}
}

Many useful programming constructions can be expressed as monads. Examples include support for probabilistic computations, time-varying expressions, parsers, and information flow tracking, not to mention effectful features like state and I/O. In this paper, we present a type-based rewriting algorithm to make programming with arbitrary monads as easy as using ML's built-in support for state and I/O. Programmers write programs using monadic values of type M t as if they were of type t, and our algorithm inserts the necessary binds, units, and monad-to-monad morphisms so that the program typechecks. Our algorithm is based on Jones' qualified types and enjoys three useful properties: (1) principal types, i.e., the rewriting we perform is the most general; (2) coherence, i.e., thanks to the monad and morphism laws, all instances of the principal rewriting have the same semantics; (3) decidability; i.e., the solver for generated constraints will always terminate. Throughout the paper we present simple examples from the domains listed above. Our most complete example, which illustrates the expressive power of our system, proves that ML programs rewritten by our algorithm to use the information flow monad are equivalent to programs in FlowCaml, a domain-specific information flow tracking language.

@TechReport{sglh11monadic,
  AUTHOR = {Nikhil Swamy and Nataliya Guts and  Daan Leijen and Michael Hicks}, 
  TITLE = {Lightweight Monadic Programming in ML}, 
  MONTH = March,
  YEAR = 2011,
  INSTITUTION = {Microsoft Research}, 
  NOTE = {MSR-TR-2011-39}
}

Distributed applications are difficult to program reliably and securely. Dependently typed functional languages promise to prevent broad classes of errors and vulnerabilities, and to enable program verification to proceed side-by-side with development. However, as recursion, effects, and rich libraries are added, using types to reason about programs, specifications and proofs becomes challenging.

We present F*, a full-fledged design and implementation of a new dependently typed language for secure distributed programming. Unlike prior languages, F* provides arbitrary recursion while maintaining a logically consistent core; it enables modular reasoning about state and other effects using affine types; and it supports proofs of refinement properties using a mixture of cryptographic evidence and logical proof terms. The key mechanism is a new kind system that tracks several sub-languages within F* and controls their interaction. F* subsumes two previous languages, F7 and Fine. We prove type soundness (with proofs partially mechanized in Coq) and logical consistency for F*.

We have implemented a compiler that translates F* to .NET bytecode, based on a prototype for Fine. F* provides access to libraries for concurrency, networking, cryptography, and interoperability with C#, F# and the other .NET languages. The compiler produces verifiable binaries with 60% code size overhead for proofs and types, as much as a 45x improvement over the Fine compiler, while still enabling efficient bytecode verification.

To date, we have programmed and verified more than 17,000 lines of F* including (1) new schemes for multi-party sessions; (2) a new zero-knowledge privacy-preserving payment protocol; (3) a provenance aware curated database; (4) a suite of 17 web-browser extensions verified for authorization properties; and (5) a cloud-hosted multi-tier web application with a verified reference monitor.

@inproceedings{fstar-icfp11,
  author    = {Nikhil Swamy and
               Juan Chen and
               C{\'e}dric Fournet and
               Pierre-Yves Strub and
               Karthikeyan Bhargavan and
               Jean Yang},
  title     = {Secure distributed programming with value-dependent types},
  booktitle = {Proceeding of the 16th ACM SIGPLAN international conference
               on Functional Programming, ICFP 2011, Tokyo, Japan, September
               19-21, 2011},
  year      = {2011},
  pages     = {266-278},
  ee        = {http://doi.acm.org/10.1145/2034773.2034811},
}

This paper introduces Yarra, a conservative extension to C to protect applications from non-control data attacks. Yarra programmers specify their data integrity requirements by declaring critical data types and ascribing these critical types to important data structures. Yarra guarantees that such critical data is only written through pointers with the given static type. Any attempt to write to critical data through a pointer with an invalid type (perhaps because of a buffer overrun) is detected dynamically. We formalize Yarra's semantics and prove the soundness of a program logic designed for use with the language. A key contribution is to show that Yarra's semantics are strong enough to support sound local reasoning and the use of a frame rule, even across calls to unknown, unverified code. We evaluate a prototype implementation of a compiler and runtime system for Yarra by using it to harden four common server applications against known non-control data vulnerabilities. We show that Yarra defends against these attacks with only a negligible impact on their end-to-end performance.

@InProceedings{sps11yarra, 
  AUTHOR = {Cole Schlesinger, Karthik Pattabiraman, Nikhil Swamy, David Walker and Ben Zorn, 
  TITLE = {Modular Protections Against Non-control Data Attacks},
  MONTH = June,
  YEAR = 2011,
  BOOKTITLE = {In Proceedings of the IEEE Symposium on Computer Security Foundations (CSF)}
}

Popup blocking, form filling, and many other features of modern web browsers were first introduced as third-party extensions. New extensions continue to enrich browsers in unanticipated ways. However, powerful extensions require capabilities, such as cross-domain network access and local storage, which, if used improperly, pose a security risk. Several browsers try to limit extension capabilities, but an empirical survey we conducted shows that many extensions are over-privileged under existing mechanisms.

This paper presents a comprehensive new model for extension security that aims to redress the shortcomings of existing extension mechanisms. Our model includes various components. First, we develop a logic-based specification language for describing fine-grained access control and data flow policies that govern an extension's privilege over web content. We show how to understand security policies by providing visualization tools that highlight the impact of a policy on particular web pages. We formalize the semantics of policies in terms of a safety property on the execution of extensions and we develop a verification methodology that allows us to statically check extensions for safety. Static verification eliminates the need for costly runtime monitoring, and increases robustness since verified extensions cannot raise security exceptions. We also provide compiler tools to translate extension code authored in ML to either .NET or JavaScript, facilitating cross-browser deployment of extensions.

We evaluate our work by implementing and verifying 17 extensions with a diverse set of features and security policies. We deploy our extensions in Internet Explorer, Chrome, Firefox, and a new experimental HTML5 platform called C3. In so doing, we demonstrate the versatility and effectiveness of our approach.

@InProceedings{gfls11ibx, 
  AUTHOR = {Arjun Guha and Matthew Fredrikson and Benjamin Livshits and Nikhil Swamy}, 
  TITLE = {Verified Security for Browser Extensions},
  MONTH = May,
  YEAR = 2011,
  BOOKTITLE = {In Proceedings of the IEEE Symposium on Security and Privacy (Oakland)}
}

A variety of techniques have been proposed to verify stateful functional programs by developing Hoare logics for the state monad. For better automation, we explore a different point in the design space: we propose using affine types to model state, while relying on refinement type checking to prove assertion safety.

Our technique is based on verification by translation, starting from FX, an imperative object-based surface language with specifications including object invariants and Hoare triple computation types, and translating into Fine, a functional language with dependent refinements and affine types. The core idea of the translation is the division of a stateful object into a pure value and an affine token whose type mentions the current state of the object. We prove our methodology sound via a simulation between imperative FX programs and their functional Fine translation.

Our approach enables modular verification of FX programs supported by an SMT solver. We demonstrate its versatility by several examples, including verifying clients of stateful APIs, even in the presence of aliasing, and tracking information flow through side-effecting computations.

@InProceedings{bcs11fx,
  AUTHOR = {Johannes Borgstrom and Juan Chen and Nikhil Swamy},
  TITLE = {Verifying Stateful Programs with Substructural State and Hoare Types}, 
  MONTH = January,
  YEAR = 2011,
  BOOKTITLE = {In Proceedings of the ACM SIGPLAN Workshop on Programming Languages meet Program Verification (PLPV)}
}

A number of programming languages use rich type systems to verify security properties of code. Some of these languages are meant for source programming, but programs written in these languages are compiled without explicit security proofs, limiting their utility in settings where proofs are necessary, e.g., proof-carrying authorization. Others languages do include explicit proofs, but these are generally lambda calculi not intended for source programming, that must still be compiled further to be executable on real computers. A language suitable for source programming backed by a compiler that enables end-to-end verification is missing.

In this paper, we present a type-preserving compiler that translates programs written in Fine, a source-level functional language with dependent refinements and affine types, to DCIL, a new extension of the .NET Common Intermediate Language. Fine is type checked using an external SMT solver to reduce the proof burden on source programmers. We extract explicit LCF-style proof terms from the solver and carry these proof terms in the compilation to DCIL, thereby removing the solver from the trusted computing base. Explicit proofs enable DCIL to be used in a number of important scenarios, including the verification of mobile code, proof-carrying authorization, and evidence-based auditing. We report on our experience using Fine to build reference monitors for several applications, ranging from a plugin-based email client to a conference management server.

@InProceedings{ccs10fine,
  AUTHOR = {Juan Chen and Ravi Chugh and Nikhil Swamy},
  TITLE = {Type-preserving Compilation for End-to-end Verification of Security Enforcement},
  MONTH = June,
  YEAR = 2010,
  BOOKTITLE = {In Proceedings of the ACM SIGPLAN Conference on Programming Language Design and Implementation (PLDI)}
}

Proving software free of security bugs is hard. Languages that ensure that programs correctly enforce their security policies would help, but, to date, no security-typed language has the ability to verify the enforcement of the kinds of policies used in practice---dynamic, stateful policies which address a range of concerns including forms of access control and information flow tracking.

This paper presents Fine, a new source-level security-typed language that, through the use of a simple module system and dependent, refinement, and affine types, checks the enforcement of dynamic security policies applied to real software. Fine is proven sound. A prototype implementation of the compiler and several example programs are available from here.

@InProceedings{scc10fine,
  AUTHOR = {Nikhil Swamy and Juan Chen and Ravi Chugh},
  TITLE = {Enforcing Stateful Authorization and Information Flow Policies in Fine}, 
  MONTH = March,
  YEAR = 2010,
  BOOKTITLE = {In Proceedings of the European Symposium on Programming (ESOP)}, 
}

A number of important program rewriting scenarios can be recast as type-directed coercion insertion. These range from more theoretical applications such as coercive subtyping and supporting overloading in type theories, to more practical applications such as integrating static and dynamically typed code using gradual typing, and inlining code to enforce security policies such as access control and provenance tracking. In this paper we give a general theory of type-directed coercion insertion based on generating and inserting coercions. We specifically explore the inherent tradeoff between expressiveness and ambiguity---the more powerful the strategy for generating coercions, the greater the possibility of several, semantically distinct rewritings for a given program. We consider increasingly powerful coercion generation strategies, work out example applications supported by the increased power (including those mentioned above), and identify the inherent ambiguity problems of each setting, along with various techniques to tame the ambiguities.

@InProceedings{shb09coercions,
  AUTHOR = {Nikhil Swamy and Michael Hicks and Gavin Bierman},
  TITLE = {A Theory of Typed Coercions and its Applications},
  MONTH = March,
  YEAR = 2009,
  BOOKTITLE = {Proceedings of the {ACM} International Conference on Functional Programming (ICFP)},
}

This paper presents SELinks, a programming language focused on building secure multi-tier web applications. SELinks provides a uniform programming model, in the style of LINQ and Ruby on Rails, with language syntax for accessing objects residing either on the database or at the server. Object-level security policies are expressed as labels, which are themselves fully-customizable, first-class objects. Access to labeled data is mediated via trusted, user-provided policy enforcement functions.

SELinks has two novel features that ensure security policies are enforced correctly and efficiently. First, SELinks uses a novel type system that allows a protected object's type to refer to its protecting label. This way, the type system can check that labeled data is never accessed directly by the program without first passing through the appropriate policy enforcement function. Second, SELinks compiles policy enforcement code to database-resident user-defined functions, which can be called directly during query processing. Database-side checking avoids transferring data to the server needlessly, while still allowing policies to be expressed in a customizable and portable manner.

Our experience with two sizeable web applications, a model health-care database and a secure wiki with fine-grained security policies, indicates that cross-tier policy enforcement in SELinks is flexible, relatively easy to use, and, when compared to a single-tier approach, improves throughput by nearly an order of magnitude.

@InProceedings{corcoran09selinks,
  AUTHOR = {Brian J. Corcoran and Nikhil Swamy and Michael Hicks},
  TITLE = {Cross-tier, Label-based Security Enforcement for Web Applications},
  MONTH = July,
  YEAR = 2009,
  BOOKTITLE = {Proceedings of the {ACM SIGMOD} International Conference on the Management of Data},
}

Many organizations specify information release policies to describe the terms under which sensitive information may be released to other organizations. This paper presents a new approach for ensuring that security-critical software correctly enforces its information release policy. Our approach has two parts. First, an information release policy is specified as a security automaton written in a new language called AIR. Second, we enforce an AIR policy by translating it into an API for programs written in LAIR, a core formalism for a functional programming language. LAIR uses a novel combination of dependent, affine, and singleton types to ensure that the API is used correctly. As a consequence we can certify that programs written in LAIR meet the requirements of the original AIR policy specification.

@INPROCEEDINGS{swamy08lair,
  AUTHOR = {Nikhil Swamy and Michael Hicks},
  TITLE = {Verified Enforcement of Stateful Information Release Policies},
  MONTH = JUN,
  YEAR = 2008,
  BOOKTITLE = {Proceedings of the {ACM SIGPLAN} Workshop on Programming Langauges and Analysis for Security (PLAS)},
}

This paper presents Fable, a core formalism for a programming language in which programmers may specify security policies and reason that these policies are properly enforced. In Fable, security policies can be expressed by associating security labels with the data or actions they protect. Programmers define the semantics of labels in a separate part of the program called the enforcement policy. Fable prevents a policy from being circumvented by allowing labeled terms to be manipulated only within the enforcement policy; application code must treat labeled values abstractly. Together, these features facilitate straightforward proofs that programs implementing a particular policy achieve their high-level security goals. Fable is flexible enough to implement a wide variety of security policies, including access control, information flow, provenance, and security automata. We have implemented Fable 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. To our knowledge, no existing framework enables the enforcement of such a wide variety of security policies with an equally high level of assurance.

@INPROCEEDINGS{swamy08fable,
  AUTHOR = {Nikhil Swamy and Brian Corcoran and Michael Hicks},
  TITLE = {Fable: A Language for Enforcing User-defined Security Policies},
  BOOKTITLE = {Proceedings of the {IEEE} Symposium on Security and Privacy (Oakland)},
  MONTH = MAY,
  YEAR = 2008,
}

We describe reference implementations for selected configurations of the user authentication protocol defined by the Information Card Profile V1.0. Our code can interoperate with existing implementations of the roles of the protocol (client, identity provider, and relying party). We derive formal proofs of security properties for our code using an automated theorem prover. Hence, we obtain the most substantial examples of verified implementations of cryptographic protocols to date, and the first for any federated identity-management protocols. Moreover, we present a tool that downloads security policies from services and identity providers and compiles them to a verifiably secure client proxy.

@inproceedings{wcf-cardspace-asiaccs08,
  author = {Karthikeyan Bhargavan and C\'edric Fournet and Andrew D. Gordon and Nikhil Swamy},
  title = {Verified Implementations of the {I}nformation {C}ard Federated Identity-Management Protocol},
  pages = "123--135",
  crossref = "asiaccs08",
  abstract = "We describe reference implementations for selected configurations of
  the user authentication protocol defined by the Information Card Profile V1.0.
  Our code can interoperate with existing implementations of the
  roles of the protocol (client, identity provider, and relying party).
  We derive formal proofs of security properties for our code using an
  automated theorem prover.
  Hence, we obtain the most substantial examples of verified implementations
  of cryptographic protocols to date, and the first for any federated
  identity-management protocols.
  Moreover, we present a tool that downloads security policies from
  services and identity providers and compiles them to a verifiably secure
  client proxy."}

@proceedings{asiaccs08,
 title = "Proceedings of the ACM Symposium on Information, Computer and Communications Security (ASIACCS'08)",
 booktitle = "Proceedings of the ACM Symposium on Information, Computer and Communications Security (ASIACCS'08)",
  month = mar,
  year = 2008,
  publisher = {ACM Press},
  address = {Tokyo, Japan}
}

Web 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 make filtering quite difficult, however, and attacks such as the Samy and Yamanner worms have exploited filtering weaknesses. This paper proposes a simple alternative mechanism for preventing script injection called Browser-Enforced Embedded Policies (BEEP). The idea is that a web site can embed a policy in 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.

@INPROCEEDINGS{jim07beep,
  AUTHOR = {Trevor Jim and Nikhil Swamy and Michael Hicks},
  TITLE = {Defeating Script Injection Attacks with Browser-Enforced Embedded Policies},
  BOOKTITLE = {Proceedings of the International World Wide Web Conference (WWW)},
  PAGES = {601--610},
  MONTH = MAY,
  YEAR = 2007,
  LOCATION = {Banff, Alberta, Canada}
}

This paper presents RX, a new security-typed programming language with features intended to make the management of information-flow policies more practical. Security labels in RX, in contrast to prior approaches, are defined in terms of owned roles, as found in the RT role-based trust-management framework. Role-based security policies allows flexible delegation, and our language RX provides constructs through which programs can robustly update policies and react to policy updates dynamically. Our dynamic semantics use statically verified transactions to eliminate illegal information flows across updates, which we call transitive flow. Because policy updates can be observed through dynamic queries, policy updates can potentially reveal sensitive information. As such, RX considers policy statements themselves to be potentially confidential information and subject to information-flow metapolicies.

@INPROCEEDINGS{swamy06rx,
  TITLE = {Managing Policy Updates in Security-Typed Languages},
  AUTHOR = {Nikhil Swamy and Michael Hicks and Stephen Tse and Steve Zdancewic},
  BOOKTITLE = {Proceedings of the Computer Security Foundations Workshop (CSFW)},
  MONTH = {July},
  PAGES = {202--216},
  YEAR = 2006,
  HTTP = {http://www.cs.umd.edu/projects/PL/rx/}
}

Software systems obey the 80/20 rule: aggressively optimiz- ing a vital few execution paths yields large speedups. However, find- ing the vital few paths can be difficult, especially for large systems like web applications. This paper describes a novel approach to finding bot- tlenecks in such systems, given (possibly very large) profiles of system executions. In the approach, for each kind of profile (for example, call- tree profiles), a tool developer implements a simple profile interface that exposes a small set of primitives for selecting summaries of profile mea- surements and querying how summaries overlap. Next, an analyst uses a search tool, which is written to the profile interface and thus independent of the kind of profile, to find bottlenecks. Our search tool (Bottlenecks) manages the bookkeeping of the search for bottlenecks and provides heuristics that automatically suggest likely bottlenecks. In one case study, after using Bottlenecks for half an hour, one of the authors found 14 bottlenecks in IBM's WebSphere Ap- plication Server. By optimizing some of these bottlenecks, we obtained a throughput improvement of 23% on the Trade3 benchmark. The opti- mizations include novel optimizations of J2EE and Java security, which exploit the high temporal and spatial redundancy of security checks.

@InProceedings{ammons04bottlenecks,
  author = 	 {Glenn Ammons and Jong-Deok Choi and Manish Gupta and Nikhil Swamy},
  title = 	 {Finding and Removing Performance Bottlenecks in Large Systems},
  booktitle =	 {European Conference on Object-Oriented Programming (ECOOP)},
  year =	 2004
}

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.

@PhdThesis{swamy08thesis,
  author = 	 {Nikhil Swamy},
  title = 	 {Language-based Enforcement of User-defined Security Policies},
  note = 	 {As Applied to Multi-tier Web Programs},
  school = 	 {University of Maryland, College Park},
  year = 	 2008,
  month = 	 {August},
}

The goal of the Cyclone project is to investigate how to make a low-level C-like language safe. Our most difficult challenge has been providing programmers control over memory management while retaining safety. This paper describes our experience trying to integrate and use effectively two previously-proposed, safe memory-management mechanisms: statically-scoped regions and tracked pointers. We found that these typing mechanisms can be combined to build alternative memory-management abstractions, such as reference counted objects and arenas with dynamic lifetimes, and thus provide a flexible basis. Our experience-porting C programs and device drivers, and building new applications for resource-constrained systems-confirms that experts can use these features to improve memory footprint and sometimes to improve throughput when used instead of, or in combination with, conservative garbage collection.

@ARTICLE{swamy05experience,
  AUTHOR = {Nikhil Swamy and Michael Hicks and Greg Morrisett and Dan Grossman and Trevor Jim},
  TITLE = {Safe Manual Memory Management in {Cyclone}},
  JOURNAL = {Science of Computer Programming (SCP)},
  VOLUME = 62,
  NUMBER = 2,
  MONTH = OCT,
  PAGES = {122--144},
  YEAR = 2006,
  NOTE = {Special issue on memory management.x},
  PUBLISHER = {Elsevier},
  HTTP = {http://cyclone.thelanguage.org}
}

We present an FindLocks, an approach for automatically proving the absence of data races in multi-threaded Java programs, using a combination of dynamic and static analysis. The program in question is instrumented so that when executed it will gather information about locking relationships. This information is then used to automatically generate annotations needed to type check the program using the Race-Free Java type system. Programs that type check are sure to be free from races. We call this technique dynamic annotation inference. We describe the design and implementation of our approach, and our experience applying the tool to a variety of Java programs. We have found that when using a reasonably comprehensive test suite, which is easy for small programs but harder for larger ones, the approach generates useful annotations.

@ARTICLE{rose05scp,
  AUTHOR = {James Rose and Nikhil Swamy and Michael Hicks},
  TITLE = {Dynamic Inference of Polymorphic Lock Types},
  JOURNAL = {Science of Computer Programming (SCP)},
  VOLUME = 58,
  NUMBER = 3,
  PAGES = {366--383},
  MONTH = {December},
  YEAR = 2005,
  NOTE = {Special Issue on Concurrency and Synchronization in Java programs.  Supercedes 2004 CSJP paper of the same name.},
  PUBLISHER = {Elsevier}
}

Quantum computers are computational devices that use the dynamics of atomic-scale objects to store and manipulate information. Only a few, small-scale quantum computers have been built to date, but quantum computers can in principle outperform all possible classical computers in significant ways. Quantum computation is therefore a subject of considerable theoretical interest that may also have practical applications in the future.

Genetic programming can automatically discover new algorithms for quantum computers [spector:1998:GPqc]. We describe how to simulate a quantum computer so that the fitness of a quantum algorithm can be determined on classical hardware. We then describe ways in which three different genetic programming approaches can drive the simulator to evolve new quantum algorithms. The approaches are standard tree-based genetic programming, stack-based linear genome genetic programming, and stackless linear genome genetic programming. We demonstrate the techniques on four different problems: the two-bit early promise problem, the scaling majority-on problem, the four-item database search problem, and the two-bit and-or problem. For three of these problems (all but majority-on) the automatically discovered algorithms are more efficient than any possible classical algorithms for the same problems. One of the better-than-classical algorithms (for the two-bit and-or problem) is in fact more efficient than any previously known quantum algorithm for the same problem, suggesting that genetic programming may be a valuable tool in the future study of quantum programming.

@InCollection{	  spector99aigp3,
  author	= "Lee Spector and Howard Barnum and Herbert J. Bernstein and
		  Nikhil Swamy",
  title		= "Quantum Computing Applications of Genetic Programming",
  booktitle	= "Advances in Genetic Programming 3",
  publisher	= "MIT Press",
  year		= "1999",
  editor	= "Lee Spector and William B. Langdon and Una-May O'Reilly
		  and Peter J. Angeline",
  chapter	= "7",
  pages		= "135--160",
  address	= "Cambridge, MA, USA",
  month		= jun,
  keywords	= "genetic algorithms, genetic programming",
  isbn		= "0-262-19423-6",
  url		= "http://www.cs.bham.ac.uk/~wbl/aigp3/ch07.pdf",
  notes		= "AiGP3"
}

Provenance and security are intimately related. Cheney et al. show that the dependencies underlying provenance information also underly information flow security policies. Provenance information can also play a role in history-based access control policies. Many real applications have the need to combine a variety of security policies with provenance tracking. For instance, an online stock trading website might restrict access to certain premium features it offers using an access control policy, while at the same time using an information flow policy to ensure that a user's sensitive trading information is not leaked to other users. Similarly, the application might need to track the provenance of transaction information to support an annual financial audit while also using provenance to attest to the reliability of stock analyses that it presents to its users.

We have been exploring the interaction between provenance and security policies while developing a document management system we call the Collaborative Planning Application (CPA). The CPA is written in SELinks, our language for supporting user-defined, label-based security policies. SELinks is an extension of the Links web-programming language with means to express label-based security policies. Labels are associated with the data they protect by using dependent types which, along with some syntactic restrictions, suffice to ensure that user-defined policies enjoy complete mediation and cannot be circumvented. Our interest in provenance and security policies is thus part of a broader exploration of how security policies can be encoded, composed, and reasoned about within SELinks. In this paper, we describe the architecture of the CPA and its approach to label-based provenance and security policies and we sketch directions for further exploration on the interaction between the two.

@INPROCEEDINGS{corcoran07provenance,
  AUTHOR = {Brian Corcoran and Nikhil Swamy and Michael Hicks},
  TITLE = {Combining Provenance and Security Policies in a Web-based
    Document Management System},
  BOOKTITLE = {On-line Proceedings of the Workshop on Principles of Provenance (PrOPr)},
  NOTE = {\url{http://homepages.inf.ed.ac.uk/jcheney/propr/}},
  LOCATION = {Edinburgh, Scotland, UK},
  MONTH = NOV,
  YEAR = 2007
}

We describe work in progress that uses program analysis to show that security-critical programs, such as cross-domain guards, correctly enforce cross-domain security policies. We are enhancing existing techniques from the field of security-oriented programming languages to construct a new language for the construction of secure networked applications, SELinks. In order to specify and enforce expressive and fine-grained policies, we advocate dynamically associating security labels with sensitive entities. Programs written in SELinks are statically guaranteed to correctly manipulate an entity's security labels and to ensure that the appropriate policy checks mediate all operations that are performed on the entity. We discuss the design of our main case study: a web-based collaborative planning application that will permit a collection of users, with varying security requirements and clearances, to access sensitive data sources and collaboratively create documents based on these sources.

@INPROCEEDINGS{swamy07milcom,
  AUTHOR = {Nikhil Swamy and Michael Hicks and Simon Tsang},
  TITLE = {Verified Enforcement of Security Policies for Cross-Domain
Information Flows},
  MONTH = OCT,
  YEAR = 2007,
  BOOKTITLE = {Proceedings of the 2007 Military Communications Conference (MILCOM)}
}

We present an approach for automatically proving the absence of race conditions in multi-threaded Java programs, using a combination of dynamic and static analysis. The program in question is instrumented so that when executed it will gather information about locking relationships. This information is then fed to our tool, FindLocks, that generates annotations needed to type check the program using the Race-Free Java type system. Our approach extends existing inference algorithms by being fully context-sensitive. We describe the design and implementation of our approach, and our experience applying the tool to a variety of Java programs. In general, we have found the approach works well, but has trouble scaling to large programs, which require extensive testing for full coverage.

@INPROCEEDINGS{rose04dynamic,
  AUTHOR = {James Rose and Nikhil Swamy and Michael Hicks},
  TITLE = {Dynamic Inference of Polymorphic Lock Types},
  BOOKTITLE = {Proceedings of the {ACM} Conference on Principles of Distributed Computing (PODC) Workshop on Concurrency and Synchronization in Java Programs (CSJP)},
  PAGES = {18--25},
  MONTH = {July},
  YEAR = 2004
}

Our work focuses on the study of learning paradigms within a hybrid reasoning system, consisting of a Neural Network and Symbolic Reasoner. There are several aspects to this problem that invite comparisons to work in other fields of study involving for example, knowledge representation, behavioral modeling, and neuromorphic engineering. Central to this paper is a discussion on the coupling between a particular learning paradigm and the behaviors that a real-time system develops in attempting to achieve a specific goal.

@InProceedings{hennacy03rgl,
  author = 	 {Ken Hennacy and Nikhil Swamy and Don Perlis},
  title = 	 {{RGL} Study in Hybrid Real-Time Systems},
  booktitle =	 {Neural Networks and Computational Intelligence},
  year =	 2003
}

This paper documents the discovery of a new, better-than-classical quantum algorithm for the depth- two AND/OR tree problem. We describe the genetic pro- gramming system that was constructed specifically for this work, the quantum computer simulator that is used to evaluate the fitness of evolving quantum algorithms, and the newly discovered algorithm.

@InProceedings{spector99andor,
  author = 	 {Lee Spector and Howard Barnum and Herbert J. Bernstein and Nikhil Swamy},
  title = 	 {Finding a Better-than-classical Quantum AND/OR Algorithm},
  booktitle =	 {Proceedings of the Congress of Evolutionary Computation},
  year =	 1999
}

De 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.

@techreport{swamy06halo,
  title = "A Distributed Algorithm for Constructing a Generalization of de Bruijn Graphs",
  author = "Nikhil Swamy and Konstantinos Bitsakos and Nikolaos Frangiadakis",
  institution = {Department of Computer Science, University of Maryland},
  number = "CS-TR-4792",
  month = "August",
  year = 2006,
  url = {http://hdl.handle.net/1903/3682},
  category = "Networks, Algorithms",
}