IS 2150 / TEL 2810 Introduction to SecurityObjectivesSlide 3Security PolicyConfidentiality PolicyIntegrity PolicyTrustTrust in Formal VerificationSecurity ModelSecurity policiesAccess ControlSlide 12Slide 13Slide 14Bell-LaPadula: Basics“No Read Up”“No Write Down”ExampleAccess RulesCategoriesLattice of categoriesSlide 22Communication across levelRead & writeProblem: No write-downPrinciple of TranquilitySlide 27Types of TranquilitySlide 29DG/UX LabelsDG/UXSlide 32Slide 33Slide 34Biba’s Integrity Policy ModelBiba’s modelLow-water-markSummary1IS 2150 / TEL 2810Introduction to SecurityJames JoshiAssociate Professor, SISLecture 5September 20, 2011Security PoliciesConfidentiality Policies2ObjectivesUnderstanding/defining security policy and nature of trustOverview of different policy modelsDefine/Understand existing Bell-LaPadula model of confidentialityhow lattice helps?Understand the Biba integrity model3Security Policies4Security PolicyDefines what it means for a system to be secureFormally: Partitions a system intoSet of secure (authorized) statesSet of non-secure (unauthorized) statesSecure system is one that Starts in authorized stateCannot enter unauthorized state5Confidentiality PolicyAlso known as information flowTransfer of rightsTransfer of information without transfer of rightsTemporal contextModel often depends on trustParts of system where information could flowTrusted entity must participate to enable flowHighly developed in Military/Government6Integrity PolicyDefines how information can be alteredEntities allowed to alter dataConditions under which data can be alteredLimits to change of dataExamples:Purchase over $1000 requires signatureCheck over $10,000 must be approved by one person and cashed by anotherSeparation of duties : for preventing fraudHighly developed in commercial world7TrustTheories and mechanisms rest on some trust assumptionsAdministrator installs patch1. Trusts patch came from vendor, not tampered with in transit2. Trusts vendor tested patch thoroughly3. Trusts vendor’s test environment corresponds to local environment4. Trusts patch is installed correctly8Trust in Formal VerificationFormal verification provides a formal mathematical proof that given input i, program P produces output o as specifiedSuppose a security-related program S formally verified to work with operating system OWhat are the assumptions during its installation?9Security ModelA model that represents a particular policy or set of policiesAbstracts details relevant to analysisFocus on specific characteristics of policiesE.g., Multilevel security focuses on information flow control10Security policiesMilitary security policyFocuses on confidentialityCommercial security policyPrimarily IntegrityTransaction-orientedBegin in consistent state“Consistent” defined by specificationPerform series of actions (transaction)Actions cannot be interruptedIf actions complete, system in consistent stateIf actions do not complete, system reverts to beginning (consistent) state11Access ControlDiscretionary Access Control (DAC)Owner determines access rightsTypically identity-based access control: Owner specifies other users who have accessMandatory Access Control (MAC)Rules specify granting of accessAlso called rule-based access control12Access ControlOriginator Controlled Access Control (ORCON)Originator controls accessOriginator need not be owner!Role Based Access Control (RBAC)Identity governed by role user assumes13Confidentiality Policies14Confidentiality PolicyAlso known as information flow policyIntegrity is secondary objectiveEg. Military mission “date”Bell-LaPadula Model Formally models military requirementsInformation has sensitivity levels or classification Subjects have clearanceSubjects with clearance are allowed accessMulti-level access control or mandatory access control15Bell-LaPadula: BasicsMandatory access control Entities are assigned security levelsSubject has security clearance L(s) = lsObject has security classification L(o) = loSimplest case: Security levels are arranged in a linear order li < li+1ExampleTop secret > Secret > Confidential >Unclassified16“No Read Up”Information is allowed to flow up, not downSimple security property: s can read o if and only iflo ≤ ls ands has discretionary read access to o-Combines mandatory (security levels) and discretionary (permission required)-Prevents subjects from reading objects at higher levels (No Read Up rule)17“No Write Down”Information is allowed to flow up, not down*property s can write o if and only ifls ≤ lo ands has write access to o-Combines mandatory (security levels) and discretionary (permission required)-Prevents subjects from writing to objects at lower levels (No Write Down rule)18Examplesecurity level subject objectTop Secret Tamara Personnel FilesSecret Samuel E-Mail FilesConfidential Claire Activity LogsUnclassified Ulaley Telephone Lists•Tamara can read which objects? And write?•Claire cannot read which objects? And write?•Ulaley can read which objects? And write?19Access RulesSecure system: One in which both the properties holdTheorem: Let Σ be a system with secure initial state σ0, T be a set of state transformationsIf every element of T follows rules, every state σi secureProof - induction20CategoriesTotal order of classifications not flexible enoughAlice cleared for missiles; Bob cleared for warheads; Both cleared for targetsSolution: CategoriesUse set of compartments (from power set of compartments)Enforce “need to know” principleSecurity levels (security level, category set)(Top Secret, {Nuc, Eur, Asi})(Top Secret, {Nuc, Asi})21Lattice of categoriesCombining with clearance:(L,C) dominates (L’,C’) L’ ≤ L and C’ CInduces lattice of security levelsExamples of levels(Top Secret, {Nuc,Asi}) dom (Secret, {Nuc}) ?(Secret, {Nuc, Eur}) dom (Topsecret, {Nuc,Eur}) ?(Top Secret, {Nuc}) dom (Confidential, {Eur}) ?Exercise: Hesse diagram for: Security levels: TS, S, C Compartments US, EU; Exercise: Hesse diagram for: Security levels: TS, S, C Compartments US, EU; Exercise: Hesse diagram for: compartments: NUC, US, EU; Exercise: Hesse diagram
View Full Document