A Type Discipline for Authorization in Distributed Systems

Cédric Fournet, Andrew Gordon, Sergio Maffeis

Research output: Chapter in Book/Report/Conference proceedingConference contribution

Abstract

We consider the problem of statically verifying the conformance of the code of a system to an explicit authorization policy. In a distributed setting, some part of the system may be compromised, that is, some nodes of the system and their security credentials may be under the control of an attacker. To help predict and bound the impact of such partial compromise, we advocate logic-based policies that explicitly record dependencies between principals. We propose a conformance criterion, safety despite compromised principals, such that an invalid authorization decision at an uncompromised node can arise only when nodes on which the decision logically depends are compromised. We formalize this criterion in the setting of a process calculus, and present a verification technique based on a type system. Hence, we can verify policy conformance of code that uses a wide range of the security mechanisms found in distributed systems, ranging from secure channels down to cryptographic primitives, including encryption and public-key signatures.
Original languageEnglish
Title of host publication20th IEEE Computer Security Foundations Symposium, CSF 2007, 6-8 July 2007, Venice, Italy
PublisherInstitute of Electrical and Electronics Engineers (IEEE)
Pages31-48
Number of pages18
ISBN (Print)0-7695-2819-8
DOIs
Publication statusPublished - 2007

Fingerprint

Dive into the research topics of 'A Type Discipline for Authorization in Distributed Systems'. Together they form a unique fingerprint.

Cite this