Higher-Order Abstract Syntax and Induction
Logical frameworks supporting higher-order abstract syntax (HOAS) allow a direct and concise specification of a wide variety of logics, programming languages, and deductive systems. Programming with such specifications is well-supported by languages such as Lambda Prolog and Twelf. Reasoning about such specifications provides the opportunity to establish meta-theory of the encoded languages; it can be used, for example, to formalize the meta-theory of programming languages. Our group is active in developing the Hybrid approach and tool. We focus on the implementation of Hybrid in the Coq Proof Assistant [Hy], whose main web page can be found here. We have also been involved in improvements and case studies in the Isabelle version [Mar10]. More recent work involves case studies in the Coq version [] as well as work on benchmarks and comparison to other systems.[Hy] Two-level Hybrid: A System for Reasoning Using Higher-Order Abstract Syntax.
[Mar10] Reasoning Using Higher-Order Abstract Syntax in a Higher-Order Logic Proof Environment: Improvements to Hybrid and a Case Study, by Alan J. Martin, Ph. D. thesis, University of Ottawa, November 2010, (pdf, code).
Policy Compliance and Policy Verification
We work on tools and services for fast, accurate, and consistent management of access control across multiple applications, using a variety of policy languages, including SELinux [ESF17] and XACML (OASIS eXtensible Access Control Markup Language) [SF20, SF16, SFM14a, SFM14b, SFM12, SMF11, SMF10, SFM09]. We are also working on defining a new policy language with a simple semantics and formal proofs of correctness properties. [SF17] In addition, we have formally verified algorithms for detecting conflicts in XACML policies [StF16] and firewall access rules [C+07]. Another kind of policy of interest are those which concern 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 [DFM05, M+05, FM02] This is joint work with several colleagues including Stan Matwin of the Institute for Big Data Analytics.[SF20] Resolving XACML Rule Conflicts Using Artificial Intelligence, by Bernard Stepien and Amy Felty, In Proceedings of the 2020 The 3rd International Conference on Information Science and System (ICISS 2020), ACM, pages 121-127, March 2020 (pdf).
[SF17] A Certified Core Policy Language, by Bahman Sistany and Amy Felty In 15th Annual International Conference on Privacy, Security, and Trust (PST) , August 2017, (pdf).
[ESF17] Review of Existing Analysis Tools for SELinux Security Policies: Challenges and a Proposed Solution, by Amir Eaman, Bahman Sistany, and Amy Felty E-Technologies: Embracing the Internet of Things, Proceedings of the 7th International MCETECH Conference, Springer LNBIP 289, pages 116-135, May 2017 (pdf).
[SF16] Using Expert Systems to Statically Detect "Dynamic" Conflicts in XACML, by Bernard Stepien and Amy Felty. In Proceedings of the Eleventh International Conference on Availability, Reliability and Security (ARES), August 2016 (pdf).
[StF16] A Verified Algorithm for Detecting Conflicts in XACML Access Control Rules, by Michel St-Martin and Amy P. Felty. In Proceedings of the Fifth ACM SIGPLAN Conference on Certified Programs and Proofs (CPP), pages 166-175, January 2016 (pdf, Coq formalization).
[SFM14a] Challenges of Composing XACML Policies, by Bernard Stepien, Amy Felty, and Stan Matwin. Proceedings of the Ninth International Conference on Availability, Reliability and Security (ARES), September 2014, (pdf).
[SFM14b] A Non-Technical XACML Target Editor for Dynamic Access Control Systems, by Bernard Stepien, Amy Felty, and Stan Matwin. Proceedings of the 2014 International Conference on Collaboration Technologies and Systems (CTS), pages 150-157, May 2014, (pdf).
[SFM12] An Algorithm for Compression of XACML Access Control Policy Sets by Recursive Subsumption, by Bernard Stepien, Amy Felty, and Stan Matwin. 7th International Conference on Availability, Reliability, and Security (ARES), pp. 161-167, August 2012 (pdf).
[SMF11] Advantages of a Non-Technical XACML Notation in Role-Based Models, by Bernard Stepien, Stan Matwin, and Amy Felty. In 9th Annual International Conference on Privacy, Security, and Trust (PST), July 2011 (pdf).
[SMF10] Strategies for Reducing Risks of Inconsistencies in Access Control Policies, by Bernard Stepien, Stan Matwin, and Amy Felty. In 5th International Conference on Availability, Reliability, and Security, February 2010 (pdf).
[SFM09] A Non-technical User-Oriented Display Notation for XACML Conditions, by Bernard Stepien, Amy Felty, and Stan Matwin. In E-Technologies: Innovation in an Open World, Proceedings of the 4th International MCETECH Conference, Springer LNBIP 26, 2009 (pdf).
[C+07] Formal Correctness of Conflict Detection for Firewalls, by Venanzio Capretta, Bernard Stepien, Amy Felty, and Stan Matwin. In ACM Workshop on Formal Methods in Security Engineering, November 2007 (pdf, Coq formalization).
[DFM05] 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 (pdf).
[M+05] 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 (pdf).
[FM02] 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 (pdf).
Modelling and Verifying Properties of Biological Systems
We work on modelling properties of biological systems and verifying their properties in the Coq Proof assistant. We have proposed an approach to formal verification of biological systems based on the use of linear logic. Examples include models of the P53/Mdm2 DNA-damage repair mechanism [DDF14] and breast cancer progression [D+18]. We have also modelled and verified properties of biological neural networks [BDF18].[D+18] A Logical Framework for Modelling Breast Cancer Progression, by Joëlle Despeyroux, Amy Felty, Pietro Lio, and Carlos Olarte. In Proceedings of the International Symposium on Molecular Logic and Computational Synthetic Biology (MLCSB 2018), Springer LNCS, to appear, (pdf, Coq code).
[BDF18] Modelling and Verifying Dynamic Properties of Biological Neural Networks in Coq, by Abdorrahim Bahrami, Elisabetta De Maria, and Amy Felty. In Proceedings of the 9th International Conference on Computational Systems-Biology and Bioinformatics (CSBio 2018), ACM, Article No.: 12, pages 1-11, 2018, (pdf, Electronic appendix).
[DDF14] A Logical Framework for Systems Biology, by Elisabetta de Maria, Joëlle Despeyroux, and Amy P. Felty. 1st International Conference Formal Methods in Macro-Biology (FMMB), Springer LNCS 8738, pages 136-155, September 2014, (pdf, electronic appendix).
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 recent work has included probabilistic proof-carrying code [Sha12] and foundational proof-carrying code [Fel07, AF00]. In our approach to probabilistic PCC, we considier implementations of computing systems that are susceptible to probabilistic behaviours that can alter the execution of a program in ways that can result in corruption or security breaches. Foundational PCC 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 was in collaboration with Andrew Appel (Princeton University) and others. We have also been interested in scaling up the approach to fully automate proofs of safety for full programming languages such as ML and Java [WF11]. In addition, we have been involved in designing a general environment for implementing foundational proof-carrying code systems [AF04a, AF04b]. 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.[Sha12] Probabilistic Proof-Carrying Code, by Ian Sharkey. Master's thesis, April 2012, (pdf).
[WF11] An Implementation of a Verification Condition Generator for Foundational Proof-Carrying Code, by Jiangong Weng and Amy Felty. In 9th Annual International Conference on Privacy, Security, and Trust (PST), July 2011, (pdf).
[Fel07] Tutorial Examples of the Semantic Approach to Foundational Proof-Carrying Code, by Amy P. Felty. Fundamenta Informaticae, 7(4):303-330, 2007 (pdf).
[AF04a] 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).
[AF04b] 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 (pdf).
[AF00] 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 (pdf).
Genetic Programming with Polymorphic Types and Higher-Order Functions
We developed a new approach to program representation for genetic programming (GP), replacing the usual s-expression representation scheme with programs in the higher-order polymorphically typed language System F [BF08, BF07]. As a result of the expressive power of this calculus, the system is able to express programming structures such as recursion and data types without explicit definitions. Using such a system, we are able to evolve programs that exhibit recursive behavior without explicitly defining recursion-specific syntax in the terminal set. This work can be viewed as an approach to inductive programming.[BF08] Genetic Programming with Polymorphic Types and Higher-Order Functions, by Franck Binard and Amy Felty. In Proceedings of the Tenth Annual Conference on Genetic and Evolutionary Computation, ACM Press, 2008 (pdf).
[BF07] An Abstraction-Based Genetic Programming System, by Franck Binard and Amy Felty. In Genetic and Evolutionary Computation Conference: Late Breaking Papers, 2007 (pdf).
Faculty:
|
Amy Felty (EECS and Math) |
Postdocs:
|
Abdorrahim Bahrami (EECS) Amir Eaman (EECS) |
Ph.D. Students:
Master's Students:
|
John Shortt (EECS and Carleton, SCS) Yan Steimle (EECS) |
Recent Alumni:
|
Abdorrahim Bahrami (EECS, Ph.D.) Chelsea Battell (Math, Master's) Franck Binard (EECS, Ph.D.) Amir Eaman (EECS, Ph.D.) Weiyun Lu (EECS, Master's) Alan Martin (Math, Ph.D.) Mohamed Yousri Mahmoud (EECS, Postdoc) Ian Sharkey (EECS, Master's) Bahman Sistany (EECS, Ph.D.) Bernard Stepien (EECS, Research Scientist) Michel St-Martin (Math, Master's) Polina Vinogradova (EECS, Ph.D.) |