abadi fcs arspa floc06

Calculi for Access Control: 

Calculi for Access Control Martίn Abadi University of California, Santa Cruz and Microsoft Research, Silicon Valley

The access control model: 

The access control model Elements: Objects or resources Requests Sources for requests, called principals A reference monitor to decide on requests

Authentication vs. access control: 

Authentication vs. access control Access control (authorization): Is principal A trusted on statement s? If A requests s, is s granted? Authentication: Who says s?

An access control matrix [Lampson, 1971]: 

An access control matrix [Lampson, 1971]

Access control in current practice: 

Access control in current practice Access control is pervasive applications virtual machines operating systems firewalls doors … Access control seems difficult to get right. Distributed systems make it harder.

General theories and systems: 

General theories and systems Over the years, there have been many theories and systems for access control. Logics Languages Infrastructures (e.g., PKIs) Architectures They often aim to explain, organize, and unify access control.

An approach: 

An approach A notation for representing principals and their statements, and perhaps more: objects and operations, trust, channels, … Derivation rules

A calculus for access control[Abadi, Burrows, Lampson, and Plotkin, 1993]: 

A calculus for access control [Abadi, Burrows, Lampson, and Plotkin, 1993] A simple notation for assertions A says s A speaks for B (sometimes written A ⇒ B) With logical rules ⊢ A says (s  t)  (A says s)  (A says t) If ⊢ s then ⊢ A says s. ⊢ A speaks for B  (A says s)  (B says s) ⊢ A speaks for A ⊢ A speaks for B ∧ B speaks for C  A speaks for C

An example: 

An example Let good-to-delete-file1 be a proposition. Let B controls s stand for (B says s)  s Assume that B controls (A speaks for B) B controls good-to-delete-file1 B says (A speaks for B) A says good-to-delete-file1 We can derive: B says good-to-delete-file1 good-to-delete-file1

Another example: 

Another example Let good-to-delete-file2 be a proposition too. Assume that B controls (A speaks for B) B controls good-to-delete-file1 B says (A speaks for B) A says (good-to-delete-file1 ∧ good-to-delete-file2) We can derive: B says good-to-delete-file1 good-to-delete-file1

Says: 

Says Channel statement (from: context 1 ) Says represents communication across contexts. Says abstracts from the details of authentication.

Choosing axioms: 

Choosing axioms Standard modal logic? (As above.) Less? Treat says “syntactically”, with no special rules (Halpern and van der Meyden, 2001)

Choosing axioms (cont.): 

Choosing axioms (cont.) More? ⊢ (A says (B speaks for A))  (B speaks for A) The “hand-off axiom”; in other words, A controls (B speaks for A). ⊢ s  (A says s) (Lampson, 198?; Appel and Felten, 1999) but then ⊢ (A says s)  s  (A says false)

Semantics: 

Semantics Following standard semantics of modal logics, a principal may be mapped to a binary relation on possible worlds. A says s holds at world w iff s holds at world w’ for every w’ such that w A w’ This is formally viable, also for richer logics. It does not give much insight on the meaning of authority, but it is sometimes useful.

Proof strategies: 

Proof strategies Style of proofs: Hilbert systems Tableaux (Massacci, 1997) … Proof distribution: Proofs done at reference monitors Partial proofs provided by clients (Wobber et al., 1994; Appel and Felten, 1999) With certificates pulled or pushed

More principals: 

More principals Compound principals represent a richer class of sources for requests: A ∧ B Alice and Bob (cosigning) A quoting B server.uxyz.edu quoting Alice A for B server.uxyz.edu for Alice A as R Alice as Reviewer A ∧ B speaks for A, etc. Groups represent collections of principals, and may be treated as principals themselves. Programs may be treated as roles.

Applications (1): Security in an operating system [Wobber et al., 1994]: 

Applications (1): Security in an operating system [Wobber et al., 1994]

Applications (2): An account of security in JVMs [Wallach and Felten, 1998]: 

Applications (2): An account of security in JVMs [Wallach and Felten, 1998]

Applications (3): A Web access control system [Bauer, Schneider, and Felten, 2002]: 

Applications (3): A Web access control system [Bauer, Schneider, and Felten, 2002]

Applications (4): The Grey system [Bauer, Reiter, et al., 2005]: 

Applications (4): The Grey system [Bauer, Reiter, et al., 2005] Converts a cell-phone into a tool for delegating and exercising authority. Uses cell phones to replace physical locks and key systems. Implemented in part of CMU. With access control based on logic and distributed proofs.

Distributed Proving: 

Distributed Proving

Further applications: Other languages and systems: 

Further applications: Other languages and systems Several languages rely on logics for access control and on logic programming: D1LP and RT [Li, Mitchell, et al.] SD3 [Jim] Binder [DeTreville] “speaks for” plays a role in other systems: SDSI and SPKI [Lampson and Rivest; Ellison et al.] Plan 9 [Pike et al.] …

Some issues: 

Some issues It is easy to add constructs and axioms, but sometimes difficult to decide which are right. Explicit representations for proofs are useful. Even with logic, access control typically does not provide end-to-end guarantees (e.g., the absence of flows of information).

The Dependency Core Calculus (DCC) [Abadi, Banerjee, Heintze, and Riecke, 1999]: 

The Dependency Core Calculus (DCC) [Abadi, Banerjee, Heintze, and Riecke, 1999] A minimal but expressive calculus in which the types capture dependencies. A foundation for some static program analyses: information-flow control, binding-time analysis, slicing, … Based on the computational lambda calculus.

DCC basics: 

DCC basics Let L be a lattice. For each type s and each l in L, there is a type Tl(s). If l ⊑ k then terms of type Tk(t) may depend on terms of type Tl(s). For instance: The lattice may have two elements Public and Secret, with Public ⊑ Secret. TPublic(int) and TSecret(bool) would be two types. Then DCC guarantees that outputs of type TPublic(int) do not depend on inputs of type TSecret(bool).

A new look at DCC: 

A new look at DCC We read DCC as a logic, via the Curry-Howard isomorphism. Types are propositions. Programs are proofs. We consider significant but routine variations on the original DCC: We remove fixpoints and related constructs. We add polymorphism in the style of System F. We write A says s instead of Tl(s). We write A speaks for B as an abbreviation for X. (A says X  B says X).

A new look at DCC (cont.): 

A new look at DCC (cont.) The result is a logic for access control, with some principles and some useful theorems. The logic is intuitionistic (like a recent system by Garg and Pfenning). Terms are proofs to be used in access control.

Simply Typed DCC: Syntax: 

Simply Typed DCC: Syntax

Simply Typed DCC: Protected types: 

Simply Typed DCC: Protected types

Simply Typed DCC: Typing rules: 

Simply Typed DCC: Typing rules The typing rules are those of simply typed λ-calculus plus:

Simply Typed DCC: Logical reading: 

Simply Typed DCC: Logical reading Reading the typing rules as a logic can be simply a matter of omitting terms…

Polymorphic DCC: 

Polymorphic DCC Polymorphic DCC is obtained by adding type variables and universal quantification, with the standard rules. The definition of “protected” is extended:

Semantics: 

Semantics Operational semantics (one possibility): usual λ-calculus rules, plus the new rule (Zdancewic recently checked subject reduction and progress properties for this semantics in Twelf.) Denotational semantics? (We have some pieces, but more could be done.)

DCC theorems: 

DCC theorems We can rederive the core of the previous logics: ⊢ A says (s  t)  (A says s)  (A says t) If ⊢ s then ⊢ A says s. ⊢ A speaks for B  (A says s)  (B says s) ⊢ A speaks for A ⊢ A speaks for B ∧ B speaks for C  A speaks for C

DCC theorems (cont.): 

DCC theorems (cont.) DCC has some additional useful theorems. ⊢ (A says (B speaks for A))  (B speaks for A) ⊢ s  (A says s) and also ⊢ A says A says s  A says s ⊢ A says B says s  B says A says s These follow from general rules, apparently without annoying consequences.

DCC theorems (cont.): 

DCC theorems (cont.) If A ⊑ B, then ⊢ A speaks for B. B says (A speaks for B) does not imply A ⊑ B. B says (A ⊑ B) is not even syntactically correct. Lattice elements may represent groups, rather than individual principals. The operations ⊓ and ⊔ may represent group intersection and union. ⊢ (A ⊓ B) says s  A says s ∧ B says s. The converse fails (quite reasonably).

DCC metatheorems: 

DCC metatheorems DCC also has a useful metatheory, which includes old and new non-interference results.

Mapping to System F (warm-up): 

Mapping to System F (warm-up) Tse and Zdancewic have defined a clever encoding of Simply Typed DCC in System F. We can define a more trivial mapping (.)F from Polymorphic DCC to System F by letting This mapping preserves provability, so Polymorphic DCC is consistent.

Non-interference: 

Non-interference Access control requires the integrity of requests and policies. We would like some guarantees on the possible effect of the statements of principals. E.g., if A and B are unrelated principals, then B’s statements should not interfere with A’s. There are previous non-interference theorems for DCC, and we can prove some more.

Another mapping: what a formula means when B may say anything: 

Another mapping: what a formula means when B may say anything

A theorem: 

A theorem

Some corollaries: 

Some corollaries

Further work and open questions: 

Further work and open questions Rich, convenient languages for writing policies. Procedures for analyzing policies. Revisiting compound principals. Other logics with similar principles (but different theorems). More semantics. Integration of access control into programming. Relation to information flow.

Outlook: 

Outlook We can provide at least partial evidence of the “goodness” of our rules. Even with imperfect rules, declarative policies may contribute to improving authorization. Logics and types should help.