'$

Static Detection of Security Flaws in Object-Oriented Databases
Keishi Tajima
Kyoto Univ.

&Univ. of Tokyo† currently at Kobe University‡ supported by IISF&%

'$Background (1/4)
Database Access
User access to a database is either:• actions to get information from the database, or• actions to give information to the database.
They are usually represented as read and write operations.
readuserDBwrite&1%

'$

Background (2/4)
Need for Control in Abstract Operation Level• To give only partial information on some data.
• To allow update of some data only in speciﬁc procedure.
⇓Function-granularity Access Control• “One can read this only through this function”• “One can write this only through this function”
&2%

'$

Background (3/4)
Example 1: allowing read operation only through a speciﬁc function
A job of checking budgets of stockbrokers:function checkBudget(broker) =>=(r budget(broker), ∗(10, r salary(broker)))

&

3%

'$

Background (4/4)
Example 2: allowing write operation only through a speciﬁc function
A job of updating salaries of stockbrokers:function updateSalary(broker) =w salary(broker,calcSalary(r budget(broker), r profit(broker)))

&4%

'$

Problem
Security ﬂaws in function-granularity access control“Is that function eﬀectively hiding read/write operations inside it?”In Ex. 1:• If one can know budgets of brokers, he can partially infer their salaries.
• If one can change budgets of brokers, he can totally infer their salaries.
In Ex. 2:• If one can alter budgets of brokers, he can alter their salaries.

&5%

'$Goal of This Research• To establish a foundation of security analysis for function-granularity
access control.
• To develop a mechanism of static detection of security ﬂaws.

&6%

'$Key Concepts
Inferability and Alterability
Generalization of read/write capability:• inferability — ability to infer the result of a read operation• alterability — ability to alter the value written in a write operation
They are eﬀectively equivalent to being able
to read/write directly.

&7%

'$

Inferability and Alterability (1/3)
Further generalization:• inferability — ability to infer the returned valueof a function invocation• alterability — ability to alter the value of an argumentof a function invocation
They correspond to two kind of capability indatabase access through functions.
returned value
userfDBarguments
&8%

'$

Inferability and Alterability (2/3)
Classiﬁcation of inrerability / alterability• total inferability — ability to infer an exact value• partial inferability — ability to infer some subsets• total alterability — ability to alter it to any value in the domain• partial alterability — ability to alter only within some subdomain&9%

'$

Inferability and Alterability (3/3)
Causality between capability
base cases• inferability:
1. constants,
2. returned values of functions directly invoked by the user, or
3. arguments of functions directly invoked by the user.
• alterability — arguments of functions directly invoked by the usercausality• dependency between arguments and returned values of basic functions• persistence• alterability can cause inferability (e.g.: >, div, mod)
&10%

'$

Static Detection of Security Flaws
Basic Strategy
1. Capability List — a set of functions one can invoke.
2. Security Requirement — a set of capability that he should not achieve.
3. We analyze programs of functions and determine whether each user
can achieve speciﬁed capability.

&11%

'$

User Access through Functions
Syntax of the function deﬁnition language
e ::= c | x | fb(e, . . . , e) | fa(e, . . . , e) | r att(e) | w att(e, e)
Query language
capability list = {r name, r age, profile, . . . }select r name(p), profile(p) from p ∈ Person
where r age(p) > 20&12%

'$Description of Security Requirements
An example of description(u, r salary(employee : pa) : ti)u should not be able to invoke r salary(employee) in the context
where he can achieve• partial alterability on the argument employee, and• total inferability on the returned value.

&13%

'$

Formal Deﬁnitions (1/2)

alterability on ai of f (. . . , ai, . . .)∃hf1, . . . , fni
including indirect invocation of f , andone can alter the value of ai by changing the arguments of f1, . . . , fn.
inferability on f∃hf1(v11, . . . , v1m) → r1, . . . , fn(vn1 , . . . , vnm) → rni
including indirect invocation of f , andan inference system I can infer the returned value of it.

&14%

'$

Formal Deﬁnitions (2/2)
Inference system I
I models users’ inference on values of expressions in program codes.
term ::= [he1, . . . , eni ∈ S] | [e1 = e2]
Axioms and inference rules (part)→ [hci ∈ {c}]jj
→ [hai i ∈ {vi }]→ [he1, . . . , en, fb(e1, . . . , en)i ∈ {hv1, . . . , vn, ri | fb(v1, . . . , vn) = r}][hei, ej i ∈ S1], [hej , ek i ∈ S2]→ [hei, ej , ek i ∈ {hvi, vj , vk i | hvi, vj i ∈ S1, hvj , vk i ∈ S2}]

&15%

'$

Program Code Analysis (1/3)
Overview
1. We developed an inference system J which syntactically analyzes
program codes and determine what capability users can achieve.
2. We compute a closure set of all terms deducable by J .
3. If capability speciﬁed in security requirements are included in theclosure set, we determine that there is a security ﬂaw.

&16%

'$

Program Code Analysis (2/3)
Inference system J
term ::= ta[e] | pa[e] | ti[e] | pi[e] | =[e1, e2] | . . .
Inference rule of J (part)→ ti[c]→ ta[x] (argument of outermost function)ta[e3] → ta[r att(e2)] (if there exists w att(e1, e3))
Rules for basic functions are deﬁned according to their semantics.
e.g.: rules for >= (part)pi[e1], pi[e2]→ ti[ >= (e1, e2)]ti[e1], pa[e1], ti[ >= (e1, e2)] → ti[e2]
&17%

'$

Program Code Analysis (3/3)
An example of analysis
function checkBudget(broker) =>=(r budget(broker), ∗(10, r salary(broker)))capability list of u = {checkBudget, w budget}
security requirement = (u, r salary(broker):ti)..
=[v, r budget(broker)], ti[v] → ti[r budget(broker)]=[o, broker], pa[v] → pa[r budget(broker)]→ ti[>=(. . . )]ti[r budget(broker)], pa[r budget(broker)], ti[>=(. . . )]→ ti[∗(10, r salary(broker))]→ ti[10]ti[10], ti[∗(10, r salary(broker))] → ti[r salary(broker)]&18%

'$Conclusion• We propose the concepts of inferability and alterability.
• We develop a method to statically determine whether given security
requirements are satisﬁed or not.
Future work
• To include more complex program structures (conditional branch,recursion)• More accurate analysis. Dynamic checking.

&19%