September 16, 2004Theorem: Can_share(α,x,y,G0) (for subjects)What about objects? Initial, terminal spansTheorem: Can_share(α,x,y,G0)Slide 5Slide 6ExampleTake-Grant Model: Sharing through a Trusted EntityTheft in Take-Grant ModelA witness to theftTheorem: When Theft PossibleSlide 12ConspiracySlide 14Slide 15TheoremsBack to HRU: Fundamental questionsTuring Machine & halting problemTuring MachineSlide 20Slide 21General Safety ProblemMappingCommand Mapping (Left move)Mapping (Left Move)Mapping (Initial)Command Mapping (Right move)Slide 28Command Mapping (Rightmost move)Slide 30Rest of ProofOther theoremsSlide 33Schematic Protection ModelSlide 35Transferring RightsFilter FunctionSCM Example 1SPM Example 1SPM Example2DemandCreate OperationCreate operation Distinct TypesNon-Distinct TypesExamplesSafety Analysis in SPMTyped Access Matrix ModelHRU vs. SPMComparing ModelsExtended Schematic Protection ModelCourtesy of Professors Chris Clifton & Matt BishopINFSCI 2935: Introduction of Computer Security1September 16, 2004September 16, 2004Introduction to Introduction to Computer SecurityComputer SecurityLecture 3Lecture 3Take Grant Model (Cont)Take Grant Model (Cont)HRUHRUSchematic Protection ModelSchematic Protection ModelINFSCI 2935: Introduction to Computer Security 2Theorem: Can_share(Theorem: Can_share(αα,,xx,,yy,,GG00))(for subjects)(for subjects)Subject_can_shareSubject_can_share((αα, , xx, , yy,,GG00) is true iff ) is true iff xx and and yy are are subjects andsubjects andthere is an α edge from x to y in G0 OR if: a subject s  G0 with an s-s-to-yy α edge, and islands I1, …, In such that xx  I1, s  In, and there is a bridge from Ij to Ij+1xsααααyII11II22IInnINFSCI 2935: Introduction to Computer Security 3What about objects?What about objects?Initial, terminal spansInitial, terminal spansxx initially spansinitially spans to to yy if if xx is a subject and is a subject and there is a there is a tgtg-path associated with word -path associated with word {{tt→→*g*g→→} between them} between themxx can grant a right to yyxx terminally spansterminally spans to to yy if if xx is a subject and is a subject and there is a there is a tgtg-path associated with word -path associated with word {{tt→→**} between them} between themxx can take a right from yyINFSCI 2935: Introduction to Computer Security 4Theorem: Can_share(Theorem: Can_share(αα,,xx,,yy,,GG00))Can_share(Can_share(αα,,xx, , yy,,GG00) iff there is an ) iff there is an αα edge from edge from xx to to yy in in GG00 or if: or if: a vertex ss  G0 with an ss to yy α edge, a subject x’x’ such that x’=xx’=x or x’x’ initially spans to xx, a subject s’s’ such that s’=ss’=s or s’s’ terminally spans to ss, and islands II1, …, IIn such that x’x’  II1, s’s’  IIn, and there is a bridge from Ij to Ij+1x’s’ααααyII11II22IInnsxx’x’ can grant a right to can grant a right to xxs’s’ can take a right from can take a right from ssαINFSCI 2935: Introduction to Computer Security 5Theorem: Can_share(Theorem: Can_share(αα,,xx,,yy,,GG00))Corollary: There is an Corollary: There is an OO(|(|VV|+||+|EE|) algorithm to test |) algorithm to test can_share: can_share: Decidable in linear time!!Decidable in linear time!!Theorem:Theorem: Let G0 contain exactly one vertex and no edges, R a set of rights. G0 ├* G iff G is a finite directed acyclic graph, with edges labeled from R, and at least one subject with no incoming edge.Only if part: v is initial subject and G0 ├* G;No rule allows the deletion of a vertexNo rule allows an incoming edge to be added to a vertex without any incoming edges. Hence, as v has no incoming edges, it cannot be assigned anyINFSCI 2935: Introduction to Computer Security 6Theorem: Can_share(Theorem: Can_share(αα,,xx,,yy,,GG00))If part : G meets the requirementAssume v is the vertex with no incoming edge and apply rules1. Perform “v creates (α  {g} to) new xi” for all 2<=i <= n, and α is union of all labels on the incoming edges going into xi in G2. For all pairs x, y with x α over y in G, perform “v grants (α to y) to x”3. If β is the set of rights x has over y in G, perform “v removes (α  {g} - β) to y”INFSCI 2935: Introduction to Computer Security 7ExampleExampleINFSCI 2935: Introduction to Computer Security 8Take-Grant Model: Take-Grant Model: Sharing through a Trusted EntitySharing through a Trusted EntityLet Let pp and and qq be two processes be two processes Let Let bb be a buffer that they share to communicate be a buffer that they share to communicateLet Let ss be third party (e.g. operating system) that be third party (e.g. operating system) that controls controls bbggqbsrwrwrwurwvrwggqsurwvrwWitness•S creates ({r, w}, to new object) b•S grants ({r, w}, b) to p•S grants ({r, w}, b) to qINFSCI 2935: Introduction to Computer Security 9Theft in Take-Grant ModelTheft in Take-Grant ModelCan_stealCan_steal((αα,,xx,,yy,,GG00) is true if there is no ) is true if there is no αα edge edge from from xx to to yy in in GG00 and and  sequence sequence GG11, …, , …, GGnn s. t.: s. t.: α edge from x to y in Gn,, rules ρ1,…, ρn that take Gi-1├ ρi Gi , and v,w  Gi, 1≤i<n, if  α edge from v to y in G0 then ρi is not “v grants (α to y) to w”-Disallows owners of α rights to y from transferring those rights-Does not disallow them to transfer other rights-This models a Trojan horseINFSCI 2935: Introduction to Computer Security 10A witness to theftA witness to theftu grants (t to v) to su grants (t to v) to ss takes (t to u) from vs takes (t to u) from vs takes (s takes (αα to w) from u to w) from ugswttααuvINFSCI 2935: Introduction to Computer Security 11Theorem:Theorem:When Theft PossibleWhen Theft PossibleCan_steal(Can_steal(αα,,xx,,yy,,GG00) iff there is no ) iff there is no αα edge from edge from xx to to yy in in GG00 and and  GG11, …, , …, GGnn s. t.: s. t.:There is no α edge from x to y in G0 , subject x’ such that x’=x or x’ initially spans to x, and s with α edge to y in G0 and can_share(t,x,s,G0)Proof:Proof:: Assume the three conditions holdx can get t right over s (x is a subject) and then take α right over y from sx’ creates a surrogate to pass α to x