Transcript AURA: A language with authorization and audit

AURA:
A language with authorization and audit
Steve Zdancewic
University of Pennsylvania
HCSS 2008
Security-oriented Languages
Limin Jia, Karl Mazurak, Jeff Vaughan, Jianzhou Zhao
Joey Schorr and Luke Zarko
• Manifest Security Project (NSF-0714649)
– Penn: Benjamin Pierce, Stephanie Weirich
– CMU: Karl Crary, Bob Harper, Frank Pfenning
• CAREER: Language-based Distributed
System Security (NSF-0311204)
2
Networked Information System Security
data
host
applications
• Networked hosts
• Many applications running
• Data resides at the hosts but can be shared over the
network
3
Information-flow Constraints
data
host
applications
• Some data is confidential
• Heterogeneous trust:
– Not all hosts are trusted to the same degree
– Different principals might have different opinions about trust
4
Challenges
• Policies are complex to specify and difficult to enforce
– Many entities: hosts, programs, users, etc.
– Software is large and complex
– Heterogeneous trust implies decentralization of policies
• Existing mechanisms are necessary…
– Cryptography
– Network protocols
– OS / Firewalls, etc. level isolation
• …but not sufficient
– Must decrypt data to process it
– Hard to regulate information flows through software
– OS / Firewall access control and auditing is at the wrong level of
abstraction
5
Security-oriented Languages
• Use static analysis (e.g. type systems) and dynamic
checks to enforce security properties at the language
level.
• My own research [Zdancewic et al.]
– Jif, secure-program partitioning, robust declassification, …
• Authorization Logics & Proof Carrying Authorization:
– ABLP 1993 [Abadi, Burrows, Lampson, Plotkin]
– DCC [Abadi], linearity & time [Garg & Pfenning]
– Trust Management [Blaze et al.]
• Information flow:
– Jif [Myers, et al.] , FlowCaml [Simonet, et al.] , …
• Much work in the last decade:
ESC/Java, Spec# [Leino, et al.] Type Qualifiers [Foster, et al.]
PoET/PSLang [Erlingson & Schneider] TAL, Cyclone [Morrisett,
et al.]
PCC, Ccured[Necula, et al.] xg++, metal [Engler, et al.], Fable [Hicks…]6
Goal of the AURA project:
• Develop a security-oriented programming language that
supports:
– Proof-carrying Authorization
[Appel & Felton] [Bauer et al.]
– Strong information-flow properties
(as in Jif [Myers et al.] , FlowCaml [Pottier & Simonet])
• Why?
– Declarative policies (for access control & information flow)
– Auditing & logging: proofs of authorization are informative
– Good theoretical foundations
• In this talk: A high-level tour of AURA's design
– Focus on the authorization and audit components
7
Outline
• AURA's programming model
• Authorization logic
– Examples
• Programming in AURA
– Dependent types
• Status, future directions, conclusions
8
AURA: Programming Model
application
code
code
system interface
I/O
AURA runtime system
• AURA is a type-safe functional programming language
• As in Java, C#, etc. AURA provides an interface to the OS resources
– disk, network, memory, …
• AURA is intended to be used for writing security-critical components
9
AURA: Authorization Policies
application
proof
code
code
policy
system interface
I/O
AURA runtime system
• AURA security policies are expressed in an authorization logic
• Applications can define their own policies
• Language provides features for creating/manipulating proofs
10
AURA: Authorization Policies
application
proof
code
data
code
policy
system interface
I/O
AURA runtime system
log
• Proofs are first class and they can depend on data
• Proof objects are capabilities needed to access resources protected
by the runtime: AURA's type system ensures compliance
• The runtime logs the proofs for later audit
11
AURA: Principals and Keys
application
proof
A
code
data
B
code
policy
system interface
I/O
AURA runtime system
A
B
log
• For distributed systems, AURA also manages private keys
• Keys can create policy assertions sharable over the network
• Connected to the policy by AURA's notion of principal
12
Evidence-based Audit
• Connecting the contents of
log entries to policy helps
determine what to log.
policy
code
log
13
Evidence-based Audit
• Connecting the contents of
log entries to policy helps
determine what to log.
policy
code
• Proofs contain structure
that can help
administrators find flaws or
misconfigurations in the
policy.
log
14
Evidence-based Audit
• Connecting the contents of
log entries to policy helps
determine what to log.
policy
code
• Proofs contain structure
that can help
administrators find flaws or
misconfigurations in the
policy.
• Reduced TCB: Typed
interface forces code to
provide auditable evidence.
log
15
Outline
• AURA's programming model
• Authorization logic
– Examples
• Programming in AURA
– Dependent types
• Status, future directions, conclusions
16
AURA's Authorization Logic
• Policy propositions
 ::= true
c
A says 




. 
• Principals
A,B,C … P,Q,R etc.
• Constructive logic:
– proofs are programs
– easy integration with
software
• Access control in a
Core Calculus of
Dependency
[Abadi: ICFP 2006]
17
Example: File system authorization
• P1: FS says (Owns A f1)
• P2: FS says (Owns B f2)
• …
•
OwnerControlsRead:
FS says o,r,f. (Owns o f) 
(o says (MayRead r f)) 
(MayRead r f)
• Might need to prove: FS says (MayRead A f1)
• What are "Owns" and "f1"?
18
Decentralized Authorization
• Authorization policies require application-specific
constants:
– e.g.
"MayRead B f" or "Owns A f"
– There is no "proof evidence" associated with these constants
– Otherwise, it would be easy to forge authorization proofs
• But, principal A should be able to create a proof of
A says (MayRead B f)
– No justification required -- this is a matter of policy, not fact!
• Decentralized implementation:
– One proof that "A says T" is A's digital signature on a string "T"
– written sign(A, "T")
19
Example Proof (1)
•
•
P1: FS says (Owns A f1)
OwnerControlsRead:
FS says o,r,f. (Owns o f) 
(o says (MayRead r f)) 
(MayRead r f)
• Direct authorization via FS's signature:
sign(FS, "MayRead A f1")
: FS says (MayRead A f1)
20
Example Proof (2)
•
•
P1: FS says (Owns A f1)
OwnerControlsRead:
FS says o,r,f. (Owns o f) 
(o says (MayRead r f)) 
(MayRead r f)
• Complex proof constructed using "bind" and "return"
bind p = OwnerControlsRead in
bind q = P1 in
return FS (p A A f1 q sign(A,"MayRead A f1")))
: FS says (MayRead A f1)
21
Authority in AURA
• How to create the value sign(A, "") ?
• Components of the software have authority
– Authority modeled as possession of a private key
– With A's authority :
say("") evaluates to sign(A, "")
• What 's should a program be able to say?
– From a statically predetermined set (static auditing)
– From a set determined at load time
• In any case: log which assertions are made
22
Example Theorems
• T  P says T
"Principals assert all true statements"
• (P says T)  (P says (T  U))  (P says U)
"Principals' assertions are closed under deduction"
• Define "P speaks-for Q" = . (P says )  (Q says )
• (Q says (P speaks-for Q))  (P speaks-for Q)
"Q can delegate its authority to P"
(The "hand off"
axiom)
23
Example Non-theorems
• It is not possible to prove false: False  . 
"The logic is consistent"
• Without sign, it's not possible to prove:
"Principals are consistent"
P says False
• It is not possible to prove: .(A says )  
"Just because A says it doesn't mean it's true"
• If (Q = P) then there is no T such that:
(Q says T)  P says False
"Nothing Q can say can cause P to be inconsistent"
24
Outline
• AURA's programming model
• Authorization logic
– Examples
• Programming in AURA
– Dependent types
• Status, future directions, conclusions
25
Dynamic
Static
AURA Programming Language
Types: describe programs
int
FileHandle
string Prin
int -> int
Propositions: specify policy

A says 
(  )
.T
(Owns A fh1)
Programs: computations, I/O
3
fh1
"hello" A
say()
Evidence: proofs/credentials
sign(A, "")
bind
P
Programs
Policies
26
Dependent Types
• Policy propositions can mention program data
– E.g. "f1" is a file handle that can appear in a policy
– AURA restricts dependency to first order data types
– Disallows computation at the type level
• Programming with dependent types:
{x:T; U(x)}
(x:T)  U(x)
dependent pair
dependent functions
• Invariant: sign only types
– Computation can't depend on signatures
– But, can use predicates: {x:int; A says Good(x)}
27
Auditing Interfaces
• Type of the "native" read operation:
raw_read : FileHandle  String
• AURA's runtime exposes it this way:
read : (f:FileHandle) 
RT says (OkToRead self f) 
{ans:String; RT says (DidRead f ans)}
• RT is a principal that represents the AURA runtime
• OKtoRead and DidRead are "generic" policies
– The application implements its own policies about when it is
OKtoRead
28
Example File Server Program
(* assertions to do with FS access-control policy *)
assert Owns
: Prin -> FileHandle -> Prop;
assert MayRead : Prin -> FileHandle -> Prop;
Create application
specific propositions
(* RT's delegation to FS *)
let del = say((f:FileHandle) -> (p:Prin) -> FS says (MayRead p f)
-> OkToRead FS f)
(* FS code to handle a request *)
let handle (r:Request) =
match r with {
| readRequest q o f (x:o says MayRead q f) ->
match getOwner f with {
| Just {o':Owner; ownFS:FS says Own o' f} ->
if o = o' then
let FSproof = bind a = OwnerControlsRead in
bind b = ownFS in
Dynamically testing
return FS (a o q f b x))) in
values refines
let cap : OkToRead FS f = del f q FSproof
proof types.
Just (read f cap)
else …
| Nothing -> …
Call the AURA
|…
runtime.
Interface with AURA's
generic policy
Construct a
proof object
29
Outline
• AURA's programming model
• Authorization logic
– Examples
• Programming in AURA
– Dependent types
• Status, future directions, conclusions
30
AURA's Status
• AURA's core calculus:
– Rich type system that supports dependent authorization policies, recursive
types, etc., suitable for compiler intermediate language
– Type system is specified using the Coq proof assistant
– Correctness properties proved in Coq:
Type soundness proof is (nearly) complete (~7000 loc)
• Have implemented an interpreter in F#
– Many small examples programs
– Working on larger examples
– Goal: experience with proof sizes, logging infrastructure
• Planning to compile AURA to Microsoft .NET platform
– Proof representation / compatibility with C# and other .NET languages
31
Open Questions
• This story seems just fine for integrity, but what about
confidentiality?
– We have many ideas about connecting to information-flow analysis
– Is there an "encryption" analog to "signatures" interpretation?
• Other future directions:
–
–
–
–
Revocation/expiration of signed objects?
(Dependent) Type inference? Proof inference?
Connection to program verification?
Correlate distributed logs?
32
Security-oriented Languages
AURA
• A language with support for authorization and audit
• Authorization logic
• Dependent types
• Language features that support secure systems
www.cis.upenn.edu/~stevez
33
Thanks!
34
Auditing programs
•
•
What does the program do with the proofs?
More Logging!
– They record justifications of why certain operations were permitted.
•
When do you do the logging?
– Answer: As close to the use of the privileges as possible.
– Easy for built-in security-relevant operations like file I/O.
– Also provide a "log" operation for programmers to use explicitly.
•
Question: what theorem do you prove?
– Correspondence between security-relevant operations and log entries.
– Log entries should explain the observed behavior of the program.
•
Speculation: A theory of auditing?
35
Background: Authorization
• Enforcing authorization policies in distributed systems is difficult
– Policies can become complex
– Software that enforces the policies can be complex
• Authorization Logics:
– Abadi, Burrows, Lampson, Plotkin "ABLP" [TOPLAS 1993]
• somewhat ad hoc w.r.t. delegation and negation
– Garg & Pfenning
•
[CSFW 2006, ESORICS 2006]
a constructive modal logic that's very close to monomorphic DCC
– Becker,Gordon, Fournet
[CSFW 2007]
• Trust Management / KeyNote
– Blaze et al. [Oakland 1996…]
36
Dependency Core Calculus (DCC)
• A Core Calculus of Dependency
[Abadi, Banerjee, Heintz, Riecke: POPL 1999]
– Type system with lattice of "labels" TL
– Key property: noninterference
– Showed how to encode many dependency analyses: information flow,
binding time analysis, slicing, etc.
• Access control in a Core Calculus of Dependency
[Abadi: ICFP 2006]
– Essentially the same type system is an authorization logic
– Instead of TL read the type as "L says T"
– Curry-Howard isomorphism "programs are proofs"
37
Example AURA Program
assert Owns : Prin -> FileHandle -> Prop
data OwnerInfo : FileHandle -> Type {
| oinfo : (f:FileHandle) ->
(p:prin) ->
(pf (FS says (Owns p f))) ->
OwnerInfo f
}
getOwner : (f:FileHandle) ->
Maybe (OwnerInfo f)
38
More examples
assert OkToRead : FileHandle -> Prop
assert HasContents: FileHandle -> String -> Prop
data FileData : FileHandle -> Type {
| fd : (f:FileData) ->
(d:String) ->
(pf (FS says (HasContents f d))) ->
FileData
}
read : (f:FileHandle) -> (pf (FS says (OkToRead f)) ->
(FileData f)
39
Existing mechanisms are necessary
• Cryptographic protocols provide authentication
• Encryption protects data on the network
• OS / Firewalls provide coarse-grained isolation and
protection
40
…but not sufficient
•
•
•
•
•
Data must be decrypted during computation
Encryption must be used consistently with the policy
Regulating information-flow through software is hard
Auditing is at the wrong level of abstraction (Firewall, OS)
Policy is usually expressed at the application level
41