Distributed System Security via Logical Frameworks

First, we are investigating how to exploit existing technologies to mechanically reason about security policies as specified in a logical framework. This would close an important security gap, helping users and managers understand the consequences of their policies.

Second, we plan to demonstrate the use of logical frameworks for encoding and enforcing access-control policies in a practical distributed system. Access-control mechanisms today, whether it be physical keys for doors or password protection for computer accounts, reflect access-control policies that are explicit only in the manual procedures of the organization that manages these resources. As such, any change in policy, e.g., creating a new computer account, or permitting a person to unlock a door, is effected through a manual process. We propose to utilize logical frameworks to encode organizational policies within computer systems, thereby harnessing the power of these frameworks to support the management and enforcement of access-control policy, and gaining security and flexibility by doing so. We intend to demonstrate this capability in a ubiquitous computing test-bed that we will develop at Carnegie Mellon.

Third, we are developing and implementing a framework for the specification of distributed and concurrent systems and their implementations, specifically targeting the architecture we are implementing. This work extends a previous collaboration between NRL and Carnegie Mellon that resulted in the design of CLF, an innovative logical language for the specification of concurrent systems. CLF incorporates ideas from logical frameworks, linear logic, and monads into an expressive meta-language.

This work was supported by the Office of Naval Research (ONR) Grants N00014-01-1-0432 and N00173-00-C-2086 -- Efficient Logics for Reasoning about Security Protocols and Their Implementations. CLF is now fully specified and has been successfully validated on mainstream concurrency formalisms (e.g., Petri nets, the pi-calculus), advanced concurrent programming languages (Concurrent ML), and security protocol specification languages (MSR). In the context of the present proposal, our goal is to facilitate the transition of CLF from a foundational language into an implemented tool that can be applied to the specification of complex distributed and concurrent systems.

Researchers at Carnegie Mellon University

Co-Principal Investigators

• Lujo Bauer, CyLab, Carnegie Mellon University
• Frank Pfenning, Department of Computer Science
• Michael K Reiter, Department of Electrical and Computer Engineering and Department of Computer Science

Other Researchers

• Kaustuv Chaudhuri
• Deepak Garg
• Scott Garriss
• Jon McCune
• Jason Rouse
• Kevin Watkins

Collaborators

• Pablo Lopez, Universidad de Málaga, Spain
• Jeff Polakow, National Institute of Advanced Industrial Science and Technology (AIST), Osaka, Japan

Recent Drafts, Talks, and Publications

• Consumable Credentials in Logic-Based Access-Control Systems. Proceedings of the 14th Annual Network and Distributed System Security Symposium (NDSS'07), San Diego, CA, February 2007. To appear. Preliminary version available as Technical Report CMU-CYLAB-06-002, Carnegie Mellon University, February 2006. Kevin D. Bowers, Lujo Bauer, Deepak Garg, Frank Pfenning and Michael K. Reiter
  
  
• A Linear Logic of Affirmation and Knowledge. Proceedings of the 11th European Symposium on Research in Computer Security (ESORICS'06), Hamburg, Germany, September 2006. Deepak Garg, Lujo Bauer, Kevin Bowers, Frank Pfenning, and Michael Reiter. [PDF] [PS]
  
  
• Non-Interference in Constructive Authorization Logic. Proceedings of the 19th Computer Security Foundations Workshop (CSFW'06), Venice, Italy, July 2006. Deepak Garg and Frank Pfenning.
  [PDF] [PS] [Formalization]
  
  
• Avoiding Spurious Causal Dependencies via Proof Irrelevance in a Concurrent Logical Framework. Submitted, April 2006. Ruy Ley-Wild and Frank Pfenning. [PDF] [PS]


• A Logical Characterization of Forward and Backward Chaining in the Inverse Method. Proceedings of the 3rd International Joint Conference on Automated Reasoning (IJCAR'06), Seattle, Washington, August 2006. Kaustuv Chaudhuri, Frank Pfenning, and Greg Price. Version from March 2006: [PDF] [ PS]


• Constructive Authorization Logics. Invited talk at the 4th Workshop on Foundations of Computer Security (FCS'05), Chicago, Illinois, July 2005. [PDF] [PS]
  
  
• Focusing the Inverse Method for Linear Logic. 16th Annual Conference on Computer Science Logic (CSL'05), Oxford, UK, August 2005. Kaustuv Chaudhuri and Frank Pfenning. [PDF] [PS] [Implementation]
  


• A Focusing Inverse Method Prover for First-Order Linear Logic. 20th International Conference on Autmated Deduction (CADE-20), Tallinn, Estonia, July 2005. Kaustuv Chaudhuri and Frank Pfenning. [PDF] [PS] [Propositional] and [first-order] prover implementations.
  


• Distributed proving in access-control systems. In Proceedings of the 2005 IEEE Symposium on Security and Privacy, May 2005. Lujo Bauer, Scott Garriss and Michael K. Reiter.
  
  
• Monadic concurrent linear logic programming. 7th International Symposium on Principles and Practice of Declarative Programming (PPDP '05), Lisbon, Portugal, July 2005. Pablo López, Frank Pfenning, Jeff Polakow, and Kevin Watkins. [PDF] [PS] [Prototype] implementation.
  

Support

This project is supported by the Office of Naval Research (ONR) under grant MURI N00014-04-1-0724: Distributed System Security via Logical Frameworks.

[ Home | Publications | Software | Links ]

http://www.cs.cmu.edu/~self