SAFE: A Declarative Trust-Agile System with Linked Credentials

SAFE: A Declarative Trust-Agile System with Linked Credentials

Vamsi Thummala
vamsi@cs.duke.edu
5th April 2016

Slides @ https://users.cs.duke.edu/~vamsi/safe/

Presenter Notes

Access Control Systems

TrustOverview-slides1

  • Who is the requesting principal?
  • What actions are requested?
  • What resources are requested?
  • What are the resource access policies?

Presenter Notes

Logical Trust Systems

TrustOverview-slides2

  • Credential discovery: Where to find the appropriate credentials for a given request?
  • Context management: How to build a proof context tailored to each request?
  • Delegation: How to delegate authority?

Presenter Notes

.fx: centerquote

Trust management deals with specifying and interpreting security policies, credentials, and relationships among entities in a system to reach an authorization decision.

Elements of Trust Logics

1. Properties of principals and objects are represented as logic statements

  • Principals may have secure names (e.g., public key/hash) or unique identifiers (e.g., email ID)
  • Build statements from atomic formulas (atoms) and logical operators

2. Predicates/atoms represent roles, attributes, capabilities, etc

3. Atoms are qualified with says operator: who says or believes it

4. Statements are authenticated and may be shared over a network

Example

1
2
3
4
5
Alice: predicate(?X) :- Alice: trustAnchor(?Root), ?Root: predicate(?X).
// Read as
Alice says predicate(?X) if 
  Alice says trustAnchor(?Root) 
  and ?Root says predicate(?X).

Presenter Notes

Multi-domain Cooperative IaaS Cloud
(NSF GENI Architecture)



GeniArch

  • GENI is a federated cloud with evolving trust structure
  • GENI is a trust-agile system: each cloud/resource provider may define local policies and provide local roots that govern the interactions with peers

Presenter Notes

Secure Name Resolution

secure-name-resolution

  • Hierarchical naming system: DNSSec
  • Web-of-trust: PGP
  • Naming as a foundation for reasoning about trust: SPKI/SDSI

Presenter Notes

Challenges of Building Trust Systems

challenges

Presenter Notes

Trust Logics from Literature

Logic variant Language Tractable Credential discovery Reduce to datalog Application
ABLP-based logics BAN Authentication
ABLP Authorization
Domain specific trust languages PolicyMaker Secure web pages
KeyNote Secure web pages
SPKI/SDSI ✓ (p) Secure web pages
RT* ✓ (p) ✓ (p) General
Datalog variants SD3 DNSSec
Binder General
PCA Grey Access to buildings
Insight Every tractable logic reduces to datalog
Claim Datalog-based logics are sufficiently powerful to express practical trust domains

Presenter Notes

Credential Discovery: Approaches


Approach Examples
Authorizer gathers credentials from a trusted local store ACLs, Capability lists
Subject provides credentials PCA
Authorizer issues on-demand distributed queries SD3, RT, Grey


Our approach: Controlled linking of credentials

  • Credentials are represented via a new abstraction called slogsets
  • A slogset is set of logic statements indexed by an issuer chosen name/token
  • Linking of slogsets reflects the delegation patterns of the application
  • Linking enables policy mobility

Presenter Notes

Problem

Practical end-to-end trust management


Thesis Statement

Delegation-driven credential linking and trust agility enable flexible, sound, and automated policy management for building secure networked systems

Presenter Notes

Contributions

contributions

Presenter Notes

Outline of the talk

Introduce SAFE system

  • Slog
  • Slogsets
  • Slang

Implementation

Applications

Summary

Presenter Notes

Secure Access For Everyone (SAFE)

Presenter Notes

SAFE Design Principle


Separation of concerns

Decouple trust logic from the app layer

  • Trust logic is factored out of an application behind a programmable API

Decouple credential gathering from proof evaluation

  • Introduces a scripting layer called "slang" encompassing the logic prover, "slog"

Decouple certificate encoding from credential representation

  • Introduces a flexible encoding for transport called "SafeX"

Presenter Notes

SAFE Design Overview


Safe-design

Presenter Notes

SAFE Components

Slang

  • Construct a proof context: Union of slogsets tailored to substantiate each request
  • Organize and link slogsets: To match the delegation patterns of the application
  • Publish slogsets: As certificates that encode trust assertions

Slog

  • Tractable logic: Based on the foundations of datalog
  • Support for practical trust domains: Hierarchical and range domains

SafeSets

  • Online storage with flexible transport: Authenticated slogsets with SafeX encoding

Presenter Notes

SAFE Logic (slog)

Presenter Notes

Slog Overview

Datalog-with-says

1
2
3
4
5
Alice: tag(?Subject, student) :- Bob: tag(?Subject, student). // A simple rule
Bob: tag(Charlie, student).     // A ground fact

Alice: tag(?Subject, student)?  // A query
?Who: tag(Charlie, student)?    // A query with a speaker variable

Delegation of attribute authority: fine-grained "speaks for"

1
2
// Alice delegates authority over student to Bob
Alice: tag(?Subject, student) :- Bob: tag(?Subject, student).

Attribute-based delegation of attribute authority

1
2
3
tag(?Subject, identityRegistrar) :- // Self delegates authority on 
         tag(?Geni, geniRoot),      // identityRegistrar to ?Geni
  ?Geni: tag(?Subject, identityRegistrar).

Presenter Notes

Slog Constraint Domains

Extends datalog to tractable functional domains

Domain Operations Description Example
Numeric $=, \ne, \lt, \leq, \gt, \geq, +, -, *, /$ Equality, inequality, arithmetic, and comparison $?X < 20$
String $=, \ne$ Equality, inequality, and ad hoc filtering (regular expressions) $?X = r``C.*?"$
Seq $=, \lt, \leq, \gt, \geq, <:, <<$ Equality, comparison, containment, and descendant $?X <: seq``[1, 2, 3, 4, 5]"$

Ranges and hierarchical domains are syntactic sugar of sequences

Example: Representing file paths

1
2
3
4
5
Alice: read(Bob, path"/user/*").
read(Bob, ?X) :- Alice: read(Bob, ?Y), ?Y < ?X. // < is a "child" operator

read(Bob, path"/user/bob")? // OK
read(Bob, path"/user/bob/home")? // Not OK

Presenter Notes

SAFE Language (slang)

Presenter Notes

Slang Overview

Multi-principals communicate signed slogsets via shared storage

SafeDesign

Presenter Notes

Organizing Slogsets

Support sets

  • Set of all upstream credentials that an authorizer needs to validate a given request
  • Credentials may be distributed and chained across multiple authorities

Anchor sets

  • Set of all locally established policies that an authorizer needs to verify before granting access to a request

Materializing slogsets

  • Indexed by issuer support sets
  • Indexed by subject support sets

Presenter Notes

Credential Linking

  • Linking reflects the delegation patterns of the application Linking
  • Trust logic is agnostic of linking, i.e., links are interpreted above logic
  • Policy mobility: Resource object authorities may define policies and attach them to the objects. These policies are retrieved, imported, and evaluated for access decision on the object.

Presenter Notes

Context-layer Scripting

Functional logic programming

Builtin function type Description
defcon constructs a slogset
defenv defines an environment variable
defun provides a native API (to invoke a function in the host language)
defguard provides a RESTful API for each guard method and executes a query

Slogsets templates

Enables sharing of logic content across its participants

Example: Delegation of attribute authority

1
2
3
4
5
6
7
8
9
defcon endorseByAttrDelegation(?TrustedRoot, ?Attr) :-
  spec('delegate authority on an attribute to a trustedRoot'),
  ''endorse/delegate/$Attr''{ // substitutes $Attr via lexical scoping
    endorse(?Entity, $Attr) :-
                 endorse(?Delegator, $TrustedRoot),
     ?Delegator: endorse(?Entity, $Attr).
     mkLink("subject/delegate/$Attr").
  }
end

Presenter Notes

Implementation

Presenter Notes

SAFE Architecture

SafeArch

Decouples the trust logic from the app layer

Caching at multiple levels

Entire system is built in Scala language

Presenter Notes

SafeSets Implementation

Built on the top of a off-the-shelf Key-Value store

Writes on the SafeSets server are authorized via SAFE itself

Parallel fetches use actor-based programming for asynchronous processing (Akka)

SafeSetsAkka

Presenter Notes

Applications

Presenter Notes

SAFE Applications

Application Description SLOC Delegation pattern Related systems
SafeSets Authorization for a simple key-value store 15 Linear "speaks for" validation; secure web proxies
SafeNS Secure naming service in SAFE 40 Hierarchy/DAG SDSI; SD3 certified evaluation
SafeCoda Secure cooperative analytics in the cloud 150 DAG DIFC; Penumbra: tag-based access control
SafeGENI Authorization system for NSF GENI 110 DAG RT*; ABAC

Presenter Notes

SafeGENI Workflow: Decentralized Policies

genflow

Local policies and selective trust anchors enables trust agility

Presenter Notes

SafeGENI Policies: An example

Guard policy to create a project

1
2
3
PA: createProject(?User) :-
  PA: identityRegistrar(?IdR),
  ?IdR: geniPI(?User).

Guard policy to create a slice

1
2
3
4
5
SA: createSlice(?User, ?Project) :-
  ?PA := rootID(?Project),
  SA: projectAuthority(?PA),
  ?PA: project(?Project),
  ?PA: createSlice(?User, ?Project).

Capabilities

1
2
3
capability(?Subject, ?Slice, ?Priv, ?Delegatable) :-
  ?Delegator: delegateCap(?Subject, ?Object, ?Priv, ?Delegatable),
  capability(?Delegator, ?Object, ?Priv, true).

Presenter Notes

Evaluation

  • Slog vs Slang overhead
  • Latency vs Throughput
  • Impact of caching

Experiment Setup

  • Authorizer experiments: 8-core Xeon processor
  • SafeSets cluster: 6 VMs each with single Xeon core
  • Workload is simulated based on application patterns

    - Lognormal for SafeNS

    - Geometric and logarithmic for SafeGENI

Presenter Notes

Microbenchmarks

function compute hash verify sig sign a set parse a set null inference fetch a set post a set
latency (ms) 0.13 0.56 12.14 2.2 0.09 3.8 22.4

  • Cost of inference with varying proof length and degree of backtracking $b_d$.

proofLength

5% overhead upto $b_d <= 10$ and proof length (#of unifications) $<= 500$

Presenter Notes

SafeSets Authorization with SAFE

  • SafeSets uses SAFE for post authorization and signing the requests.
  • Measure the overhead of post authorization guard check by SafeSets server, i.e., whether the requester possesses the speaksFor attribute

exp-safesets

Throughput drops by 20% and latency drops by 15%

Presenter Notes

SafeGENI

exp-safegeni

Presenter Notes

Impact of Caching

Geni Workload

Workload mix: 1024 users and 4096 slices. Logarithmic delegation chains: i.e., any user is at most $log_2{N}$ from accessing a slice.
- Baseline case: all certs are processed in their entirety; no caching involved
- Cold caching: certs are cached but proof contexts are build on-demand per each request
- Hot caching: with all caching enabled including the proof context cache

geni-cache

Presenter Notes

Summary

SAFE bridges the gap between theory and practice of trust logics by approaching the end-to-end trust management as a systems problem

Design principle: Separation of concerns

  • Slog: Maximally tractable trust logic
  • SlogSets: New abstraction for representing set of statements/credentials
  • Slang: Manages slogsets and builds tailored proof contexts
  • SafeSets: Online credential store
  • Service integration: Provides REST APIs to app layer

Potential new applications domains: Software-defined networks, IoT

Presenter Notes

Other topics not covered in this talk

  • Certificate management

  • Negation and safety restrictions in slog

  • Support for aggregation and indexing techniques at slang

  • Accountablity of SafeSets service

  • Flexible federation (peering) across multiple service providers

Presenter Notes

q

Presenter Notes

thankyou

Presenter Notes

Presenter Notes

Transport: Certificate Encoding

Encoded in Safe expressions (SafeX)

Example: Alice issues read credentials to Bob on a specified path

 1
 2
 3
 4
 5
 6
 7
 8
 9
10
11
12
13
14
15
cert #'application/slang;charset=utf8;hash=sha256' -> u'kM--9Mqbimxnsm0_...'(
  signedData(
    version('1'),
    issuer(u'1RF6d7jpvAVVsByofu7XLx4-O9Qhbd5eXLGhFSGQTps', nil, nil),
    subject(u'1RF6d7jpvAVVsByofu7XLx4-O9Qhbd5eXLGhFSGQTps', nil),
    validity('2015-05-11T00:50:00', '2017-05-11T01:00:00', 'PT24H'),
    cred #'application/slog;charset=utf8;hash=md5' -> ''{
      read(Bob, path"/user/*").
      read(?Subject, ?Path) :- Bob: read(?Subject, ?BPath), ?Path < ?BPath.
      link('1RF6d7jpvAVVsByofu7XLx4-O9Qhbd5eXLGhFSGQTps').
    },
    signatureAlgorithm('SHA256withRSA')
  ),
  signature(u'RyIJNdWTJzT7CBToNk51gWPF-37SYY4kukidAkL_xe4LwusiWo...')
).

Writes to a slogset are idempotent

Presenter Notes

Trust Logic: The Quest for Tractability

$\exists~{SOL} \subseteq NP^{TIME}$

Ronald Fagin [1974]

${FLP}^{\leq} \subseteq P^{TIME}$

Immerman; Vardi [1982]

${Datalog}^{Pure} \subseteq P^{TIME}$

Jeff Ullman [1986]

Presenter Notes

Trust Logics

ABLP-based logics

  • BAN Logic [1990]: A logic for authentication
    - Introduces the foundational "says" operator for logical authentication
  • ABLP Logic [1993]: A calculus for access control in distributed systems
    - First systematic analysis of properties to satisfy for authorization logics

Languages for Trust Management

  • PolicyMaker: Introduced the problem of decentralized trust management
  • SPKI/SDSI: Secure name resolution; privilege computation from auth certs
  • RT*: Set of multiple languages for expressing role-based trust

Datalog-based languages

  • SD3: DNSSec resolver written in logic
  • Binder: Communicating contexts

Proof-carrying authorization (PCA)

Presenter Notes

Certificate Management

Rotation

Supported through sub-principals

Revocation & Renewal

Simplified through SafeSets

Malicious content

Issuers may create potentially long certificate chains mounting DOS attacks. The authorizer can control the fetch by bounding the delegation length for a given link

Confidentiality

Set identifiers support limited confidentiality. Issuers can choose complementary approaches such as encryption for enhanced confidentiality

Presenter Notes

Safety in slog: Range Restriction

A slog rule is safe iff:

Each variable in a rule head also appears in a relational subgoal or a domain subgoal

1
2
Alice: tag(?Who, student)     :- Bob: tag(?Subject, student). // Unsafe
Alice: tag(?Subject, student) :- Bob: tag(?Subject, student). // Safe

Each variable in an arithmetic subgoal also appears in the relational subgoal or bound to a constant

1
2
isLessThan(?X, ?Y) :- ?X < ?Y, fact(?X, ?Y). // Unsafe: ?X and ?Y are unbound
isLessThan(?X, ?Y) :- fact(?X, ?Y), ?X < ?Y. // Safe

Note: Extending slog to function domains impacts declarative syntax; however, the slog compiler aids in pushing constraints to the right
No negated subgoal in a rule.

1
2
Alice:student(?Subject) :- !Bob:student(?Subject)? // Unsafe
Alice:student(?Who), Bob:student(?Subject)? // Safe

Presenter Notes

Tractable Declarative Trust Logic

DescriptionComplexity

Claim Datalog-based logics are sufficiently powerful to express practical trust domains

Presenter Notes

Elements of Trust Systems

TrustElements

Presenter Notes

SafeFlow

Comparison of IP addresses

1
2
3
4
5
Alice: delegate(Bob, ipv4"192.168.1.0/24").
authorize(Bob, ?X) :- Alice: delegate(Bob, ?Y), ?Y <: ?X. // <: is an "in" operator

authorize(Bob, ipv4"192.168.1.100")? // OK
authorize(Bob, ipv4"192.168.1.300")? // Not OK

Presenter Notes

SafeSets Guard Method

 1
 2
 3
 4
 5
 6
 7
 8
 9
10
11
12
13
14
15
16
17
defguard safesetsPost(?SetId, ?PostSetAsString) :-
  spec('validate the principal and verify the integrity of a slogset before posting'),
  ?PostSet    := parseSet(?PostSetAsString),
  ?Issuer     := getIssuer(?PostSet),
  ?Subject    := getSubject(?PostSet),
  ?IssuerKey  := getIssuerKey(?PostSet),
  ?SetName    := getName(?PostSet),
  ?SpeaksForRef     := fetch(getIssuerRef(?PostSet)),
  ?IsSignatureValid := verifySignature(?PostSet, ?IssuerKey),
  {
    import!($SpeaksForRef).
    authorize() :- $Subject: speaksFor($Issuer, $Subject).
    authorize() :- $Subject: speaksForOn($Issuer, $Subject, $SetName).
    $IsSignatureValid, authorize()?
  },
  localPost(?SetId, ?PostSetAsString)
end

Presenter Notes

SafeNS

safens

Presenter Notes