Proving software free of security bugs is hard. Programming language support to ensure that programs correctly enforce their security policies would help, but, to date, no language has the ability to verify the enforcement of the kinds of policies used in practice---dynamic, stateful policies which address a broad range of concerns including forms of access control and information flow tracking.
This paper makes two main contributions. First, we present Fine, a new source-level security-typed language that, through the use of a simple module system and dependent, refinement, and affine types, can be used to check the enforcement of dynamic security policies applied to real software. Second, we define DCIL, a small extension to the type system of the .NET Common Intermediate Language, and show how to compile Fine in a type-preserving manner to DCIL. Our approach allows Fine programs to run on stock .NET virtual machines and to interface with .NET libraries. Additionally, our type-preserving compiler allows code consumers to download DCIL programs and check them for security while relying on a small trusted computing base. We have proved our source and target languages sound, our compilation type-preserving, and have made a prototype implementation of our compiler and several example programs available.

@Unpublished{sch09fine,
  AUTHOR = {Nikhil Swamy and Juan Chen and Ravi Chugh},
  TITLE = {End-to-End Verification of Security Enforcement is Fine},
  MONTH = July,
  YEAR = 2009,
  NOTE = {In submission}
}

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)},
  NOTE = {To appear}
}

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},
  NOTE = {To appear}
}

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,
  NOTE = {To appear}
}

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",
}