Applications of Computational Logic
Tim Hinrichs
University of Chicago
COMPULOG Summer School
July 24-27, 2008
Collaborative Programming
Settings in which groups of people issue
instructions to computer systems.
– Cooperative goals
– Competitive goals
COMPULOG Summer School 2008
2
Collaborative Programming Languages
Principles of Collaboration
– No one knows everything.
– People never agree on everything.
Required Language Properties
– Partial instruction sets
– Conflicting instruction sets
– Combinable instruction sets
COMPULOG Summer School 2008
3
Logical Languages
Benefits:
– Can express partial instruction sets.
– Can express conflicting instruction sets.
– Combination is relatively straightforward.
Drawback:
Processing logical languages, especially with
conflicts and incompleteness, can be
expensive relative to traditional
programming languages.
COMPULOG Summer School 2008
4
Network Security
Local Area Networks
COMPULOG Summer School 2008
6
Network Policy Examples
“Every wireless guest user must send http
requests through an http-proxy.”
“No phone can communicate with any private
computer.”
“Two superusers have no communication
restrictions.”
COMPULOG Summer School 2008
7
Desiderata
• Collaborative policy authoring
• High Performance: 105 queries per
second.
• Interact with outside world.
COMPULOG Summer School 2008
8
FSL
FSL: Flow Security Language [Hinrichs2008b]
Multiple network administrators issue instructions for
each message/flow.
•Protocol
•User source
•Host source
•Access point source
COMPULOG Summer School 2008
•User target
•Host target
•Access point target
9
Basic Rules
“Two superusers have no communication
restrictions.”
allow(Usrc,Hsrc,Asrc,Utgt,Htgt,Atgt,Prot)
:-
superuser(Usrc) , superuser(Utgt)
superuser(bob)
superuser(alice)
COMPULOG Summer School 2008
10
Rule Sets
“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)
laptop(lap1)
desktop(desk1)
phone(phone1)
COMPULOG Summer School 2008
No Recursion
11
More Keywords
“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
guest(alice)
guest(bob)
wireless(wap1)
COMPULOG Summer School 2008
12
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
COMPULOG Summer School 2008
13
Negation
“Every user except a guest can ssh into
any server.”
allow(Usrc,Hsrc,Asrc,Utgt,Htgt,Atgt,ssh)
:-
guest(Usrc) , server(Htgt)
COMPULOG Summer School 2008
14
FSL Overview
FSL is built on nonrecursive datalog with negation
without existential variables or safety.
Keywords/queries
allow: allow(Usrc,Hsrc,Asrc,Utgt,Htgt,Atgt,Prot)
deny: deny(Usrc,Hsrc,Asrc,Utgt,Htgt,Atgt,Prot)
visit: visit(Usrc,Hsrc,Asrc,Utgt,Htgt,Atgt,Prot,host)
avoid: avoid(Usrc,Hsrc,Asrc,Utgt,Htgt,Atgt,Prot,host)
In security policies, visit and avoid require a constant in
the last argument of the consequent.
COMPULOG Summer School 2008
15
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)
COMPULOG Summer School 2008
16
Example Compiled
bool deny (Usrc,Hsrc,Asrc,Utgt,Htgt,Atgt,Prot) {
(phone(Hsrc) && private(Htgt)) ||
(private(Hsrc) && phone(Htgt))
}
bool private(X) {
laptop(X) || desktop(X)
}
Assume the existence of functions for phone, laptop,
desktop.
COMPULOG Summer School 2008
17
Conflicts and Incompleteness
Conflicts are easy to express:
deny(Usrc,Hsrc,Asrc,Utgt,Htgt,Atgt,Prot) 
a(Hsrc)  b(Htgt)
allow(Usrc,Hsrc,Asrc,Utgt,Htgt,Atgt,Prot) 
a(Hsrc)  b(Htgt)
Incompleteness is easy to express:
What should the system do if a(Hsrc)  b(Htgt)?
COMPULOG Summer School 2008
18
Collaborative Programming versus
Policy Enforcement
FSL meets the requirements of
Collaborative Programming languages
– Partial instruction sets
– Conflicting instruction sets
– Combinable instruction sets
Authorization systems cannot enforce
incomplete or conflicting security
policies.
COMPULOG Summer School 2008
19
FSL Usage Overview
Policy
1
Policy
n
Combined
Policy
Analysis
Engine
COMPULOG Summer School 2008
Authorization
System
20
Conflict Resolution Strategies
• No conflicts: conflicts are errors.
• Most secure: choose instructions that are most
secure.
• Most permissive: choose policy instructions that
give users the most rights.
• Cancellation: a flow with conflicting constraints has
no constraints.
COMPULOG Summer School 2008
21
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.
COMPULOG Summer School 2008
22
Logical Spreadsheets
Logical Spreadsheets
See [Kassoff2007]
COMPULOG Summer School 2008
24
Websheets
COMPULOG Summer School 2008
25
COMPULOG Summer School 2008
26
Websheet Demo
Live Demo
COMPULOG Summer School 2008
27
Collaborative Programming?
Collaboration
– Constraints sometimes originate from
multiple sources.
– Data source often different than constraint
source.
“Programming” is a bit of a stretch.
COMPULOG Summer School 2008
28
Logical Foundations
Cells: unary predicates, e.g. drive and engine.
Constraint: quantifier-free, function-free firstorder 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)
COMPULOG Summer School 2008
29
Conflict Detection I
Check if for spreadsheet S
S |= drive(4x4) and S |= drive(4x4)
COMPULOG Summer School 2008
30
Problem
COMPULOG Summer School 2008
31
Problem Explanation
S: drive(4x2) V engine(small)
drive(4x4)
drive(4x2)
engine(small)
engine(large)
S is inconsistent. Therefore
S |= drive(4x4) and S |= drive(4x4)
And for every other predicate p and value a,
S |= p(a) and S |= p(a)
COMPULOG Summer School 2008
32
Paraconsistent Entailment
Definition (Existential Entailment [Hunter98])
 existentially entails  if there is some set of
sentences  such that
•  
•  is consistent
•  |= 
COMPULOG Summer School 2008
33
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.
COMPULOG Summer School 2008
34
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.
COMPULOG Summer School 2008
35
Spreadsheet Implementation
Comparison
Logic
Conflicts
datalog
keywords
FOL
built-in
Reasoning
Semantics
standard
1 model
paraconsistent
0,1,2,…
models
How do we leverage the strengths while
avoiding the weaknesses?
COMPULOG Summer School 2008
37
Compilation Approach
FOL
COMPULOG Summer School 2008
Datalog
38
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)
COMPULOG Summer School 2008
39
Theory Completion
Semantic 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.
COMPULOG Summer School 2008
40
Example
FOL
Constraints:
drive(4x2) V engine(small)
Want a Datalog/Prolog program that given
ground atoms for engine enumerates the
values of drive that are entailed.
ent_drive(X) :- X=4x2, engine(small)
What about negative values for engine?
ent_notengine(X) :- X=small,not(drive(4x2))
COMPULOG Summer School 2008
41
More Generally
Given FOL constraints C,
1. Compute resolution closure of C (Res[C]).
2. For each clause in Res[C], produce a series
of Datalog queries, introducing 2 keywords
per predicate.
NB: Res[C] is always finite because C has only
unary predicates.
See [Hinrichs2008c] for more details.
COMPULOG Summer School 2008
42
Existential Entailment
Two possible sources of inconsistency:
• C itself
• C together with cell assignment A
Because ent_drive is built only from
constraints that include drive, the
Datalog queries implement Existential
Entailment.
COMPULOG Summer School 2008
43
Message
Build Applications
and
Embrace Conflicts
COMPULOG Summer School 2008
44
[Hinrichs2008a] T. Hinrichs. Collaborative Programming.
Workshop on Practical Aspects of Automated Reasoning,
2008. http://people.cs.uchicago.edu/~thinrich/papers/
hinrichs2008collaborative.pdf
[Hinrichs2008b] T. Hinrichs, et. al. Design and Implementation
of a Flow-based Security Language. Unpublished.
Available upon request.
[Kassoff2007] 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
[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
[Hinrichs2008c] T. Hinrichs and M. Genesereth. Injecting the
How into the What. KR 2008.
http://people.cs.uchicago.edu/~thinrich/papers/hinrichs2008i
njecting.pdf
COMPULOG Summer School 2008
45
Questions
COMPULOG Summer School 2008
46
Descargar

Collaborative Programming: Logic and Automated …