Distributed System Security via Logical FrameworksWe are conducting a research program with the goal of advancing security in distributed systems via the application of logical frameworks. Our work targets multiple facets of the life-cycle of a distributed system, ranging from design through execution, and from sound mechanism design through sound policy enforcement. It consists of three major interconnected thrusts.
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
[ Home | Publications | Software | Links ]