Transcript Collaborative Programming: Logic and Automated Reasoning

Collaborative Programming
Tim Hinrichs
University of Chicago
Collaborative Programming
Settings in which groups of people issue
instructions to computer systems.
– Cooperative goals
– Competitive goals
2
Collaborative Programming Languages
Principles of Collaboration
–
–
–
Information is combined.
No one knows everything.
People never agree on everything.
Required Properties of Collaborative
Programming Languages
–
–
–
Combinable instruction sets
Partial instruction sets
Conflicting instruction sets
3
Logical Languages
Benefits:
– Combination is relatively straightforward.
– Can express partial instruction sets.
– Can express conflicting instruction sets.
Drawback:
Processing logical languages, especially with
conflicts and incompleteness, can be
expensive relative to traditional
programming languages.
4
Example: Access Control for Files
/common
Files of interest: /alice
/bob
/alice
Alice rw, Bob r
/common
Everyone r
/bob
Bob rw, Alice r
/common
Everyone rw
5
Example: Access Control for Files
/common
Files of interest: /alice
/bob
/alice
Alice +rw, Bob +r-w
/common
Everyone +r-w
/bob
Bob +rw, Alice +r-w
/common
Everyone +rw
6
Applications
Applications
– Security (Authorization Policies)
– World Wide Web (Web forms)
Non-Applications
– Operating systems
– Compilers
7
Network Security
Local Area Networks
9
Network Policy Examples
“Every wireless guest user must send HTTP
requests through an HTTP proxy.”
“No phone can communicate with any private
computer.”
“Superusers have no communication
restrictions.”
10
Enforcement Today
10.0.0.1
Src IP
10.0.0.1
Port
80
Forward
10.0.0.25
10.0.0.25
11
NOX
Network Operating System
• Gives administrators control of the network by
exposing network events, e.g. new-flow, hostjoin, host-leave, user-authenticate.
• Requires no changes to current OSes.
• Does require changes to current routers.
• Relies on central controller.
12
NOX Operation
13
NOX Operation
SECURITY
POLICY
14
NOX Operation
15
Collaborative Programming?
Collaboration
– Standard network security approaches
allow admins a great deal of autonomy.
– Collaborative Programming techniques
preserve that sense of autonomy.
Programming
– Instructions tell computer system how to
route network communications.
16
FSL
FSL: Flow Security Language [Hinrichs2009]
Balances the desires to make expressing policies
natural and implementing policies efficient.
•Protocol
•User source
•Host source
•Access point source
•User target
•Host target
•Access point target
17
Features
•
•
•
•
•
Distributed policy authorship
External references
Conflict detection/resolution
Incremental policy authorship via priorities
High Performance: 104 queries/second
Layered language:
Prioritization
Conflict Resolution
Keywords
Logic
Data
18
Datalog with Attachments
Syntax
h :- b1,…,bn,c1,…,cm
•
•
•
•
h must exist.
Every variable in the body must occur in h.
No external reference occurs in h.
Nonrecursive sentence sets.
Semantics
– Statement order is irrelevant.
– Every sentence set is satisfied by exactly one model.
19
Keyword: allow
“Superusers have no communication
restrictions.”
allow(Usrc,Hsrc,Asrc,Utgt,Htgt,Atgt,Prot)
:-
superuser(Usrc)
superuser(bob)
superuser(alice)
20
Keyword: deny
“No phone can communicate with any private
computer.”
deny(Usrc,Hsrc,Asrc,Utgt,Htgt,Atgt,Prot) :phone(Hsrc) , private(Htgt)
deny(Usrc,Hsrc,Asrc,Utgt,Htgt,Atgt,Prot) :private(Hsrc) , phone(Htgt)
private(X) :- laptop(X)
private(X) :- desktop(X)
21
Keyword: visit
“Every wireless guest user must send HTTP
requests through a proxy.”
visit(Usrc,Hsrc,Asrc,Utgt,Htgt,Atgt,Prot,httpproxy)
:-
guest(Usrc) , wireless(Asrc) , Prot=http
22
Current Keyword List
• allow: allow the flow
• deny: deny the flow
• visit: force the flow to pass through an intermediary
• avoid: forbid the flow from passing through an
intermediary
• ratelimit: limit on Mb/second
23
Collaborative Programming versus
Policy Enforcement
FSL is a Collaborative Programming language
Combinable, partial, conflicting instruction sets
deny
avoid
visit
allow
ratelimit
deny
avoid
visit
allow
ratelimit
Authorization systems cannot enforce partial
or conflicting security policies.
24
FSL Usage Overview
Policy
1
Policy
n
Combined
Policy
Analysis
Engine
Authorization
System
25
Conflict Resolution
• Most restrictive: choose instructions that give users
the least rights.
• Most permissive: choose policy instructions that
give users the most rights.
Implementable using standard Datalog tools.
Most restrictive for just allow and deny…
P |=c deny(…) if P |= deny(…)
P |=c allow(…) if P |/= deny(…)
26
Deployment Experiences
• FSL has been used for 10 months on a small
internal network (about 50 hosts).
• We are preparing for two larger deployments
(of hundreds and thousands of hosts).
• So far, policies are expressed over just a few
classes of objects.
Thus, we expect policies to grow slowly with the
number of principals.
27
Related Work
Authorization Language Features in Literature
•
•
•
•
•
•
•
•
•
Logic: Logic programming, FOL, Modal, Linear
With or without recursion
With or without negation
For citations, see
Handling conflicts
[Hinrichs2009].
Delegation
History and future-dependent policies
Several metalevel operations
Centralized/decentralized enforcement
Efficiency
28
Datalog as a
Collaborative Programming Language
Expressing conflicts requires keywords.
Benefit:
Conflicts can be detected and resolved using
traditional inference tools.
Drawback:
All possible conflicts must be anticipated at
language-design time.
29
World Wide Web Forms
Web Forms
31
32
Construction and Maintenance
Central difficulty: constraints interact.
Small constraint changes can correspond to large
implementation changes.
Approach: users specify constraints and the
computer system generates a spreadsheet.
Small constraint changes now correspond to little
work for users.
33
Websheet Demo
Live Demo
34
Collaborative Programming?
Collaboration
Maintenance of web forms requires
collaboration, whether between different
people or different instances of the same
person.
Programming
Specification-based programming
35
Logical Foundations
Cells: unary predicates, e.g. drive and engine.
Constraint: quantifier-free, function-free first-order
formula, e.g.
“if the engine is small then the drive is 4x2.”
drive(4x2) V engine(small)
Cell assignment: ground literals, e.g.
drive(4x4)
drive(4x2)
36
Conflict Detection Proposal
Check if for spreadsheet S
S |= drive(4x4) and S |= drive(4x4)
37
Problem
38
Problem Explanation
S: drive(4x2) V engine(small)
drive(4x4)
drive(4x2)
engine(small)
engine(large)
S is inconsistent. Therefore for every
predicate p and value a,
S |= p(a) and S |= p(a)
39
Paraconsistent Entailment
Definition (Existential Entailment [Hunter98])
 existentially entails  if there is some
satisfiable subset of  that entails .
40
Performance Demands
Need to compute existential entailment
in real-time.
Each cell click requires computing 2n
entailment queries, where n is the
domain of the cell.
A change to one cell may require
updates to many other cells.
41
Related Work
Logical spreadsheets
– Stanford (Kassoff and Genesereth)
– Stony Brook (Ramakrishnan, Ramakrishnan,
Warren)
– University of Texas (Gupta and Akhter)
– Carnegie Mellon-Qatar (Cervesato)
– Several in industry
DARPA small business program in 2004
Logical Spreadsheets Workshop in 2005
See [Kassoff2007]
42
Classical Logic as a
Collaborative Programming Language
Conflicts require no special machinery.
Benefit:
Conflicts do not need to be anticipated by
the language designer.
Drawback:
Automated reasoning tools must implement
a paraconsistent version of entailment.
43
Final Words
Comparison
Logic
Datalog
FOL
Conflicts
keywords
built-in
Reasoning
Semantics
standard
1 model
paraconsistent
0,1,2,…
models
How do we leverage the strength of Datalog
while retaining the strength of FOL?
45
Compilation Approach
FOL
Datalog
Two phases:
1. Compilation for traditional entailment.
2. Compilation for existential entailment.
46
Compiler
Definition (Parameterized Theory-Completion):
Suppose I is a satisfiable set of constraints. A complete
theory  is a parameterized theory-completion of I if
for each predicate p, there are predicates p+ and p- s.t.
for every complete theory C,
C U I |=E p(a) iff C U  |= p+(a)
C U I |=E p(a) iff C U  |= p-(a)
47
Summary
Language
Compiler
Datalog
First-order logic
FOL to Datalog
Logic
Datalog
FOL
Conflicts
Reasoning
keywords
standard
built-in
paraconsistent
Run-time
Environment
Example
Network
Security
Logical
Spreadsheets
48
[Hinrichs2008a] T. Hinrichs. Collaborative Programming. IJCAR
Workshop on Practical Aspects of Automated Reasoning, 2008.
http://people.cs.uchicago.edu/~thinrich/
papers/hinrichs2008collaborative.pdf
[Hinrichs2009] T. Hinrichs, et. al. Design and Implementation of a Flowbased Security Language. Under review. Available upon request.
[Kassoff2007a] M. Kassoff and M. Genesereth. PrediCalc: A Logical
Spreadsheet Management System. Knowledge Engineering
Review, 22(3), 2007, pp. 281-295.
http://logic.stanford.edu/~mkassoff/papers/predicalc.pdf
[Kassoff2007b] M. Kassoff and A. Valente. An introduction to logical
spreadsheets. Knowledge Engineering Review, 22(3), 2007, pp.
213-219.
[Hunter1998] A. Hunter. Paraconsistent Logics. In Handbook of
Defeasible Reasoning and Uncertain Information.
http://www.cs.ucl.ac.uk/staff/a.hunter/papers/para.ps
[Hinrichs2008b] T. Hinrichs and M. Genesereth. Injecting the How into
the What. KR 2008. http://people.cs.uchicago.edu/
~thinrich/papers/hinrichs2008injecting.pdf
49
Questions
50
Backup
According to Webster’s…
col•lab•o•ra•tive
produced or conducted by two or more parties; can
be cooperative or competitive.
pro•gram•ming
the act of issuing instructions, esp. to computer
systems.
in•struc•tions
detailed information telling how something should
be done, operated, or assembled.
52
Collaborative Programming Overview
Components
Language
Run-time
Environment
Compiler
First-order logic
Logic programming
Description logics
SAT solvers
Prolog
Traditional PL
Use Case (Scripting Language)
Software
Language
Compiler
Run-time
53
Web Form Implementation
Comparison
Logic
Datalog
FOL
Conflicts
keywords
built-in
Reasoning
Semantics
standard
1 model
paraconsistent
0,1,2,…
models
How do we leverage the strength of Datalog
while retaining the strength of FOL?
55
Compilation Approach
FOL
Datalog
Two phases:
1. Compilation for traditional entailment.
2. Compilation for existential entailment.
56
Theory Completion
Central difficulty:
A theory with many models (FOL) must be
converted to a theory with one model (Datalog).
Consequently:
• Compiling FOL to Datalog is a form of theory
completion.
• Spreadsheet compilation is a parameterized form of
theory completion.
57
Parameterized Theories
The theory that is queried to determine
conflicts is comprised of two pieces:
FOL Constraints
Incomplete (I)
Current Cell Values
Complete (C)
Need a compiler that produces a Datalog program that
enumerates the logical consequences for ANY
complete theory C.
58
Compiler
Definition (Parameterized Theory-Completion):
Suppose I is a satisfiable set of constraints. A complete
theory  is a parameterized theory-completion of I if
for each predicate p, there are predicates p+ and p- s.t.
for every complete theory C s.t. C U I is satisfiable,
C U I |= p(a) iff C U  |= p+(a)
C U I |= p(a) iff C U  |= p-(a)
59
Example
FOL
Constraints:
engine(small)  trans(5-speed)
Datalog when engine has a value.
engine+(X) :- engine(X)
engine-(X) :- engine(X)
trans+(X) :- X=5-speed, engine(small)
trans-(X) :- X=5-speed, engine(small)
60
Compiler
Given constraints I,
1. Compute resolution closure of I (Res[I]).
2. For each clause in Res[I], produce a series
of Datalog queries, introducing 2 keywords
per predicate.
NB: Res[I] is always finite because I has only
unary predicates.
See [Hinrichs2008b] for more details.
61
Existential Entailment
Two possible sources of inconsistency:
• Constraints (I)
• Cell assignment (C)
• Constraints and cell assignments (C U I)
It turns out that the compilation
technique just described implements a
form of Existential Entailment.
62
Summary
Language
Compiler
Run-time
Environment
Datalog
First-order logic
FOL to Datalog
Datalog eval
Logic
Datalog
FOL
Conflicts
Reasoning
keywords
standard
built-in
paraconsistent
Example
Network
Security
Logical
Spreadsheets
63
Intro Backup
Database Applications
65
WWW Privacy
66
FSL Backup
Negation
“Every user except a guest can ssh into any
server.”
allow(Usrc,Hsrc,Asrc,Utgt,Htgt,Atgt,ssh)
:-
guest(Usrc) , server(Htgt)
68
Traditional Security Mechanisms
NAT: disable incoming connections for laptops
deny(Usrc,Hsrc,Asrc,Utgt,Htgt,Atgt,Prot) :laptop(Htgt)
VLAN: isolate machines a,b,c
vlan(a), vlan(b), vlan(c)
deny(Usrc,Hsrc,Asrc,Utgt,Htgt,Atgt,Prot) :vlan(Hsrc),
vlan(Htgt)
deny(Usrc,Hsrc,Asrc,Utgt,Htgt,Atgt,Prot) :-
vlan(Hsrc), vlan(Htgt)
69
Query Processing Example
“No phone can communicate with any private
computer.”
deny(Usrc,Hsrc,Asrc,Utgt,Htgt,Atgt,Prot) :phone(Hsrc) , private(Htgt)
deny(Usrc,Hsrc,Asrc,Utgt,Htgt,Atgt,Prot) :private(Hsrc) , phone(Htgt)
private(X) :- laptop(X)
private(X) :- desktop(X)
70
Example Compiled
bool deny (Usrc,Hsrc,Asrc,Utgt,Htgt,Atgt,Prot) {
return (phone(Hsrc) && private(Htgt)) ||
(private(Hsrc) && phone(Htgt));
}
bool private(X) {
return laptop(X) || desktop(X);
}
Assume the existence of functions for phone,
laptop, desktop.
71
Access Control Decision-Making
Complexity
Query processing is PSPACE-complete in the size of
the policy.
If the number of arguments are bounded by a
constant, query processing takes polynomial time
in the size of the policy.
If the tallest possible call stack is 1 (ignoring external
references), then query processing takes linear
time in the size of the policy.
72
Implementation Tests
Flows/s
0 rules
103,699
Mem
(MB)
0
Rule
Matches
0
100 rules
100,942
1
2
500 rules
85,373
1
4
1,000 rules
76,336
2
10
5,000 rules
54,416
9
30
10,000 rules
46,956
38
52
73
Additive Elaboration
To tighten a FSL security policy, one
needs only to add statements to it.
The conflict resolution strategy ensures
that the most restrictive constraints are
used.
To relax a FSL policy, it is therefore
insufficient to simply add statements.
74
Relaxing Security
Borrow a mechanism from Cascading Style
Sheets (CSS): cascades.
To relax security, FSL allows one policy to be
overridden by another policy.
P1 < P 2
Any request constrained by P2 is only
constrained by P2.
75
Algorithms
Group Normal Form: every rule body consists
only of external references (and =).
Flattened Cascades: a policy cascade
expressed as a flat policy.
Conflict Conditions: conditions on external
references under which there will be a
conflict.
Conflict-free Normal Form: equivalent policy
(under conflict resolution) without conflicts.
76
Related Work Comparison
•
•
•
•
•
•
•
•
Not using FOL, Modal logic, Linear logic
No existential variables
No recursion
Fixed conflict resolution scheme
No delegation
No history/future-dependent policies
Centralized enforcement
Limited metalevel operations
• Access control decisions are constraints.
• Conflict resolution produces constraint set
77
Core Language Application:
Conflict Resolution Language
One keyword: resolve, and one external
reference: constraint
P1
resolve(deny) :- constraint(deny)
resolve(deny) :- constraint(avoid(X)),
constraint(visit(X))
P2
resolve(avoid(X)) :- constraint(avoid(X))
resolve(visit(X)) :- constraint(visit(X))
P3
resolve(allow) :- constraint(allow)
78
Ongoing Work
Currently, each flow initiation requires
contacting a central controller.
The route for that flow is cached at the router.
Working to generalize this caching scheme.
Each trip to the central controller caches more than
just the route for one flow.
79
Spreadsheet Backup
Mathematical Model
• Each cell is a variable: V
• Each variable has a domain: DV
• Constraints require that certain combinations
of variables be assigned certain combinations
of values: CV
The purpose of a spreadsheet is to help users
enter data by providing feedback when
constraints are violated.
81
Performance Demands
Need to compute existential entailment
in real-time.
Each cell click requires computing O(n)
entailment queries, where n is the
domain size of the cell.
A change to one cell may require
updates to many other cells.
82
Compilation Backup
Experiments: Two Formulations
FHL:
color(X,Y)  adj(X,Z)  color(Z,Y)
color(X,Y)  node(X)  hue(Y)
 …  X=an
hue(X)  X=b1  …  X=bm
node(X)  X=a1
adj(X,Y)  …
X1…Xn. color(a1,X1)  …  color(an,Xn)
Datalog:
ans(X,Y,Z) :- hue(X), hue(Y), XY, hue(Z), YZ
hue(b1) hue(b2) … hue(bm)
84
Experiments: Details
• For graph sizes 25, 30, 35,…, 60, tested 20
randomly generated graphs.
• For each graph, tested 3 different hue sets.
– k is the maximum degree of the graph.
– Graph can always be colored with k+1 colors.
– Tested k+1, 2/3k, and 1/3k hues.
• Compilation cost not counted
85
Experiments: Results I
86
Experiments: Results II
87
Scrap
External References
Group definitions change far more frequently
than security policies.
External references allow a policy to remain
unchanged even if the groups it relies upon
change often.
visit(Usrc,Hsrc,Asrc,Utgt,Htgt,Atgt,Prot,httpproxy)
:-
guest(Usrc) , wireless(Asrc) , Prot=http
89
Implementing Existential Entailment
Resolution-based approach: only generate
resolvents whose premises are consistent.
DATALOG-based approach: generate
database queries that enumerate the
existentially-entailed consequences.
90
Spreadsheet Compilation
FOL
Constraints:
Cell
Assignments:
drive(4x2) V engine(small)
drive(4x4)
drive(4x2)
engine(small)
engine(large)
Problem: Compile FOL constraints C to Datalog
D s.t. for every cell assignment A
D U A |=D []p(a) iff C U A |=E []p(a)
91
Message
Logical languages are powerful tools in
collaborative settings.
Collaboration breeds conflict.
Embrace conflicts!
92