463.8 Information FlowOverviewRequiredExample 1NoninterferenceExample 2Model of NoninterferenceState AutomatonCapability SystemTransition FunctionProjectionSlide 12Security PoliciesSlide 14Example 2 MLSMLS ContinuedExample 4 IsolationExample 5 Channel ControlExample 6 Information FlowExample 3 Security OfficerEntropy and Information FlowEntropySlide 23Slide 24Slide 25Example 3Implicit Flow of InformationCompiler-Based MechanismsExampleDeclarationsAssignment StatementsCompound StatementsIterative StatementsConditional StatementsSlide 35Input ParametersOutput ParametersProcedure CallsSlide 39Array ElementsOther ConstructsResource SharingConfinement ProblemTransitivityIsolationMechanisms for IsolationMemory protectionchrootSlide 49SandboxesUser-space SandboxesKernel-basedHybridFiltering [Janus]Filtering system calls:Delegation [Ostia]DelegationSandboxing policiesVirtual machinesApproachesProtection RingsEmulationSpecial KernelSlide 64Sandboxes vs. VMMsUnanticipated ChannelsTwo Types of ChannelsExample Timing ChannelNoiseDetecting Covert ChannelsShared Resource MatrixExamplesAnalysis using SRMSRM applicationsInformation FlowKernel AnalysisChannels Found in XenixCovert Flow TreesExample TreePossible Covert ChannelsOther IssuesSummary463.8 Information FlowUIUC CS463 Computer Security2Overview•Motivation•Non-interference model•Information flow and language analysis•Confinement and covert channels3Required•Reading–Chapter 8 up to the beginning of 8.2.1–Gougen Meseguer 82–Chapter 16 sections 16.1 and 16.3–Chapter 17–Garfinkel Pfaff Rosenblum 034•Downloadable financial planner:Example 1NetworkDiskAccountingSoftware Access control insufficient Encryption necessary, but also insufficient5NoninterferenceAccountingSoftware Private data does not interfere with network communication Baseline confidentiality policyNetworkDisk6Example 2•Smart card for financial transactions–Card contains sensitive financial information used to make a transaction–Used in the terminal of a merchant–Card is tamper-resistant, protects card secrets from both the merchant and card holder–Java cards provide limited card-based computation–Must split the computation between the card, the terminal, and network connections7Model of Noninterference•Represent noninterference as a relation between groups of users and commands•Users in group G do not interfere with those in group G’ if the state seen by G’ is not affected by the commands executed by members of GGoguen Meseguer 828State Automaton•U – Users •S – States•C – Commands•Out – Outputs•do : S £ U £ C ! S – state transition function•out : S £ U ! Out – output function•s0 – initial machine state9Capability System•U, S, Out – users, states, commands, and outputs as before (in a state machine)•SC – State commands•Capt – Capability tables•CC – Capability commands•out : S £ Capt £ U ! Out•do : S £ Capt £ U £ SC ! S•cdo : Capt £ U £ CC ! Capt – Capability selection function•s0 2 S and t0 2 Capt – Initial state and capability tables10Transition Function•C = SC ] CC - Commands•csdo : S £ Capt £ U £ C ! S £ Capt–csdo(s,t,u,c) = (do(s,t,u,c),t) if c 2 SC–csdo(s,t,u,c) = (s,cdo(s,t,u,c)) if c 2 CC•csdo* : S £ Capt £ (U £ C)* ! S £ Capt–csdo*(s,t,nil) = (s,t)–csdo*(s,t,w.(u,c)) = csdo(csdo*(s,t,w),u,c)•[[w]] = csdo*(s0,t0,w)•[[w]]u = out([[w]],u)11Projection•Let G µ U and A µ C and w 2 (U £ C)*•PG(w) = subset of w obtained by eliminating pairs (u,c) where u 2 G•PA(w) = subset of w obtained by eliminating pairs (u,c) where c 2 A•PG,A(w) = subset of w obtained by eliminating pairs (u,c) where u 2 G and c 2 A12Noninterference•M state machine and G, G’ µ U and A µ C•G :| G’ iff 8 w 2 (U £ C)*. 8 u 2 G’. [[w]]u = [[pG(w)]]u•A :| G iff 8 w 2 (U £ C)*. 8 u 2 G. [[w]]u = [[pA(w)]]u•A,G :| G’ iff 8 w 2 (U £ C)*. 8 u 2 G’. [[w]]u = [[pA,G(w)]]u13Security Policies•Noninterference assertions have the formsG :| G’A :| GA,G :| G’•A security policy is a set of noninterference assertions14Example 1•A :| {u}•The commands in A do not interfere with the state of user u15Example 2 MLS•Level : U ! L - assignment of security levels in L•Above(l) = { u 2 U | l v Level(u)}•Below(l) = { u 2 U | Level(u) v l}•M is multi-level secure with respect to L if, for all l @ l’ in L, Above(l’) :| Below(l)SecretUnclassifiedTop SecretLevels L v16MLS Continued•G is invisible if G :| Gc where Gc is the complement of G in U•Proposition 1: If M,L is multi-level secure, then Above(l) is invisible for every l 2 L.17Example 4 Isolation•A group of users G is isolated if: G :| Gc and Gc :| G.•A system is completely isolated if every user in U is isolated.18Example 5 Channel Control•View a channel as a set of commands A•We can assert that groups of users G and G’ can only communicate through channel A with the following two noninterference assertions:–Ac,G :| G’ and–Ac,G’ :| G19Example 6 Information Flowu u’u2u1A1AA2u’,u1,u2 :| uu1,u2 :| u’u1 :| u2u2 :| u1Ac,u :| {u’,u1,u2}A1c,u’ :| {u1}A2c,u’ :| {u2}20Example 3 Security Officer•Let A be the set of commands that can change the security policy•seco 2 U is the only individual permitted to use these commands to make changes•This is expressed by the following policy: A,{seco}c :| U21Entropy and Information Flow•Idea: info flows from x to y as a result of a sequence of commands c if you can deduce information about x before c from the value in y after c•Formalized using information theory22Entropy•Entropy: measure of uncertainty in a random variable–H(X) = -i p(xi) log(p(xi))–constant: H(c) = 0–uniform distribution: H(Un) = log(n)•Conditional entropy: how much uncertainty left about X knowing Y–H(X | Y) = -j p(yj) i p(xi | yj) log(p(xi | yj))–H(X | Y) = j p(yj) H(X | Y=yj) –H(X | Y) = H(X) if X,Y are independent23Entropy and Information Flow•Definitions:–Sequence of commands c–xs, ys are (distributions) of values of x,y before commands c–xt, yt are values after c•Commands c leak information about x into y if:–H(xs | yt) < H(xs | ys)–If no y at time s, then H(xs | yt) < H(xs)24Example 1•y := x–If we learn y, then we know x–H(xs|yt=y) = 0 for all y, so H(xs|yt) = 0–Information flow exists if xs not a (known) constant25Example 2•Destroyed information1: r1 := x2: …3: r1 := r1
View Full Document
Unlocking...