Security 2
Courses classes are Thursday form 9h45 to 11h15 online (the link is available on the moodle)
Online resurces
Evaluation:
- Attack trees presentations (30%)
- Evaluation on information flows (20%)
- Homeworks on Proverif (50%)
Course schedule
Week 1, 18 February: Overview
- What does security mean?
- Secure systems need good design:
- Evaluate potential risks
- Risk assessment and cost models
- Risk prevention/incentives
Suggested reading:
What Is Security Engineering
Week 2, 25 February: Attack Trees
Risk management
- security risk = possible damage
- Identify risks
- Reduce risks
- Keep other risks under control during this operation
- Repete...
- Glossary:
- Asset = something of Evaluate
- Vulnerability = a weakeness of the system which can be exploited to harm the asset
- Threat = exploitation of a vulnerability by a threat agent
- Risk = quantification of a threat
- Control = measure to reduce a risk
- How to do risk analysis?
- identify context
- identify assets
- assess risks
- treat risks
- Classify threats (impact vs likelihood)
- Possible controls:
- acceptance
- avoidance
- transfer
- possible treatments: accept risks, reduce impact, reduce likelihood
- Controls have costs or may not be 100% effective
Attack Trees
- free lunch tree example
- threat Trees
- fault Trees
- Tree nodes are AND, OR, SAND, KofN ...
Attack Trees semantics
- Why semantics? (distinguis equivalent trees)
- propositional/set semantics
- multiset semantics
Computing Attributes
- possible attribute domains: cost, probability, possibility, time, ...
- possibility = boolean circuits
- cost = OR -> minimum of children values / AND -> sum of children values
- probability = OR -> probability of union / AND -> probability of intersection
Suggested reading:
Week 3, 4 March: free meal case study
- Attack trees Evaluation:
- case analysis of the free-meal attack tree
- focus on nodes refinements types
Week 4, 11 March: Students presentations
During this class students will give short presentations of some attack trees they produce.
Each presentation must include
Suggested reading
Week 5, 15 March (Matteo): Control Access Models
- Access control policies: determine who has access to what (and when) in a system
- Discretionary Access Control (DAC): users decide
- each resource has an owner
- each owner decides who has access to a resource
- Troyan horse information leak: Alice owns a file Info which cannot be accessed by Bob. A Troyan-horse (executed as Alice) may read Info and copy on a file Stole owned by Bob, allowing Bob to read the content of Info.
- Mandatory Access Control (MAC): system decides
- each user and security has a security Labels
- if labels match some conditions, then access is guaranteed
- resource access must not change during import/export of datas
- Role Based Access Control (RBAC): roles decides
- each user has a role
- roles determine access rights
- Principles:
- least privilege: each user should have the minimal access privileges to accomplish its tasks
- separating duties: avoid to have users with too much power
- policies combination: combine policies for finer access control
- Terminology:
- Users: active in the system.
- Objects: passive in the system.
- Access rights: read, write, execute, delede, create, switch, move, ...
- System description: (S, O, A, M: S x O -> P(A)) where
- S = set of subjects
- O = set of Objects
- A = set of access rights
- M: S x O -> P(A) = matrix associating to every subject and object a set of access rights in A
- in MAC there is also:
- (L,>) = partially ordered set of labels
- l: S U O -> L = labeling function associating a label to each object and subject
Bell LaPadula Model (MAC)
[The model preserves confidentiality but not integrity of data!]
- Simple security rule [or ss-rule] (no read up): a subject s can read an object o only if l(s)=l(o) or l(s)>l(o)
- *-Property (no write down): a subject s can write an object o only if l(s)=l(o) or l(s)<l(o)
- Discretionary security property [or ds-property]: users can grant access to objects according with ss-rule and *-property
State of a system
- (C, M, l) where
- C = configuration / current access status: it is given by a set of triple of the form (s,o,a) in S x O x A
- M and l are respectively the access matrix and the label function (which may be updated)
- Possible evolutions (operational semantic rules):
- add (s,o,a) to C when s get the access right a to o
- remove (s,o,a) from C when s release the access right a to o
- change l(s) when the security label of s is changed
- change l(o) when the security label of o is changed
- add a to M(s,o) to give s the access right a on o
- remove a from M(s,o) to rescind s the access right a on o
- a subset C of S x O x A may evolve to C' if C' may be obtained by applying operational semantic rules to C
Suggested reading
Week 6, 22 March (Matteo): Chinese Wall
- In the Bell-LaPadula model if a configuration C satisfies the ss-rule, *-property and ds-property, then any confuguration C' which may be obtained by applying operational semantic rules to C does.
- Troyan-horse example in Bell-LaPadula:
- S:={Alice, Bob}
- O:={Info, Stole}
- M:=
|
Alice |
Bob |
Info |
Read, Write |
None |
Stole |
Read, Write |
Read |
- (L,<):= ({top,bot} , top<bot)
- l: S U O -> L:=
l(Alice)=l(Info)=top and l(Bob)=l(Stole)=bot
- the initial configuration is the empty one, the final configuration should be
{(Alice, Info, Read), (Alice, Stole, Write), (Bob ,Stole , Read)}
Chinese Wall or Brewer-Nash (DAC + Mandatory access)
- objects have owners (companies databases)
- each company belongs to a conflic of interest class
- you can think that every object has a label (owner, owner's conflict of interest class)
- SS-rule: a subject s can read an object o belonging to a company x only if
- s had no access to any object in a different company x' in the same conflict of interest class
- *-Property: a subject s can write an object o belonging to a company x only if
- s have read access to o
- s had read access only to objects in x's database
Suggested reading
Week 7, 1 April (Ross Horne): Hardware security:
Spring break (week of the 5th of April)
Week 8, 15 April (Sjouke Mauw): Intro to protocols
Week 9, 22 April (Ross Horne): students presentations on access control models
Week 10, 29 April (Sergiu Bursuc): Protocol verification inProverif
Week 11, 6 May (Semyon Yurkov): ePayment protocol proof in Proverif
Week 12, 13 May (Reynaldo Gil Pons): Mafia fraud proof in Proverif
Week 13, 20 May (Sergiu Bursuc): Advanced
Week 14, 27 May (Sergiu Bursuc): Advanced