Research
I've been working on my Ph.D. since Fall 2006. My advisor is Dr. Michael Hicks in the programming language research group. I'm currently working with Nik Swamy on SELinks, a secure web programming language.
Publications
Conference Papers
-
Fable : A Language for Enforcing
User-defined Security Policies
Nikhil Swamy, Brian Corcoran, and Michael Hicks.
IEEE Symposium on Security and Privacy, May 2008 (To appear).
[ abstract ]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.
Workshop Papers
-
Combining Provenance and Security Policies in a Web-based
Document Management System (Extended abstract)
Brian Corcoran, Nikhil Swamy, and Michael Hicks.
In On-line Proceedings of the Workshop on Principles of Provenance (PrOPr); Edinburgh, Scotland; November 2007.
[ abstract ]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 n 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.
Technical Reports
-
Testing Formal Semantics: Handel-C
Brian J. Corcoran. University of Dublin, Trinity College, Techical Report TCD-CS-2005-73, Sep. 2005.
[ abstract ]This dissertation addresses the formal semantics of Handel-C: a C-based language with true parallelism and priority-based channel communication, which can be compiled to hardware. It describes an implementation in the Haskell functional programming language of a denotational semantics for Handel-C, as described in (Butterfield & Woodcock). In particular, the Typed Assertion Trace model is used, and difficulties in creating a concrete implementation of the abstract model are discussed. An existing toolset supporting an operational semantics for the language is renovated, in part to support arbitrary semantic "modes", and to add support for the denotational semantics using this feature. A comparison module is written to compare the traces of two programs in any semantic mode supported by the simulator.
Random testing support is implemented via the QuickCheck testing tool for Haskell. This tool is incorporated into the comparison module, allowing testing of various properties of Handel-C, as well as its traditional use of testing the Haskell implementation for errors. This support is used to search for discrepancies between the operational and denotational semantic models.
Finally, several proposed "Laws of Handel-C" are implemented and tested using the QuickCheck module. Some errors in the specification of the laws are discovered and corrected. Once the specifications are corrected, all of the proposed laws pass, paving the way for future formal verification.
-
Presentation Tools For Molecular Biology
Brian J. Corcoran, Bradley Noyes, Steven Willis.
Worcester Polytechnic Institute Project MQP-MOW-0304, Dec. 2003. -
An Introductory CS Course For Non-majors
Brian J. Corcoran and Bradley K. Noyes.
Worcester Polytechnic Institute Project IQP-CK-IB02, May 2003.
Coursework
- CMSC 838F Language-Based Security
- CMSC 630 Theory of Programming Languages
- CMSC 818K Advanced Topics in Distributed Systems
- CMSC 724 Database Management Systems
- CMSC 751 Parallel Algorithmics
- CMSC 838F Language-Based Techniques for Concurrent and Distributed Systems
- CMSC 631 Program Analysis and Understanding
- CMSC 651 Analysis of Algorithms
Teaching
I was a teaching assistant for CMSC 131 (Object-Oriented Programming I) in Fall 2006 and Spring 2007.
Education
- University of Maryland, College Park : Oct
2006–present
Ph.D. Student, Department of Computer Science. - Trinity College,
University of Dublin : Oct. 2004–Sep. 2005
M.Sc. in Computer Science (Networks and Distributed Systems).
My thesis involved implementation and automated testing of the semantics of the Handel-C language, advised by Dr. Andrew Butterfield. - Worcester Polytechnic Institute :
Sep. 2000–May 2004
B.Sc. in Computer Science with high honors; minor in Electrical and Computer Engineering.