Skip to main content
Department of Information Technology

Security Models

To reason abstractly about security, and the correspondence between mechanisms and policies, we need formal models of security.

Information flow

Access control makes sure all direct accesses to objects are allowed. This does not solve all problems.

Example:

  • "read" not in M(p,f), "read" in M(q,f)
    p can not read f, but q can
  • "read" in M(p,g) w in M(q,g)
    p can read g, and q can write it.

What can happen, even if all rights are checked correctly?

q reads f (which p cannot read), and writes the contents to g (where p can read it)

What to do:

  • use mandatory access control (MAC)
  • analyse information flows

Different analyses and policies for different goals (see below).

Multi-Level Security: (MLS) use different security classes, e.g.

  • supervisor/user mode in processors
  • superuser/user access in e.g. Unix
  • ring protection in more advanced processors and OSs (e.g. kernel/OS/utilities/user pgms)
  • military: top secret, secret, confidential, unclassified

[Above: totally ordered, but also partial orders can be used.]

Harrison-Ruzzo-Ullman

HRU model handles changes to protection, and provides nice example about policy verification. This part of the notes has more detail than the book.

Subjects S, objects O, access matrix M,
+ access rights A:

  • enforcement: read, write, execute, append...
  • rights movement: own, control, *, +
  • domain change: enter [changes row for executing subject]

Updates to the matix by primitive operations:

  • enter a into M(s,o)
  • delete a from M(s,o)
  • create subject/object s/o [adds to S/O, and a row/column to M]
  • delete subject/object s/o

Commands specify mechanisms for access control modification. Defined using conditions on M and primitive operations.

2.1. Examples

Examples showing the semantics of "own" [slides]:

command create_file(p,f)      // p process (subj), f file (obj)
    create object f	      // create the object
    enter "own" into M(p,f)   // set default permissions for creator
    enter "read" into M(p,f)
    enter "write" into M(p,f)
end

command grant_read(p,q,f)	// owner p can give read rights on f to q
    if "own" in M(p,f)
    then enter "read" into M(q,f)
end

2.1.1. Transferrable permissions

Semantics (meaning) of transferrable permissions can be defined by commands:

*-marked permissions can be copied (without the *) to others

command copy_read(p,q,f)
    if "read*" in M(p,f)
    then enter "read" into M(q,f)
end

Further transfer: +-marked permissions can be transferred to others, losing the permission

command transfer_read(p,q,f)
    if "read+" in M(p,f)
    then
	delete "read+" from M(p,f)
	enter "read+" into M(q,f)
end

2.2. States, Transitions, and Properties

The state of the access control system is the current values of (S,O,M).

Transitions are defined by the commands and their effects on (S,O,M) [the state].

Write P --c--> Q if the command c takes the state P to the state Q.
[example using create_fileÅ

2.2.1. Property: Leaking rights

A state P = (S1,O1,M1) leaks the right r if

  • there is a transition from P to a state Q = (S2,O2,M2)
    such that for some s in S1 and o in O1,
    r not in M1(s,o) and r in M2(s,o)
(i.e: the transition adds r to a place where it wasn't)

Safe states:
A state P is safe with respect to r if no sequence of transitions from P leaks r.

Verifying safety in general is undecidable, but under some circumstances it is decidable (single primitive operation in every command, or finite number of subjects).
Cf. 3rd design principle: complexity/simplicity, assurance.

2.3. Policies

Note: the state (by M) specifies what subjects can do, not necessarily what the may do.

We can use HRU to define security policies. Security policies say which states are authorised.

2.3.1. Example: only one reader, only one writer

"For each buffer b, there is exactly one process p which can write to it, and only one process q which can read from it"

  • A state Q = (S,O,M) is authorised only if
    • for every buffer b in O:
      • the set { p : p in S and "read" in M(p,b) } is a singleton
      • the set { p : p in S and "write" in M(p,b) } is a singleton

2.3.2. Example: only granted permissions

"No subject can get access to a file f unless that right has been granted by the owner of f"

  • if Q = (S,O,M) is an authorised state, and
    • for some file f and subject s,
      • "read" not in M(s,f) and Q --c--> (S1,O1,M1) such that "read" in M1(s,f)
        (i.e. the command c enters "read" rights for s on f)
    • then (S1,O1,M1) is authorised only if
      • for some p in S, "own" in M(p,f) and c = grant_read(p, s, f)
        (i.e. p was the owner of f in the state Q, and used grant_read to give the right to s)
2.4. Verifying policies

Using e.g. HRU we can formally verify whether a set of mechanisms enforces a policy.

  • both mechanisms and policy formally defined

If R is the set of reachable states, and P is the set of authorised states,

  • the system is secure if R is a subset of P
  • the system is precise if R = P

In general undecidable [draw figure].

2.5. Bell-LaPadula (BLP)

Very standard model; a bit complex.

  • MLS: each subject and object has a security level (these are either totally ordered or partially ordered and form a lattice)
  • captures confidentiality aspects: information can not flow from more secure to less secure.
  • intended for static permissions (constant M)

Standard desired properties:

  • no read up: can't read from more secure levels
  • no write down: can't write to less secure (e.g. copy "secret" to "public")

Subjects S, objects O, access operations A (r,w,x,a)
+ a set L of security levels, partially ordered.

A state is a triple (b, M, f) where

  • b is the currently active accesses: a set of (s,o,a) triples
  • M is the current access control matrix (current permissions)
  • f is the current security level assignment:
    • three functions (fs, fc, fo) where
      • fs(s) is the maximal security level the subject s can have (clearance)
      • fc(s) is the current security level of the subject s
      • fo(o) is the classification of the object o (its security level)
    • and fc(s) <= fs(s) (fs dominates fc)

Transitions change b and f.

Policies: standard properties below.

2.5.1. Simple Security property (ss-property)

A state (b,M,f) satisfies the ss-property if

  • forall (s,o,a) in b:
    • if a is read or write, fo(o) <= fs(s) [note fs: max level]
      (a subject may read or write only if it has at least as high security clearance as the object - no read up)

This doesn't help against the example above. Need to control also write operations!

2.5.2. Star property (*-property)

A state (b,M,f) satisfies the *-property if

  • forall (s,o,a) in b:
    • if a is write or append,
      • fc(s) <= fo(o) (no write down) and [note fc: current level]
      • forall other (s,o1,a1) in b such that a1 is read or write: fo(o1) <= fo(o)
        (can't be reading a higher level object while writing a lower)

Sometimes necessary for high-level subject to write low-level object. Solutions:

  • downgrade: temporarily move the subject to a lower level (fc < fs)
  • trusted subjects: define a set of trusted subject which are allowed to break *-property (assuming they always "clean" the information)

Note:

  • no memory in subjects (or as long as they can read o, (s,o,read) is in b)
  • "trusted" means "can hurt you" (cf. "trustworthy": verified not hurting)

2.5.3. Discretionary security property (ds-property)

A state (b,M,f) satisfies the ds-property if

  • forall (s,o,a) in b, a is in M(s,o)
    (only permitted accesses are allowed)

2.5.4. Secure state

A state is secure if all of the ss-property, *-property, and ds-property hold.

2.5.5. Basic security theorem

Suppose we have transitions between states:
(b1,M1,f1) ---> (b2,M2,f2) is secure if both states are secure.

If the initial state is secure, and all transitions are secure, then the the system is secure.

How do we show this? We show that the transitions preserve the properties.
Example: the ss-property is preserved if and only if:

  • for b = b2 minus b1:
    • (b,_,f2) satisfies ss-property [new accesses are ss-OK] and
    • if (s,o,a) in b1 does NOT satisfy the ss-property with respect to f2, then (s,o,a) is not in b2
      i.e. if ( { (s,o,a) }, _, f2) does not satisfy the ss-property, then (s,o,a is not active after the transition
      i.e. accesses in b1 which are not OK with the new security assignment are not active after the transition
2.6. Biba

Deals with integrity; basically uses integrity levels, and reverses the permitted flows (information may flow from "clean" high level to "dirty" low level).

Updated  2007-09-27 09:20:12 by Björn Victor.