Transcript Declarative Networking - University of Pennsylvania

Towards a Declarative Language and
System for Secure Networking
Martín Abadi1,2, Boon Thau Loo3
1Microsoft Research Silicon Valley, 2UC Santa Cruz, 3University of Pennsylvania
Motivation
Designing secure network protocols is hard

Imperative languages makes process tedious and
error-prone
Explore the use of declarative languages for
secure networking:


“Ask for what you want, not how to
implement it”
Success of database research
 70’s – today: Database research has revolutionized data
management
Approach
Examine two classes of declarative languages:


Database query language for declarative networking
Logic-based access control languages in distributed
systems
Contribution:


Compare these two classes of languages
Propose a unifying declarative language and system
Why might this be useful?
Intellectually interesting to compare two languages
Single declarative language and system



Ease of management
Many useful examples: authenticated routing protocols,
secure overlays, DNSSEC, trust management in shared
testbeds, P2P information sharing, etc.
Fine-grained control over interaction between security and
network protocol
 Potential for cross-layer analysis and optimizations
Distributed query engines to process security policies
Outline
Background:


Declarative networking
Access control & related languages
Introduction to Datalog
Network Datalog and Binder languages
Secure Network Datalog


Language design
Examples
Future Directions
Declarative Networking
A declarative framework for networks:


Declarative specifications of networks,
compiled to distributed dataflows
Distributed query engine to execute
distributed dataflows to implement protocols
Observation:

Recursive queries are a natural fit for routing

Network Datalog (NDlog) language
A Declarative Network
messages
Dataflow
Dataflow
messages
Dataflow
Dataflow
messages
Dataflow
Distributed
recursive query
Dataflow
Traditional Networks
Network State
Network protocol
Network messages
Declarative Networks
Distributed database
Recursive Query Execution
Distributed Dataflow
Declarative Networking
Declarative Routing [SIGCOMM ’05]:
Extensible Routers (balance of flexibility, efficiency and
safety).
 Textbook routing protocols (3-8 lines)
Declarative Overlays [SOSP ’05]:
 Rapid prototyping of new overlay networks
 Chord DHT overlay routing (47 lines)
 Narada Mesh (16 lines)
Database Fundamentals [SIGMOD ‘06]
 Languge, execution and optimizations

System available: http://p2.cs.berkeley.edu
Access Control
Central to security, pervasive in computer systems
Model:




objects, resources
requests for operations on objects
sources for requests, called principals
a reference monitor to decide on requests
Principal
Do
operatio
n
Reference
Monitor
guard
Object
Logics in Access Control
Logical tools and ideas have been used to
explain and improve access control
Logic-based languages: Binder, SD3, D1LP,
SecPAL, etc.
Trust management
We focus on Binder:



Simple design,
Most similar to NDlog
Promises relatively straightforward unification
with NDlog
Key Insight
Binder and NDlog are based on logic and Datalog
Extends Datalog in surprisingly similar ways


Notion of context (location) to identify components (nodes) in a
distributed system
Suggests possibility to unify both languages
Similar observation:


Martín Abadi. “On Access Control, Data Integration, and Their
Languages.”
Comparing Tsimmis and Binder
Outline
Background:


Declarative networking
Access control & related languages
Introduction to Datalog
NDlog and Binder languages
SeNDlog


Language design
Examples
Future Directions
Review of Datalog
Datalog rule syntax:
<result>  <condition1>, <condition2>, … , <conditionN>.
Head
Body
Types of conditions in body:


Input tables: link(src,dst) predicate
Arithmetic and list operations
Head is an output table

Recursive rules: result of head in rule body
All-Pairs Reachability
R1: reachable(S,D)  link(S,D)
R2: reachable(S,D)  link(S,Z), reachable(Z,D)
“For all nodes
S,D, is a link from node a to node b”
link(a,b)
– “there
If there is a link from S to D, then S can reach D”.
reachable(a,b) – “node a can reach node b”
Input: link(source, destination)
Output: reachable(source, destination)
All-Pairs Reachability
R1: reachable(S,D)  link(S,D)
R2: reachable(S,D)  link(S,Z), reachable(Z,D)
“For all nodes S,D and Z,
If there is a link from S to Z, AND Z can reach D, then S
can reach D”.
Input: link(source, destination)
Output: reachable(source, destination)
Network Datalog
Location
Specifier “@S”
R1: reachable(@S,D)  link(@S,D)
R2: reachable(@S,D)  link(@S,Z), reachable(@Z,D)
reachable(@M,N)
Query: reachable(@a,N)
link
Input table:
Output table:
All-Pairs Reachability
link
link
link
@S
D
@S
D
@S
D
@S
D
@a
b
@b
c
@c
b
@d
c
@b
a
@c
d
a
b
c
d
reachable
reachable
reachable
reachable
@S
D
@a
b
@a
c
@b
c
@a
d
@b
d
@S
D
@S
D
@S
D
@b a
Query: reachable(@a,N)
@c
a
@d
a
@c
b
@d
b
@c
d
@d
c
Implicit Communication
A networking language with no explicit communication:
R2: reachable(@S,D)  link(@S,Z), reachable(@Z,D)
Data placement induces communication
Path Vector in NDlog
R1: path(@S,D,P)  link(@S,D), P=(S,D).
R2: path(@S,D,P)  link(@S,Z), path(@Z,D,P2), P=SP2.
Query: path(@S,D,P)
Add S to front of P2
Input: link(@source, destination)
Query output: path(@source, destination, pathVector)
Previous work:
- Communication patterns are the same as the actual path vector protocol
- Easy to compose new protocols (distance-vector, link-state, multicast, etc)
Execution Plan
UDP
Rx
Round
Robin
Network
Out
CC
Tx
Messages
Queue
Queue
Messages
lookup
CC
Rx
Network
In
lookup
path
...
UDP
Tx
Demux
link
Local Tables
Single P2 Node
Nodes in execution plan (“operators”):



Network operators (send/recv, cc, retry, rate limitation)
Relational operators (selects, projects, joins, aggregates)
Flow operators (mux, demux, queues)
Binder
Logic-based language for access control
Similar to Datalog, with the special construct “says”
Rules in different context
Export: Alice says may-access(charlie,o,read).
Alice’s context
A1: may-access(P,O,read) :- good(P).
A2: may-access(P,O,read) :- bob says may-access(P,O,read).
Import: bob says may-access(charlie,o,read).
Export: bob says may-access(charlie,o,read)
Bob’s context
may-access(charlie,o,read).
Notion of “Says”
“says” abstracts the details of authentication
When “p says s”, p may transmit s in a variety of ways:




on a local channel via a trusted operating system within
a computer, on a physically secure channel between two
machines,
on a channel secured with shared-key cryptography, or,
in a certificate with a public-key digital signature.
Comparing Binder and NDlog
Trusted vs untrusted networks

NDlog:
 Location relates to data placement. E.g. link(@X,Y).
 Global rules:


Binder:
r(@X,Y) :- l(@X,Z), r(@Z,Y).
 Communication happens via “says”
 Import and export of facts into context

may-access(P,O,read) :- bob says may-access(P,O,read).
Bottom-up vs Top-down evaluation
Export of derived tuples:


Binder: no integration of security policy with export of data
NDlog: location specifier in rule head
Secure Network Datalog (SeNDlog)
Unifies Binder and NDlog
Goals of the language:




Expressive as Binder and NDlog
Supports authenticated communication and
enables differentiation of roles
Supports both trusted and untrusted environments
Amenable to execution and optimizations in
distributed query engines
 Bottom-up evaluation strategy
 Incremental continuous execution model
SeNDlog
At N,
E1:
E2:
E3:
E4:
p(X,Y) :- p1(X), p2(Y).
p(X,Y,W) :- Y says p1(X), Z says p2(W).
p(Y,Z)@X :- p1(X), Y says p2(Z).
Z says p(Y)@X :- Z says p(Y), p1(X).
Important features:
- Local principle (address, address/key, address/key/username)
- “Localized” rule bodies within context
- Import predicates. “says” construct – different levels of “says”
- Export predicates with location specifiers
- Honesty constraint
Example 1:
Authenticated Path Vector Protocol
At Z,
Z1: path(Z,X,P) :- neighbor(Z,X), P=(Z,X).
Z2: path(Z,Y,P) :- X says advertise(Y,P).
Z3: advertise(Y,P1)@X :- neighbor(Z,X), path(Z,Y,P), P1=XP.
p(@a,d,[a,b,c,d])
a
p(@b,d,[b,c,d])
b
p(@c,d,[c,d])
c
b says advertise(d,[a,b,c,d]) c says advertise(d,[b,c,d])
d
Example 2:
Secure DHT Identifiers
Security weakness in DHT – malicious nodes
occupy a high part of key space
Solution: certified node identifiers from CA
5 additional rules to P2-Chord
Details in the paper.


Nodes have different roles: CA, landmark, joining
node, etc.
Certificates can be forwarded from one node to
another:
 Use of honesty constraint.
Another example: DNSSEC
Ongoing Work
Implementation in P2 system:




“says” construct
Communication via signed certificates
Rule bodies within context
Implement variety of secure networks. E.g. DNSSEC, secure
routing, secure DHTs, trust management in extensible
testbeds, P2P information sharing, your suggestions!
Cross-layer analysis and optimizations


Exploit fine-grained control over security and networks.
Authenticity of routing table entries
 Logic proof why it is there. Trusted but not trustworthy?

Optimize protocols to favor trusted nodes
Future Work
Query language issues:



Logic-based trust management: SD3, SecPAL, D1LP
Distributed Datalog: ubQL, d3log
Data integration: Tsimmis
Different approach:



We started from Binder and NDlog
Lots of domain knowledge but biased
What if we design from scratch?




Sending / receiving & Distributed computations
Notion of context
Trust relationships
Continuous incremental evaluations
Thank You