Models & PoliciesSecurity PoliciesWhy Security Models?AgendaNotation for SetsState Machine Models (Automata)Basic Security TheoremsBell-LaPadula Model (BLP)What has to be modeled?Slide 10BLP PoliciesSlide 12Star PropertyNo Write-DownDiscretionary BLP PolicyBasic Security TheoremTranquilityCovert ChannelsAspects of BLPLimitations of BLPHarrison-Ruzo-Ullman ModelPrimitive Operations in HRUExamples‘Leaking’ of Rights in HRUSafety Properties of HRUThe 3rd Design Principle.Chinese Wall ModelChinese Wall Model - PoliciesSlide 29Biba ModelBiba: static integrity levelsBiba: dynamic integrity levelsBiba policies for invocationClark-Wilson ModelClark-Wilson: Access ControlClark-Wilson: Certification RulesClark-Wilson: Enforcement RulesInformation Flow ModelsNon-interference modelsExercisesFurther readingMT5104 - Computer Security - Models & Policies1Models & Policies•The previous lecture has presented a choice of access control structures.•Access control structures are there to encode security policies.•A security policy captures the security requirements of an enterprise, or describes the steps that have to be taken to achieve security.•A security model is a formal description of a security policy.MT5104 - Computer Security - Models & Policies2Security Policies•Organisational security policy: Laws, rules, and practices that regulate how an organisation manages and protects resources to achieve its security policy objectives. (A topic of IS1)•Automated security policy: Restrictions and properties that specify how a computing system prevents violations of the organisational security policy. (A topic for this course) D. F. Sterne: On the Buzzword ‘Security Policy’MT5104 - Computer Security - Models & Policies3Why Security Models?•They are used today in high assurance security evaluations (smart cards are currently a fruitful area of application)•They are important historic milestones in computer security (e.g. Bell-LaPadula)•They demonstrate some of the fundamental design decisions in a precise settingMT5104 - Computer Security - Models & Policies4Agenda•The Bell-LaPadula (BLP) model•Changing access rights: Harrison-Ruzo-Ullman, Chinese Wall•Integrity: Biba, Clark-Wilson•Perfection: information flow and non-interference modelsMT5104 - Computer Security - Models & Policies5Notation for Sets•a  A: a is an element of set A•A  B: the Cartesian product of two sets A and B; the elements of A  B are pairs (a,b); the elements of S  O  A would be tuples (s,o,a).•AB: the set of functions from B to A; the elements of AB are functions f: B  A .•PP(A): the power set of A; the elements of PP(A) are subsets of A.MT5104 - Computer Security - Models & Policies6State Machine Models (Automata)•Abstract models that record relevant features, like the security of a computer system, in their state.•States change at discrete points in time, e.g. triggered by a clock or an input event.•State machine models have numerous applications in computer science: processor design, programming languages, or security. Examples: –Switch: two states, ‘on’ and ‘off’–Ticket machine: inputs: ticket requests, coins, state: ticket requested and money to be paid, output: ticket, change–Microprocessors: state: register contents, inputs: machine instructionsMT5104 - Computer Security - Models & Policies7Basic Security Theorems•To design a secure system with the help of state machine models,–define its state set so that it captures ‘security’.–check that all state transitions starting in a ‘secure’ state yield a ‘secure’ state.–check that the initial state of the system is ‘secure’.•Security is then preserved by all state transitions. The system will always be ‘secure’.•This Basic Security Theorem has been derived without any definition of ‘security’!MT5104 - Computer Security - Models & Policies8Bell-LaPadula Model (BLP)•BLP formalizes a confidentiality policy forbidding information flows from ‘high’ security levels down to ‘low’ security level. •BLP only considers information flows that occur when a subject observes or alters an object. •BLP is a state machine model.•Access permissions are defined through an access control matrix and through a partial ordering of security levels.MT5104 - Computer Security - Models & Policies9What has to be modeled?1All current access operations:–an access operation is described by a triple (s,o,a), s  S(ubjects), o  O(bjects), a  A(ccess_Operations)–The set of all current access operations is an element of PP(S  O  A).–We use B as shorthand for PP(S  O  A). –We use b to denote a set of current access operations.2The current permissions as defined by the access control matrix M–MM is the set of access control matrices.MT5104 - Computer Security - Models & Policies10What has to be modeled?3The current assignment of security levels:–maximal security level: fS: S  L (L … labels)–current security level: fC: S  L –classification: fo: O  L•The security level of a user is the user’s clearance.•The current security level allows subjects to be down-graded temporarily (more later).• F  LS  LS  LO is the set of security level assignments.• f = (fS, fC, fO) denotes an element of F.•The state set of BLP: V = B MM  F•A state is denoted by (b,M,f)MT5104 - Computer Security - Models & Policies11BLP Policies•Forbid information flows from ‘high’ security levels to ‘low’ security levels that occur directly through access operations.•Simple Security Property (ss-property)•Information flow is still possible.–For example, a low subject creates a high Trojan horse program that reads a high document and copies its contents to a low file.–This constitutes an improper ‘declassification’ of the document.No read-up: fS(s)  fO(o) if access is in observe modeMT5104 - Computer Security - Models & Policies12Trojan horse copyreadcreatereadMT5104 - Computer Security - Models & Policies13Star Property - Property (star property)•The very first version of BLP did not consider the  - property.•The ss- property and  - property are called the mandatory BLP policies.No write-down: fC(s)  fO(o) if access is in alter mode; also, if subject s has access to an object o in alter mode, then fO(o’)  fO(o) for all objects o’ accessed by s in observe mode.MT5104 - Computer Security -