Evidence-based Audit

Jeff Vaughanlimin Jia, Karl Mazurak, And Steve Zdancewic

Description

Evidence-based AuditJe VaughanLimin Jia, Karl Mazurak, and Steve ZdancewicDepartment of Computer and Information ScienceUniversity of PennsylvaniaIBM PL Day/NJPLSAugust 28, 2008Our Setting: Distributed Access ControlA p p l i c a t i o n D a t aR e s o u r c e P r o o fP r i n c i p a l1/14Our Setting: Distributed Access ControlA p p l i c a t i o n D a t aR e s o u r c e P r o o fP r i n c i p a l1/14Our Setting: Distributed Access ControlA p p l i c a t i o n D a t aR e s o u r c e P r o o fP r i n c i p a l1/14Our Setting: Distributed Access ControlA p p l i c a t i o n D a t aR e s o u r c e P r o o fP r i n c i p a l1/14Our approach: Proofs attest to message validity.{ , }{ , }{ , }Application DataResource ProofPrincipal2/14[Necula+ 98]A programming language called AuraA propositional fragment: the evidenceAn ML-like computation languageA security aware programming modelActive, potentially malicious principalsMutual distrust between applications and principalsEmphasis on access control and auditAn implementationMechanized Coq proofsA prototype interpreter and .Net-based runtimeThe Aura ProjectKey IdeaAugmenting requests with logged evidence (proofs) enablesprincipled access control and meaningful audit in distributedsystems.3/14The Aura ProjectKey IdeaAugmenting requests with logged evidence (proofs) enablesprincipled access control and meaningful audit in distributedsystems.A programming language called AuraA ...

Informations

• Publié par: Thuid
• Nombre de lectures: 13
• Langue: English

Extrait

Evidence-based Audit

Jeff Vaughan Limin Jia, Karl Mazurak, and Steve Zdancewic

Department of Computer and Information Science University of Pennsylvania

IBM PL Day/NJPLS August 28, 2008

Our

Setting:

Distributed

Access

Control

1/14

Our

Setting:

Distributed

Access

Control

1/14

Our

Setting:

Distributed

Access

Control

1/14

Our

Setting:

Distributed

Access

Control

1/14

Our

approach:

[Necula+

Pro

98]

ofs

attest

to

message

validity.

2/14

untimet-basedr

The Aura Project

Key Idea

3/14

Augmenting requests with logged evidence (proofs) enables principled access control and meaningful audit in distributed systems.

acegdellalgnaugn sipoonti raAu roAp rogrammiAp ceru eg sAawertiay tatiompunguaonlanA ecnedi cekil-LM meagfralevhe:tnt pila M s tuaudlsirt lymaliciousprincitcAp,evnetolait ogprmmragminelod daudolanontresscanccisospmah la E sipncridpannsioatcilppaneewtebtsu erand.Nenterprettotopyie orfo A s rp edizqpCoMe on anch nemeitatnA ti lpmi

The Aura Project

Key Idea

Augmenting requests with logged evidence (proofs) enables principled access control and meaningful audit in distributed systems.

A programming language called Aura A propositional fragment: theevidence An ML-like computation language A security aware programming model Active, potentially malicious principals Mutual distrust between applications and principals Emphasis on access control and audit An implementation Mechanized Coq proofs A prototype interpreter and .Net-based runtime

3/14

The Aura Project

Key Idea

Augmenting requests with logged evidence (proofs) enables principled access control and meaningful audit in distributed systems.

A programming language called Aura A propositional fragment: theevidence An ML-like computation language A security aware programming model Active, potentially malicious principals Mutual distrust between applications and principals Emphasis on access control and audit An implementation Mechanized Coq proofs A prototype interpreter and .Net-based runtime

3/14

Security Problem

An application may contain bugs or be configured with incorrect formal rules.

Aura Solution Trust only a smallkernelthat isolates applications and resources. Log proofs corresponding to all access control decisions.

[Saltzer+ 75], [Bauer+ 99], [Jia+ 08] [Wee 95], [Cederquist+ 05]

4/14

In

Aura,

a

lightweight

kernel

protects

resources.

5/14