The Software Correctness and Safety Research Laboratory studies the application of theorem proving and other related formal techniques to providing assurance that complex software systems work correctly and safely. We are affiliated with: The Logic and Foundations of Computing Group (LFC); The Communications Software Engineering Research Group (CSERG). Our current research includes the following projects. Privacy Properties of Data Mining Software We are concerned with privacy protection defined as "the right of individuals to control the collection, use and dissemination of their personal information that is held by others" (Electronic Privacy Information Center). In our approach, users express their privacy policy as logical constraints and developers of data mining software provide proofs that their software respects these user-specified permissions. This is joint work with Stan Matwin of the Text Analysis and Machine Learning (TAMALE) group. [1] Privacy-Sensitive Information Flow with JML, by Guillaume Dufay, Amy Felty, and Stan Matwin. In Twentieth International Conference on Automated Deduction, Springer-Verlag LNCS, July 2005 (postscript). [2] Privacy in Data Mining Using Formal Methods, by Stan Matwin, Amy Felty, Istvan Hernadvolgyi, and Venanzio Capretta. In Seventh International Conference on Typed Lambda Calculi and Applications, Springer-Verlag LNCS 3461, April 2005 (postscript). [3] Privacy-Oriented Data Mining by Proof Checking, by Amy Felty and Stan Matwin In Sixth European Conference on Principles of Data Mining and Knowledge Discovery, Springer-Verlag LNCS 2431, August 2002 (postscript). Proof-Carrying Code Proof-carrying code (PCC) provides a mechanism for insuring that a host, or code consumer, can safely run code delivered by a code producer. The host specifies a safety policy as a set of axioms and inference rules. In addition to a compiled program, the code producer delivers a formal proof of safety expressed in terms of those rules that can be easily checked. The principle advantage is that the trusted computing base is extremely small; it includes only the proof checker for verifying the proof of safety. In addition, the safety properties of interest are much easier to prove automatically than general program correctness. Our current work is on foundational proof-carrying code [4, 7] which provides increased security by decreasing the size of the trusted computing base (TCB), and increased flexibility by allowing a single safety policy to be used for multiple programming languages and compilers. This work is in collaboration with Andrew Appel (Princeton University) and others. Our current work centers around two areas. First, we aim to scale up the approach to fully automate proofs of safety for full programming languages such as ML and Java. Second, we are designing a general environment for implementing foundational proof-carrying code systems [5, 6]. This work is part of a more general effort on the design and implementation of a system which provides a uniform framework for developing programming languages and proving properties about them, and for writing, interpreting, debugging, and proving properties of programs written in these languages. [4] A Tutorial Example of the Semantic Approach to Foundational Proof-Carrying Code, by Amy P. Felty, In Sixteenth International Conference on Rewriting Techniques and Applications, Springer-Verlag LNCS 3467, April 2005 (postscript). [5] Dependent Types Ensure Partial Correctness of Theorem Provers, by Andrew W. Appel and Amy P. Felty. Journal of Functional Programming, 14(1):3-19, January 2004 (postscript). [6] Polymorphic Lemmas and Definitions in Lambda Prolog and Twelf, by Andrew W. Appel and Amy P. Felty. Theory and Practice of Logic Programming, 4(1&2):1-39, January & March 2004 (postscript). [7] A Semantic Model of Types and Machine Instructions for Proof-Carrying Code, by Andrew W. Appel and Amy P. Felty. In The 27th Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, January 2000 (postscript). Feature Interaction Telecommunications services are typically marketed to customers as groups of features such as call-waiting and call-forwarding. We have developed a formal feature specification language and a method of automatically detecting feature conflicts ("undesirable interactions") at the specification stage [8]. Early conflict detection can help prevent costly and time-consuming problem fixes during implementation. Features are specified in linear temporal logic; two features conflict essentially if their specifications are mutually inconsistent under axioms about the underlying system behavior. We have implemented a conflict detection tool that uses the a model-checker for the inconsistency check. We are working on a theorem proving approach to allow more general conflict tests [9]. [8] Feature Specification and Automatic Conflict Detection, by Amy P. Felty and Kedar S. Namjoshi. ACM Transactions on Software Engineering and Methodology, 12(1):3-27, January 2003 (postscript). [9] Temporal Logic Theorem Proving and its Application to the Feature Interaction Problem, by Amy Felty. In E. Giunchiglia and F. Massacci, editors, Issues in the Design and Experimental Evaluation of Systems for Modal and Temporal Logics, Technical Report DII 14/01, University of Siena, June 2001 (postscript). Higher-Order Abstract Syntax and Induction Lambda Prolog and Twelf are two languages that we use extensively in our research. They both provide support for programming with data structures that are represented using higher-order abstract syntax. Although programming with such objects is supported, providing a logic that can reason about them, particularly using case analysis and induction, presents a significant challenge. This syntax is important, for example, for the specification of the primitive inference rules in our PCC system, and is likely to become more important when formalizing more complex semantics. The reasoning that will be required will need more general techniques than what has so far been developed. Developing new and general techniques have the potential to greatly simplify various aspects of formal proof. This work will also have significant impact on reasoning abilities in proof and program development environments. [10] Two-Level Meta-Reasoning in Coq, by Amy P. Felty. In Fifteenth International Conference on Theorem Proving in Higher Order Logics, Springer-Verlag LNCS 2410, August 2002 (postscript). [11] Higher-Order Abstract Syntax in Coq, by Joëlle Despeyroux, Amy Felty, and André Hirschowitz. In Second International Conference on Typed Lambda Calculi and Applications, Springer-Verlag LNCS 902, April 1995 (postscript). Requirements-Driven Development of Distributed Applications In this project, we collaborate with researchers in the Communications Software Engineering Research Group (CSERG). Our work on the project involves (a) the development of formal semantics of requirements notations, (b) techniques for verification of security and correctness properties, (c) tool development for part b, and (d) case studies using existing and new tools. Protocol Verification Theorem provers can provide a general and powerful environment for protocol verification. My work in this area has included the implemention of an environment for protocol verification within the Nuprl theorem prover and its use in formalizing a large part of a correctness argument for the SCI cache coherence protocol [12, 13]; the design and implemention of a theorem prover for a temporal logic which is used in many model checkers [14]; and the combination of model checkers (which provide powerful automation for protocol verification) with theorem provers in a manner which draws on the strengths of each [15]. [12] Cache Coherency in SCI: Specification and a Sketch of Correctness, by Amy Felty and Frank Stomp. Formal Aspects of Computing, 11(5):475-497, 1999 (postscript, abstract). [13] Protocol Verification in Nuprl, by Amy P. Felty, Douglas J. Howe and Frank A. Stomp. In Tenth International Conference on Computer-Aided Verification, Springer-Verlag LNCS 1427, June 1998 (postscript). [14] Interactive Theorem Proving with Temporal Logic, by Amy Felty and Laurent Théry, Journal of Symbolic Computation, 23(4):367-397, April 1997 (postscript). [15] Formal Metatheory Using Implicit Syntax, and an Application to Data Abstraction for Asynchronous Systems, by Amy P. Felty, Douglas J. Howe, and Abhik Roychoudhury. In Sixteenth International Conference on Automated Deduction, Springer-Verlag LNCS 1632, July 1999 (postscript).

Faculty:   Amy Felty (SITE and Math) Research Scientists:   Bernard Stepien (SITE) Ph.D. Students:   Franck Binard (SITE) Zhiping Duan (SITE) Alan Martin (Math) Bahman Sistany (SITE) M.Sc. Students:   Yanyun Lu (SITE)