CS18000 Programming I 10 18 2010 CS52600 Information Security Midterm Review 18 October 2010 Prof Chris Clifton Course Outline 1 Introduction Role of security Types of security Definitions 2 Access Control Matrix model 3 Protection Models 4 Policy Risk Analysis Policy Formation Role of audit and control 5 Formal policy models 6 Information Flow 7 Authentication and Identity 8 Forensics Midterm 10 20 10 System Design principles TCB and security kernel construction Verification Certification issues 11 Network Security Distributed cooperation and commit Distributed authentication issues Routing flooding spamming Firewalls 12 Audit Mechanisms 13 Malicious Code Viruses Worms etc 14 Vulnerability Analysis 15 Physical threats operational security Legal and Societal Issues Final Exam 2 2010 Chris Clifton 1 CS18000 Programming I 10 18 2010 Basic Components Confidentiality Keeping data and resources hidden Integrity Data integrity integrity Origin integrity authentication Availability Enabling access to data and resources 3 Policies and Mechanisms Policy says what is and is not allowed This defines security for the site system etc Policy definition Informal Formal Mechanisms enforce policies Composition of policies If policies conflict discrepancies may create security vulnerabilities 4 2010 Chris Clifton 2 CS18000 Programming I 10 18 2010 Access Control State Status of the system Protection state subset that deals with protection Access Control Matrix Describes protection state Formally Objects O Subjects S Matrix A S O Tuple S O A defines protection states of system 5 Access Control Matrix Boolean Evaluation Example Internal Public Local CR State University Long Distance International R R R CR R R R T Student Staff Account CR CR T T CR CR Transfer T T CR CR CR CR CR T T T T T 6 2010 Chris Clifton 3 CS18000 Programming I 10 18 2010 Protection State Transitions State Xi Si Oi Ai Transitions i Single transition Xi i 1 Xi 1 Series of transitions X Y Access control matrix may change Change command c associated with transition Xi ci 1 pi 1 pi 1 Xi 1 Change command c associated with transition 7 Primitive Commands Create Object o Adds o to objects with no access S S O O o x S a x o x S y O a x y a x y Create Subject s Adds s to objects subjects sets relevant access control to Enter r into a s o Delete r from a s o Destroy subject s destroy object o 8 2010 Chris Clifton 4 CS18000 Programming I 10 18 2010 Formally Given initial state X0 S0 O0 A0 Set of primitive commands c Can we reach a state Xn where s o such that An s o includes a right r not in A0 s o If so the system is not safe 9 Decidability Result Harrison Ruzzo Ullman Given a system where each command consists of a single primitive command There exists an algorithm that will determine if a protection system with initial state X0 is safe with respect to right r Proof determine minimum commands k to leak Delete destroy Can t leak or be detected Create enter new subjects objects equal so treat all new subjects as one If n rights leak possible must be able to leak in n S0 1 O0 1 1 commands Enumerate all possible to decide 10 2010 Chris Clifton 5 CS18000 Programming I 10 18 2010 Other Results most from the same authors Set of unsafe systems recursively enumerable Without create primitive safety in P SPACE Like halting problem reduction but no unlimited tape Without delete destroy still undecidable Decidable if at most one condition allowed per command Still holds if delete allowed 11 Take Grant Protection Model System is directed graph Subject Both Object labeled edge rights Take rule if t can add transitive edge Grant rule if g can add grant edge between recipients Create Remove rules 12 2010 Chris Clifton 6 CS18000 Programming I 10 18 2010 Take Grant Protection Model Sharing Given G0 can vertex x obtain rights over y Can share x y G0 iff G0 Gn using the above rules and edge from x to y in Gn tg path v0 vn where t or g edge between any vi vi 1 Vertices tg connected if tg path between them Theorem Any two subjects with tg path of length 1 can share rights 13 Theorem Can share x y G0 Can share x y G0 iff there is an edge from x to y in G0 or if a vertex s G0 with an s to y edge a subject x such that x x or x initially spans to x a subject s such that s s or s terminally spans to s and islands I1 In such that x I1 s In and there is a bridge from Ij to Ij 1 Proof If x grants to x s takes from s otherwise as with subjects Only if as before plus object can t give receive a right unless someone can take grant it Corollary There is an O V E algorithm to test can share 15 2010 Chris Clifton 7 CS18000 Programming I 10 18 2010 Theorem When Theft Possible Can steal x y G0 iff there is no edge from x to y in G0 and G1 Gn 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 easy build path Assume can steal No edge from definition Can share x y G0 from definition from x to y in Gn s exists from can share and Monday s theorem Can share t x s G0 s can t grant definition someone else must get from s show that this can only be accomplished with take rule 16 Schematic Protection Model Key idea Protection Type Label that determines how control rights affect an entity Take Grant subject and object are different protection types Unix file system File Directory Ticket Describes a set of rights Entity has set dom X of tickets Y z describing X s rights z over entities Y Inert right vs Control right Inert right doesn t affect protection state 17 2010 Chris Clifton 8 CS18000 Programming I 10 18 2010 Transferring Rights Link predicate linki X Y conjunction or disjunction of X z dom X X z Y z dom X Y z true dom Y dom Y Determines if X and Y connected to transfer right Example link X Y Y g dom X X t dom Y Filter function conditions on transfer Copy X r c from Y to Z allowed iff i such that X rc dom Y linki Y Z X r c filteri Y Z 18 Safety Analysis in SPM Idea derive maximal state where changes don t affect analysis Similar to determining max flow Theorems A maximal state exists for every system If parent gives child only rights parent has conditions somewhat more complex can easily derive maximal state 19 2010 Chris Clifton 9 CS18000 Programming I 10 18 2010 Typed Access Matrix Model Finite set T of types …