wieerwill/Informatik
1
0
Fork 0
Code Issues Pull Requests Actions Packages Projects Releases Wiki Activity

grammarand math fixes

Browse Source
This commit is contained in:
WieErWill 2021-08-02 12:29:06 +02:00
parent 6d6ab90728
commit f062f24f13
1 changed files with 108 additions and 115 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

223
Systemsicherheit.md
View File

@ -407,8 +407,7 @@ in privileged system software:
Consequence: Privileged software can be tricked into executing attacker’s code
Approach: Cleverly forged parameters overwrite procedure activation frames in
memory
Approach: Cleverly forged parameters overwrite procedure activation frames in memory
- -> exploitation of missing length checks on input buffers
- -> buffer overflow
@ -1045,7 +1044,7 @@ Access Control Functions [Lampson, 1974]
- any $s\in S$ represents an authenticated active entity (e. g. a user or process) which potentially executes operations on objects
- any $o\in O$ represents an authenticated passive entity (e. g. a file or a database table) on which operations are executed
- for any $s\in S$,$o\in O$,$op\in OP$:s is allowed to execute op on o iff f(s,o,op)=true.
- Model making: finding a $tuple⟨S,O,OP,f⟩$
- Model making: finding a $tuple\langleS,O,OP,f\rangle$
- $\rightarrow$ Definition of S,O, and OP
- $\rightarrow$ Definition of f
@ -1142,7 +1141,7 @@ Our HIS scenario ... modeled by an ACM:
We might do it like this, but ... Privilege escalation question:
"Can it ever happen that in a given state, some specific subject obtains a specific permission?"
$\varnothing \Rightarrow \{r,w\}$
- ACM models a single state ⟨S,O,OP,m⟩
- ACM models a single state \langleS,O,OP,m\rangle
- ACM does not tell us anything about what might happen in the future
- Behavior prediction $\rightarrow$ proliferation of rights $\rightarrow$ HRU safety
@ -1159,14 +1158,14 @@ Idea [Harrison et al., 1976]: A (more complex) security model combining
This idea was pretty awesome. We need to understand automata, since from then on they were used for most security models. $\rightarrow$ Small excursus
##### Deterministic Automata
Mealy Automaton: $⟨Q,\sum,\Omega,\delta,\lambda,q_0⟩$
Mealy Automaton: $\langleQ,\sum,\Omega,\delta,\lambda,q_0\rangle$
- $Q$ is a finite set of states (state space), e. g. $Q=\{q_0 ,q_1 ,q_2\}$
- $\sum$ is a finite set of input words (input alphabet), e. g. $\sum=\{a,b\}$
- $\Omega$ is a finite set of output words (output alphabet), e. g. $\Omega=\{yes,no\}$
- $\delta:Q\times\sum\rightarrow Q$ is the state transition function
- $\lambda:Q\times\sum\rightarrow\Omega$ is the output function
- $q_0\in Q$ is the initial state
- $\delta(q,\sigma)=q′$ and $\lambda(q,\sigma)=\omega$ can be expressed through thestate diagram: a directed graph $⟨Q,E⟩$, where each edge $e\in E$ is represented by a state transition’s predecessor node $q$, its successor node $q′$, and a string "$\sigma|\omega$" of its input and output, respectively.
- $\delta(q,\sigma)=q′$ and $\lambda(q,\sigma)=\omega$ can be expressed through thestate diagram: a directed graph $\langleQ,E\rangle$, where each edge $e\in E$ is represented by a state transition’s predecessor node $q$, its successor node $q′$, and a string "$\sigma|\omega$" of its input and output, respectively.
![](Assets/Systemsicherheit-mealy-automaton.png)
Example: Return "yes" for any input in an unbroken sequence of "a" or "b", "no" otherwise.
@ -1191,7 +1190,7 @@ How we use Deterministic Automata
- Effects ofoperationsthat cause such transitions are described by the state transition function
- Analyses ofright proliferation($\rightarrow$ privilege escalation)are enabled by state reachability analysis methods
An HRU model is a deterministic automaton $⟨Q,\sum,\delta,q_0 ,R⟩$ where
An HRU model is a deterministic automaton $\langleQ,\sum,\delta,q_0 ,R\rangle$ where
- $Q= 2^S\times 2^O\times M$ is the state space where
- S is a (not necessarily finite) set of subjects,
- O is a (not necessarily finite) set of objects,
@ -1211,7 +1210,7 @@ Interpretation
- current ACM $m_q\in M$ where $m_q:S_q\times O_q\rightarrow 2^R$
- State transitions modeled by $\delta$ based on
- the current automaton state
- an input word $⟨op,(x_1,...,x_k)⟩\in\sum$ where $op$
- an input word $\langleop,(x_1,...,x_k)\rangle\in\sum$ where $op$
- may modify $S_q$ (create a user $x_i$, kill a process $x_i$ etc.),
- may modify $O_q$ (create/delete a file $x_i$, open a socket $x_i$ etc.),
- may modify the contents of a matrix cell $m_q(x_i,x_j)$ (enter or remove rights) where $1\leq i,j\leq k$.
@ -1220,7 +1219,7 @@ Interpretation
##### State Transition Scheme (STS)
Using the STS, $\sigma:Q\times\sum\rightarrow Q$ is defined by a set of specifications in the normalized form
$\sigma(q,⟨op,(x_1,...,x_k)⟩)$=if $r_1\in m_q(x_{s1},x_{o1}) \wedge ... \wedge r_m\in m_q(x_{sm},x_{om})$ then $p_1\circle ...\circle p_n$ where
$\sigma(q,\langleop,(x_1,...,x_k)\rangle)$=if $r_1\in m_q(x_{s1},x_{o1}) \wedge ... \wedge r_m\in m_q(x_{sm},x_{om})$ then $p_1\circle ...\circle p_n$ where
- $q=\{S_q,O_q,m_q\}\in Q,op\in OP$
- $r_1 ...r_m\in R$
- $x_{s1},...,x_{sm}\in S_q$ and $x_{o1},...,x_{om}\in O_q$ where $s_i$ and $o_i$, $1\leq i\leq m$, are vector indices of the input arguments: $1\leq s_i,o_i\leqk$
@ -1237,7 +1236,7 @@ Conditions:
Expressions that need to evaluate "true" for state q as a necessary precondition for command $op$ to be executable (= can be successfully called).
Primitives:
Short, formal macros that describe differences between $q$ and $a$ successor state $q′=\sigma(q,⟨op,(x_1 ,...,x_k)⟩)$ that result from a complete execution of op:
Short, formal macros that describe differences between $q$ and $a$ successor state $q′=\sigma(q,\langleop,(x_1 ,...,x_k)\rangle)$ that result from a complete execution of op:
- enter r into $m(x_s,x_o)$
- delete r from $m(x_s,x_o)$
- create subject $x_s$
@ -1251,7 +1250,7 @@ Note the atomic semantics: the HRU model assumes that each command successfully
How to Design an HRU Security Model:
1. Model Sets: Subjects, objects, operations, rights $\rightarrow$ define the basic sets $S,O,OP,R$
2. STS: Semantics of operations (e. g. the future API of the system to model) that modify the protection state $\rightarrow$ define $\sigma$ using the normalized form/programming syntax of the STS
3. Initialization: Define a well-known initial stateq $0 =⟨S_0 ,O_0 ,m_0 ⟩$ of the system to model
3. Initialization: Define a well-known initial stateq $0 =\langleS_0 ,O_0 ,m_0 \rangle$ of the system to model
An Open University Information System
![](Assets/Systemsicherheit-university-information-system.png)
@ -1278,7 +1277,7 @@ Model Making
2. State Transition Scheme
- Effects of operations on protection state:
- writeSolution
Informal Policy: "A sample solution (...) can be downloaded by students only after submitting their own solution." $\Leftrightarrow$ "If the automaton receives an input ⟨writeSolution,(s,o)⟩ and the conditions are satisfied, it transitions to a state where s is allowed to download the sample solution."
Informal Policy: "A sample solution (...) can be downloaded by students only after submitting their own solution." $\Leftrightarrow$ "If the automaton receives an input \langlewriteSolution,(s,o)\rangle and the conditions are satisfied, it transitions to a state where s is allowed to download the sample solution."
```
command writeSolution(s,o) ::= if write $\in$ m(s,o)
then
@ -1286,7 +1285,7 @@ Model Making
fi
```
- readSample
Informal Policy: "Student solutions can be submitted only before downloading any sample solution." $\Leftrightarrow$ "If the automaton receives an input⟨readSample,(s,o)⟩and the conditions are satisfied, it transitions to a state wheresis denied to submit a solution."
Informal Policy: "Student solutions can be submitted only before downloading any sample solution." $\Leftrightarrow$ "If the automaton receives an input\langlereadSample,(s,o)\rangleand the conditions are satisfied, it transitions to a state wheresis denied to submit a solution."
```
command readSample(s,o) ::= if read$\in$ m(s,o)
then
@ -1294,7 +1293,7 @@ Model Making
fi
```
3. Initialization
- By model definition: $q_0 =⟨S_0 ,O_0 ,m_0 ⟩$
- By model definition: $q_0 =\langleS_0 ,O_0 ,m_0 \rangle$
- For a course with (initially) three students:
- $S_0 =\{sAnn, sBob, sChris\}$
- $O_0 =\{oAnn, oBob, oChris\}$
@ -1359,7 +1358,7 @@ A state q of an HRU model is called HRU safe with respect to a right $r\in R$ if
According to Tripunitara and Li [2013], this property (Due to more technical details, it’s called simple-safety there.) is defined as:
> HRU Safety
>
> For a state $q=\{S_q,O_q,m_q\}\in Q$ and a right $r\in R$ of an HRU model $⟨Q,\sum,\delta,q_0,R⟩$, the predicate $safe(q,r)$ holds iff
> For a state $q=\{S_q,O_q,m_q\}\in Q$ and a right $r\in R$ of an HRU model $\langleQ,\sum,\delta,q_0,R\rangle$, the predicate $safe(q,r)$ holds iff
> $\forall q′= S_{q′},O_{q′},m_{q′} \in \{\delta^^*(q,\sigma^^*)|\sigma^^*\in\sum^^*\},\forall s\in S_{q′},\forall o\in O_{q′}: r\in m_{q′}(s,o)\Rightarrow s\in S_q \wedge o\in O_q \wedge r\in m_q(s,o)$.
>
> We say that an HRU model is safe w.r.t. r iff $safe(q_0 ,r)$.
@ -1546,7 +1545,7 @@ Idea:
Outline: Two-phase-algorithm to analyze $safe(q_0,r)$:
1. Static phase: Infer knowledge from the model that helps heuristic to make "good" decisions.
- $\rightarrow$ Runtime: polynomial in model size ($q_0 + STS$)
2. Simulation phase: The automaton is implemented and, starting with $q_0$, fed with inputs $\sigma=⟨op,x⟩$
2. Simulation phase: The automaton is implemented and, starting with $q_0$, fed with inputs $\sigma=\langleop,x\rangle$
- $\rightarrow$ For each $\sigma$, the heuristic has to decide:
- which operation op to use
- which vector of arguments x to pass
@ -1588,11 +1587,11 @@ Goal
Idea [Sandhu, 1992]
- Adopted from HRU: subjects, objects, ACM, automaton
- New:leverage the principle of strong typing known from programming
- New: leverage the principle of strong typing known from programming
- $\rightarrow$ safety decidability properties relate to type-based restrictions
How it Works:
- Foundation of a TAM model is an HRU model $⟨Q,\sum,\delta,q_0 ,R⟩$, where $Q= 2^S\times 2^O\times M$
- Foundation of a TAM model is an HRU model $\langleQ,\sum,\delta,q_0 ,R\rangle$, where $Q= 2^S\times 2^O\times M$
- However: $S\subseteq O$, i. e.:
- all subjects can also act as objects (=targets of an access)
- $\rightarrow$ useful for modeling e. g. delegation ("s has the right to grant s′ her read-right")
@ -1604,7 +1603,7 @@ How it Works:
> TAM Security Model
>
> A TAM model is a deterministic automaton $⟨Q,\sum,\delta,q_0 ,T,R⟩$ where
> A TAM model is a deterministic automaton $\langleQ,\sum,\delta,q_0 ,T,R\rangle$ where
> - $Q= 2^S\times 2^O\times TYPE\times M$ is the state space where $S$ and $O$ are subjects set and objects set as in HRU, where $S\subseteq O$, $TYPE=\{type|type:O\rightarrow T\}$ is a set of possible type functions, $M$ is the set of possible $ACMs$ as in HRU,
> - $\sum=OP\times X$ is the (finite) input alphabet where $OP$ is a set of operations as in HRU, $X=O^k$ is a set of $k$-dimensional vectors of arguments (objects) of these operations,
> - $\delta:Q\times\sum\rightarrow Q$ is the state transition function,
@ -1760,13 +1759,13 @@ Auxiliary analysis tools for TAM models:
> Parent- and Child-Types
>
> For any operation $op$ with arguments $⟨x_1,t_1⟩,⟨x_2,t_2⟩,...,⟨x_k,t_k⟩$ in an STS of a TAM model, it holds that $t_i, 1\leq i\leq k$
> For any operation $op$ with arguments $\langlex_1,t_1\rangle,\langlex_2,t_2\rangle,...,\langlex_k,t_k\rangle$ in an STS of a TAM model, it holds that $t_i, 1\leq i\leq k$
> - is a child type in op if one of its primitives creates a subject or object $x_i$ of type $t_i$,
> - is a parent type in op if none of its primitives creates a subject or object $x_i$ of type $t_i$.
> Type Creation Graph
>
> The type creation graph $TCG=⟨T,E=T\times T⟩$ for the STS of a TAM model is a directed graph with vertex set $T$ and an $edge⟨u,v⟩\in E$ iff $\exists op\in OP:u$ is a parent type in $op\wedge v$ is a child type in op.
> The type creation graph $TCG=\langleT,E=T\times T\rangle$ for the STS of a TAM model is a directed graph with vertex set $T$ and an $edge\langleu,v\rangle\in E$ iff $\exists op\in OP:u$ is a parent type in $op\wedge v$ is a child type in op.
Example STS:
```bash
@ -1893,7 +1892,7 @@ RBAC Idea
RBAC Security Model Definition
> Basic RBAC model: "$RBAC_0$" [Sandhu, 1994]:
>
> An RBAC 0 model is a tuple $⟨U,R,P,S,UA,PA,user,roles⟩$ where
> An RBAC 0 model is a tuple $\langleU,R,P,S,UA,PA,user,roles\rangle$ where
> - U is a set of user identifiers,
> - R is a set of role identifiers,
> - P is a set of permission identifiers,
@ -1901,7 +1900,7 @@ RBAC Security Model Definition
> - $UA\subseteq U\times R$ is a many-to-many user-role-relation,
> - $PA\subseteq P\times R$ is a many-to-many permission-role-relation,
> - $user:S\rightarrow U$ is a total function mapping sessions to users,
> - $roles:S\rightarrow 2^R$ is a total function mapping sessions to sets of roles such that $\forall s\in S:r\in roles(s)\Rightarrow ⟨user(s),r⟩\in UA$.
> - $roles:S\rightarrow 2^R$ is a total function mapping sessions to sets of roles such that $\forall s\in S:r\in roles(s)\Rightarrow \langleuser(s),r\rangle\in UA$.
Interpretation
- Users U model people: actual humans that operate the AC system
@ -1924,7 +1923,7 @@ Note the difference between users in RBAC and subjects in IBAC: the latter usual
##### RBAC Access Control Function
- Authorization in practice: access rules have to be defined for operations on objects (cf. IBAC)
- IBAC approach: access control function $f:S\times O\times OP\rightarrow \{true,false\}$
- RBAC approach: implicitly defined through $P\rightarrow$ made explicit: $P\subseteq O\times OP$ is a set of permission tuples $⟨o,op⟩$ where
- RBAC approach: implicitly defined through $P\rightarrow$ made explicit: $P\subseteq O\times OP$ is a set of permission tuples $\langleo,op\rangle$ where
- $o\in O$ is an object from a set of object identifiers,
- $op\in OP$ is an operation from a set of operation identifiers.
- We may now define the $ACF$ for $RBAC_0$:
@ -1932,7 +1931,7 @@ Note the difference between users in RBAC and subjects in IBAC: the latter usual
> $RBAC_0$ ACF
>
> $f_{RBAC_0}:U \times O\times OP\rightarrow\{true,false\}$ where
> $f_{RBAC_0} (u,o,op)= \begin{cases} true, \quad \exists r\in R,s\in S:u=user(s)\wedge r\in roles(s)\wedge ⟨⟨o,op⟩,r⟩ \in PA \\ false, \quad\text{ otherwise\end{cases}$.
> $f_{RBAC_0} (u,o,op)= \begin{cases} true, \quad \exists r\in R,s\in S:u=user(s)\wedge r\in roles(s)\wedge \langle\langleo,op\rangle,r\rangle \in PA \\ false, \quad\text{ otherwise\end{cases}$.
##### RBAC96 Model Family
Sandhu et al. [1996]
@ -1946,12 +1945,12 @@ RBAC 1 : Role Hierarchies
- Observation: Roles in organizations often overlap:
- Users in different roles havecommon permissions: "Any project manager must have the same permissions as any developer in the same project."
- Approach 1: disjoint permissions for roles proManager and proDev $\rightarrow$ any proManager user must always have proDev assigned and activated for any of her workflows $\rightarrow$ role assignment redundancy
- Approach 2: overlapping permissions: $\forall p\in P:⟨p,proDev⟩ \in PA\Rightarrow ⟨p,proManager⟩ \in PA\rightarrow$ any permission for project developers must be assigned to two different roles $\rightarrow$ role definition redundancy
- Approach 2: overlapping permissions: $\forall p\in P:\langlep,proDev\rangle \in PA\Rightarrow \langlep,proManager\rangle \in PA\rightarrow$ any permission for project developers must be assigned to two different roles $\rightarrow$ role definition redundancy
- Two types of redundancy $\rightarrow$ undermines scalability goal of RBAC!
- Solution
- Role hierarchy: Eliminates role definition redundancy through permissions inheritance
- Modeling Role Hierarchies
- Lattice here: $⟨R,\leq⟩$
- Lattice here: $\langleR,\leq\rangle$
- Hierarchy expressed through dominance relation: $r_1\leq r_2 \Leftrightarrow r_2$ inherits any permissions from $r_1$
- Interpretation
- Reflexivity: any role consists of ("inherits") its own permissions $\forall r\in R:r\leq r$
@ -1960,9 +1959,9 @@ RBAC 1 : Role Hierarchies
> $RBAC_1$ Security Model
>
> An $RBAC_1$ model is a tuple $⟨U,R,P,S,UA,PA,user,roles,RH⟩$ where
> An $RBAC_1$ model is a tuple $\langleU,R,P,S,UA,PA,user,roles,RH\rangle$ where
> - $U,R,P,S,UA,PA$ and $user$ are defined as for $RBAC_0$,
> - $RH\subseteq R\times R$ is a partial order that represents a role hierarchy where $⟨r,r′⟩\in RH\Leftrightarrow r\leq r′$ such that $⟨R,\leq⟩$ is a lattice,
> - $RH\subseteq R\times R$ is a partial order that represents a role hierarchy where $\langler,r′\rangle\in RH\Leftrightarrow r\leq r′$ such that $\langleR,\leq\rangle$ is a lattice,
> - roles is defined as for $RBAC_0$, while additionally holds: $\forall r,r′\in R,\exists s\in S:r\leq r′\wedge r′\in roles(s)\Rightarrow r\in roles(s)$.
In prose: When activating any role that inherits permissions from another role, this other role isautomatically(by definition) active as well.
@ -1982,8 +1981,8 @@ RBAC 2 : Constraints
- Temporal constraints: time/date/week/... of role activation (advanced RBAC models, e.g. Bertino et al. [2001])
- Factual constraints: assigning or activating roles for specific permissions causally depends on any roles for a certain, other permissions (e.g. only allow user $u$ to activate auditingDelegator role if audit payments permission is usable by $u$)
- Modeling Constraints:(idea only)
- $RBAC_2 : ⟨U,R,P,S,UA,PA,user,roles,RE⟩$
- $RBAC_3 : ⟨U,R,P,S,UA,PA,user,roles,RH,RE⟩$
- $RBAC_2 : \langleU,R,P,S,UA,PA,user,roles,RE\rangle$
- $RBAC_3 : \langleU,R,P,S,UA,PA,user,roles,RH,RE\rangle$
- where $RE$ is aset of logical expressions over the other model components (such as $UA,PA,user,roles$).
##### RBAC Summary
@ -2025,7 +2024,7 @@ Idea: Generalizing the principle of indirection already known from RBAC
- $f_{IBAC}:S\times O\times OP\rightarrow\{true,false\}$
- $f_{RBAC}:U\times O\times OP\rightarrow\{true,false\}$
- $f_{ABAC}:S\times O\times OP\rightarrow\{true,false\}$
- $\rightarrow$ Evaluates attribute values for $⟨s,o,op⟩$, e. g.: $f_{ABAC}(user,game,download)=game.pegi \leq user.age$
- $\rightarrow$ Evaluates attribute values for $\langles,o,op\rangle$, e. g.: $f_{ABAC}(user,game,download)=game.pegi \leq user.age$
##### ABAC Security Model
- Note: There is no such thing (yet) like a standard ABAC model (such as RBAC96).
@ -2034,7 +2033,7 @@ Idea: Generalizing the principle of indirection already known from RBAC
> ABAC Security Model
>
> An ABAC security model is a tuple $⟨S,O,AS,AO,attS,attO,OP,AAR⟩$ where
> An ABAC security model is a tuple $\langleS,O,AS,AO,attS,attO,OP,AAR\rangle$ where
> - $S$ is a set of subject identifiers and $O$ is a set of object identifiers,
> - $A_S=V_S^1 \times...\times V_S^n$ is a set of subject attributes, where each attribute is an n-tuple of values from arbitrary domains $V_S^i$, $1\leq i \leq n$,
> - $A_O=V_O^1\times...\times V_O^m$ is a corresponding set of object attributes, based on values from arbitrary domains $V_O^j$, $1\leq j \leq m$,
@ -2057,7 +2056,7 @@ With conditions from $\Phi$ for executing operations in $OP,AAR$ determines the
> ABAC ACF
>
> $f_{ABAC}:S\times O\times OP\rightarrow\{true,false\}$ where
> $f_{ABAC}(s,o,op)= \begin{cases} true, \quad\exists ⟨\phi,op⟩\in AAR:\phi(s,o)=true\\ false, \quad\text{ otherwise }$.
> $f_{ABAC}(s,o,op)= \begin{cases} true, \quad\exists \langle\phi,op\rangle\in AAR:\phi(s,o)=true\\ false, \quad\text{ otherwise }$.
> We call $\phi$ an authorization predicate for $op$.
Example 1: Online Game Store
@ -2069,7 +2068,7 @@ Example 1: Online Game Store
- $att_S:S\rightarrow A_S$: assigns age attribute to clients
- $att_O:O\rightarrow A_O$: assigns PEGI rating attribute to games
- $OP=\{download\}$: sole operation
- One simpleauthorization rule: $AAR=\{⟨att_O(o) \leq att_S(s),download⟩\}$
- One simpleauthorization rule: $AAR=\{\langleatt_O(o) \leq att_S(s),download\rangle\}$
Example 2: Document Management System
- Policy goal: Enforce document confidentiality
@ -2080,7 +2079,7 @@ Example 2: Document Management System
- $att_S:S\rightarrow A_S$: assigns trustworthiness value to user (e. g. based on management level)
- $att_O:O\rightarrow A_O$: assigns confidentiality level to documents
- $OP=\{read,write,append,...\}$: operations
- Authorization rules: $AAR=\{⟨att_O(o)\leq att_S(s),read⟩,⟨att_S(s) \leq att_O(o),write⟩,...\}$
- Authorization rules: $AAR=\{\langleatt_O(o)\leq att_S(s),read\rangle,\langleatt_S(s) \leq att_O(o),write\rangle,...\}$
##### ABAC Summary
- Scalability
@ -2095,10 +2094,6 @@ Example 2: Document Management System
- cf. HRU:safety properties?
- solution approach: automaton-based ABAC model ...
### Information Flow Models
Abstraction Level of AC Models: rules about subjects accessing objects
@ -2121,10 +2116,10 @@ Lattices (refreshment)
> Self-Study Task
>
> I work on six days in a $week:W=\{Mo,Tu,We,Th,Fr,Sa\}$. On each of these days, I can decide to procrastinate work from daywtow′: the same or a day later that week $(w\rightarrow w′)$. For a lattice $⟨W,\rightarrow⟩$:
> I work on six days in a $week:W=\{Mo,Tu,We,Th,Fr,Sa\}$. On each of these days, I can decide to procrastinate work from daywtow′: the same or a day later that week $(w\rightarrow w′)$. For a lattice $\langleW,\rightarrow\rangle$:
> - Draw the lattice as a graph.
> - Determine $inf_W$ and $sup_W$.
> Let’s assume that Saturday is exclusively reserved for work I was unable to do on Monday. Is $⟨W,\rightarrow⟩$ still a lattice now? Why (not)?
> Let’s assume that Saturday is exclusively reserved for work I was unable to do on Monday. Is $\langleW,\rightarrow\rangle$ still a lattice now? Why (not)?
Implementation of Information Flow Models
- Background: Information flows and read/write operations are isomorphic
@ -2143,10 +2138,10 @@ On of the first information flow models [Denning, 1976]:
> Denning Security Model
>
> A Denning information flow model is a tuple $⟨S,O,L,cl,\bigoplus⟩$ where
> A Denning information flow model is a tuple $\langleS,O,L,cl,\bigoplus\rangle$ where
> - S is a set of subjects,
> - O is a set of objects,
> - $L=⟨C,\leq⟩$ is a lattice where
> - $L=\langleC,\leq\rangle$ is a lattice where
> - C is a set of classes,
> - $\leq$ is a dominance relation wherec $\leq d \Leftrightarrow$ information may flow from c to d,
> - $cl:S\cup O\rightarrow C$ is a classification function, and
@ -2159,7 +2154,7 @@ Interpretation
- Classification function $cl$ assigns a class to each entity, e.g. $cl(cox)=Physician$
- Reclassification function $\bigoplus$ determines which class an entity is assigned after receiving certain a information flow; e.g. for Physician to Patient: $\bigoplus (Physician,Patient)=sup_{\{Physician,Patient\}}$
Example $⟨S,O,L,cl,\bigoplus⟩$ mit $L=⟨C,\leq⟩$:
Example $\langleS,O,L,cl,\bigoplus\rangle$ mit $L=\langleC,\leq\rangle$:
- $S=O=\{cox,kelso,carla,...\}$
- $C=\{Physician, Anamnesis, Pharmacy, Medication,...\}$
- dominance relation $\leq$:
@ -2193,7 +2188,7 @@ Modeling Confidentiality Levels
- Note: In contrast du Denning, $\leq$ in MLS models is a total order.
Example
- Lattice $⟨\{public,confidential,secret\},\leq⟩$ where $\leq=\{⟨public,confidential⟩,⟨confidential,secret⟩\}$
- Lattice $\langle\{public,confidential,secret\},\leq\rangle$ where $\leq=\{\langlepublic,confidential\rangle,\langleconfidential,secret\rangle\}$
- Objects $O=\{ProjectXFiles, Timetable, BulletinBoard\}$
- Subjects $S=\{Ann, Bob\}$
- Classification of objects (classification level):
@ -2226,7 +2221,7 @@ Incorporates impacts on model design ...
Idea:
- entity sets S,O
- $lattice⟨C,\leq⟩$ defines information flows by
- $lattice\langleC,\leq\rangle$ defines information flows by
- C: classification/clearance levels
- $\leq$: hierarchy of trust
- classification function $cl$ assigns
@ -2236,9 +2231,9 @@ Idea:
> BLP Security Model
>
> A BLP model is a deterministic automaton $⟨S,O,L,Q,\sum,\sigma,q_0,R⟩$ where
> A BLP model is a deterministic automaton $\langleS,O,L,Q,\sum,\sigma,q_0,R\rangle$ where
> - S and O are (static) subject and object sets,
> - $L=⟨C,\leq⟩$ is a (static) lattice consisting of
> - $L=\langleC,\leq\rangle$ is a (static) lattice consisting of
> - the classes set C,
> - the dominance relation $\leq$,
> - $Q=M\times CL$ is the state space where
@ -2265,7 +2260,7 @@ Interpretation
Given an exemplary BLP model where
- $S=\{s_1,s_2\}, O=\{o_1,o_2\}$
- $C=\{public,confidential\}$
- $\leq=\{⟨public,confidential⟩\}$
- $\leq=\{\langlepublic,confidential\rangle\}$
- $cl(s_1)=cl(o_1)=public$, $cl(s_2)=cl(o_2)=confidential$
- ![](Assets/Systemsicherheit-lattice-vs-acm.png)
- Observation: L and m are isomorphic $\rightarrow$ redundancy?
@ -2295,10 +2290,10 @@ Consequence: If we can prove this property for a given model, then its implement
##### BLP Security
Help Definitions
> Read-Security Rule
> A BLP model state $⟨m,cl⟩$ is called read-secure iff $\forall s\in S,o\in O:read\in m(s,o)\Rightarrow cl(o) \leq cl(s)$.
> A BLP model state $\langlem,cl\rangle$ is called read-secure iff $\forall s\in S,o\in O:read\in m(s,o)\Rightarrow cl(o) \leq cl(s)$.
> Write-Security Rule
> A BLP model state $⟨m,cl⟩$ is called write-secure iff $\forall s\in S,o\in O:write\in m(s,o)\Rightarrow cl(s)\leq cl(o)$.
> A BLP model state $\langlem,cl\rangle$ is called write-secure iff $\forall s\in S,o\in O:write\in m(s,o)\Rightarrow cl(s)\leq cl(o)$.
Note: In some literature, read-security is called "simple security", while write-security is called "^*-property". Reasons are obscure-historical.
@ -2321,9 +2316,9 @@ Auxiliary Definition: The Basic Security Theorem for BLP (BLP BST)
> The BLP Basic Security Theorem
>
> A BLP model $⟨S,O,L,Q,\sum,\sigma,q_0,R⟩$ is secure iff both of the following holds:
> A BLP model $\langleS,O,L,Q,\sum,\sigma,q_0,R\rangle$ is secure iff both of the following holds:
> 1. $q_0$ is secure
> 2. $\sigma$ is build such that for each state q reachable from $q_0$ by a finite input sequence, where $q=⟨m,cl⟩$ and $q′=\sigma(q,\delta)=m′,cl′,\forall s\in S, o\inO,\delta\in\sum$ the following holds:
> 2. $\sigma$ is build such that for each state q reachable from $q_0$ by a finite input sequence, where $q=\langlem,cl\rangle$ and $q′=\sigma(q,\delta)=m′,cl′,\forall s\in S, o\inO,\delta\in\sum$ the following holds:
> - Read-security conformity:
> - read $\not\in m(s,o)\wedge read\in m′(s,o)\Rightarrow cl′(o)\leq cl′(s)$
> - read $\in m(s,o) \wedge\lnot (cl′(o)\leq cl′(s)) \Rightarrow read \not\in m′(s,o)$
@ -2333,7 +2328,7 @@ Auxiliary Definition: The Basic Security Theorem for BLP (BLP BST)
Proof of Read Security
- Technique: Term rewriting
Let $q=\sigma*(q_0 ,\sigma^+),\sigma^+\in\sigma^+,q′=\delta(q,\sigma),\sigma\in\sigma,s\in S,o\in O$. With $q=⟨m,cl⟩$ and $q′=m′,cl′$, the BLP BST for read-security is
Let $q=\sigma*(q_0 ,\sigma^+),\sigma^+\in\sigma^+,q′=\delta(q,\sigma),\sigma\in\sigma,s\in S,o\in O$. With $q=\langlem,cl\rangle$ and $q′=m′,cl′$, the BLP BST for read-security is
- (a1) $read \not\in m(s,o) \wedge read\in m′(s,o) \Rightarrow cl′(o) \leq cl′(s)$
- (a2) $read \in m(s,o) \wedge\lnot (cl′(o)\leq cl′(s)) \Rightarrow read \not\in m′(s,o)$
- Let’s first introduce some convenient abbreviations for this:
@ -2356,10 +2351,10 @@ Idea: Encode an additional, more fine-grained type of access restriction in the
- Comp: set of compartments
- $co:S\cup O\rightarrow 2^{Comp}$: assigns a set of compartments to an entity as an (additional) attribute
- Refined state security rules:
- $⟨m,cl,co⟩$ is read-secure $\Leftrightarrow\forall s\in S,o\in O:read \in m(s,o)\Rightarrow cl(o)\leq cl(s)\wedge co(o) \subseteq co(s)$
- $⟨m,cl,co⟩$ is write-secure $\Leftrightarrow\forall s\in S,o\in O:write\in m(s,o)\Rightarrow cl(s)\leq cl(o)\wedge co(o) \subseteq co(s)$
- Good ol’ BLP: $⟨S,O,L,Q,\sigma,\delta,q_0⟩$
- With compartments: $⟨S,O,L,Comp,Q_{co},\sigma,\delta,q_0⟩ where $Q_{co}=M\times CL\times CO$ and $CO=\{co|co:S\cup O\rightarrow 2^{Comp}\}$
- $\langlem,cl,co\rangle$ is read-secure $\Leftrightarrow\forall s\in S,o\in O:read \in m(s,o)\Rightarrow cl(o)\leq cl(s)\wedge co(o) \subseteq co(s)$
- $\langlem,cl,co\rangle$ is write-secure $\Leftrightarrow\forall s\in S,o\in O:write\in m(s,o)\Rightarrow cl(s)\leq cl(o)\wedge co(o) \subseteq co(s)$
- Good ol’ BLP: $\langleS,O,L,Q,\sigma,\delta,q_0\rangle$
- With compartments: $\langleS,O,L,Comp,Q_{co},\sigma,\delta,q_0\rangle where $Q_{co}=M\times CL\times CO$ and $CO=\{co|co:S\cup O\rightarrow 2^{Comp}\}$
Example
- Let $co(o)=secret,co(o)=airforce$
@ -2427,8 +2422,6 @@ Windows Vista UAC
- Consequence: every file, process, ... created by the web browser is classified low $\rightarrow$ cannot violate integrity of system- and user-objects
- Manual user involvement ($\rightarrow$ DAC portion of the policy):resolving intended exceptions, e. g. to install trusted application software
### Non-interference Models
Problem No. 1: Covert Channels
@ -2484,7 +2477,7 @@ $\rightarrow$ NI Model Abstractions:
- Effects of actions on domains defined by a mapping $dom:A\rightarrow 2^D$
> NI Security Model
> An NI model is a det. automaton $⟨Q,\sigma,\delta,\lambda,q_0,D,A,dom,≈_{NI},Out⟩$ where
> An NI model is a det. automaton $\langleQ,\sigma,\delta,\lambda,q_0,D,A,dom,≈_{NI},Out\rangle$ where
> - Q is the set of (abstract) states,
> - $\sigma=A$ is the input alphabet where A is the set of (abstract) actions,
> - $\delta:Q\times\sigma\rightarrow Q$ is the state transition function,
@ -2527,10 +2520,10 @@ Before we define what NI-secure is, assume we could remove all actions from an a
> NI Security
>
> For a state $q\in Q$ of an NI model $⟨Q,\sigma,\delta,\lambda,q_0,D,A,dom,≈_{NI},Out⟩$, the predicate ni-secure(q) holds iff $\forall a\in A,\forall a^*\in A^*:\lambda (\delta^*(q,a^*),a)=\lambda(\delta^*(q,purge(a^*,dom(a))),a)$
> For a state $q\in Q$ of an NI model $\langleQ,\sigma,\delta,\lambda,q_0,D,A,dom,≈_{NI},Out\rangle$, the predicate ni-secure(q) holds iff $\forall a\in A,\forall a^*\in A^*:\lambda (\delta^*(q,a^*),a)=\lambda(\delta^*(q,purge(a^*,dom(a))),a)$
Interpretation
1. Running an NI model on $⟨q,a^*⟩$ yields $q′=\delta^*(q,a^*)$.
1. Running an NI model on $\langleq,a^*\rangle$ yields $q′=\delta^*(q,a^*)$.
2. Running the model on the purged input sequence so that it contains only actions that, according to $≈_{NI}$, actually have impact on $dom(a)$ yields $q′_{clean}=\delta^*(q,purge(a^*,dom(a)))$
3. If $\forall a\in A:\lambda(q′,a)=\lambda(q′_{clean},a)$, than the model is called NI-secure w.r.t. q($ni-secure(q)$).
@ -2592,22 +2585,22 @@ Example
Representation of Conflict Classes
- Client company data: object set O
- Competition: conflict relation $C\subseteq O\times O:⟨o,o′⟩\in C\Leftrightarrow o$ and $o′$ belong to competing companies (non-reflexive, symmetric, generally not transitive)
- In terms of ABAC:object attribute $att_O:O\rightarrow 2^O$, such that $att_O(o)=\{o′\in O|⟨o,o′⟩\in C\}$.
- Competition: conflict relation $C\subseteq O\times O:\langleo,o′\rangle\in C\Leftrightarrow o$ and $o′$ belong to competing companies (non-reflexive, symmetric, generally not transitive)
- In terms of ABAC:object attribute $att_O:O\rightarrow 2^O$, such that $att_O(o)=\{o′\in O|\langleo,o′\rangle\in C\}$.
Representation of a Consultant’s History
- Consultants: subject set S
- History relation $H\subseteq S\times O:⟨s,o⟩\in H\Leftrightarrow s$ has previously consulted $o$
- In terms of ABAC: subject attribute $att_S:S\rightarrow 2^O$, such that $att_S(s)=\{o\in O|⟨s,o⟩\in H\}$.
- History relation $H\subseteq S\times O:\langles,o\rangle\in H\Leftrightarrow s$ has previously consulted $o$
- In terms of ABAC: subject attribute $att_S:S\rightarrow 2^O$, such that $att_S(s)=\{o\in O|\langles,o\rangle\in H\}$.
> Brewer-Nash Security Model
>
> The Brewer-Nash model of the CW policy is a det. $automaton⟨S,O,Q,\sigma,\delta,q_0,R⟩$ where
> The Brewer-Nash model of the CW policy is a det. $automaton\langleS,O,Q,\sigma,\delta,q_0,R\rangle$ where
> - $S$ and $O$ are sets of subjects (consultants) and (company data) objects,
> - $Q=M\times 2^C\times 2^H$ is the state space where
> - $M=\{m|m:S\times O\rightarrow 2^R\}$ is the set ofpossible ACMs,
> - $C\subseteq O\times O$ is the conflict relation: $⟨o,o′⟩\in C\Leftrightarrow o$ and $o′$ are competitors,
> - $H\subseteq S\times O$ is the history relation: $⟨s,o⟩\in H\Leftrightarrow s$ has previously
> - $C\subseteq O\times O$ is the conflict relation: $\langleo,o′\rangle\in C\Leftrightarrow o$ and $o′$ are competitors,
> - $H\subseteq S\times O$ is the history relation: $\langles,o\rangle\in H\Leftrightarrow s$ has previously
consulted $o$,
> - $\sigma=OP \times X$ is the input alphabet where
> - $OP=\{read,write\}$ is a set of operations,
@ -2618,26 +2611,26 @@ consulted $o$,
![](Assets/Systemsicherheit-brewer-example-2.png)
At the time depicted:
- Conflict relation: $C=\{⟨HSBC,DB⟩,⟨HSBC,Citi⟩,⟨DB,Citi⟩,⟨Shell,Esso⟩\}$
- History relation: $H=\{⟨Ann,DB⟩,⟨Bob,Citi⟩,⟨Bob,Esso⟩\}$
- Conflict relation: $C=\{\langleHSBC,DB\rangle,\langleHSBC,Citi\rangle,\langleDB,Citi\rangle,\langleShell,Esso\rangle\}$
- History relation: $H=\{\langleAnn,DB\rangle,\langleBob,Citi\rangle,\langleBob,Esso\rangle\}$
##### Brewer-Nash STS
- Read (here: similar to HRU notation)
$command read(s,o)::=if read \in m(s,o) \wedge\forall ⟨o′,o⟩\in C:⟨s,o′⟩\not\in H$
$command read(s,o)::=if read \in m(s,o) \wedge\forall \langleo′,o\rangle\in C:\langles,o′\rangle\not\in H$
$then$
$H:=H\cup\{⟨s,o⟩\}$
$H:=H\cup\{\langles,o\rangle\}$
$fi$
- Write
$command write(s,o)::=if write \in m(s,o) \wedge\forall o′\in O:o'\not=o \Rightarrow ⟨s,o′⟩\not\in H$
$command write(s,o)::=if write \in m(s,o) \wedge\forall o′\in O:o'\not=o \Rightarrow \langles,o′\rangle\not\in H$
$then$
$H:=H\cup\{⟨s,o⟩\}$
$H:=H\cup\{\langles,o\rangle\}$
$fi$
Not shown: Discretionary policy portion $\rightarrow$ modifications in m to enable fine-grained rights management.
Restrictiveness
- Write Command: s is allowed to write $o\Leftrightarrow write\in m(s,o)\wedge\forall o′\in O:o′\not=o\Rightarrow⟨s,o′⟩\not\in H$
- Write Command: s is allowed to write $o\Leftrightarrow write\in m(s,o)\wedge\forall o′\in O:o′\not=o\Rightarrow\langles,o′\rangle\not\in H$
- Why so restrictive? $\rightarrow$ No transitive information flow!
- $\rightarrow$ s must never have previously consulted any other client!
- $\Rightarrow$ any consultant is stuck with her client on first read access
@ -2651,8 +2644,8 @@ Instantiation of a Model
- $H_0 =\varnothing$
> Secure State
> $\forall o,o′ \in O,s\in S:⟨s,o⟩\in H_q\wedge⟨s,o′⟩\in H_q\Rightarrow⟨o,o′⟩\not\in C_q$
> Corollary: $\forall o,o′\in O,s\in S:⟨o,o′⟩\in C_q\wedge⟨s,o⟩\in H_q\Rightarrow ⟨s,o′⟩\not\in H_q$
> $\forall o,o′ \in O,s\in S:\langles,o\rangle\in H_q\wedge\langles,o′\rangle\in H_q\Rightarrow\langleo,o′\rangle\not\in C_q$
> Corollary: $\forall o,o′\in O,s\in S:\langleo,o′\rangle\in C_q\wedge\langles,o\rangle\in H_q\Rightarrow \langles,o′\rangle\not\in H_q$
> Secure Brewer-Nash Model
> Similar to "secure BLP model".
@ -2689,7 +2682,7 @@ Professionalization
#### The Least-Restrictive-CW Model
Restrictiveness of Brewer-Nash Model:
- If $⟨o_i,o_k⟩\in C$: no transitive information flow $o_i \rightarrow o_j\rightarrow o_k$, i.e. consultant(s) of $o_i$ must never write to any $o_j\not=o_i$
- If $\langleo_i,o_k\rangle\in C$: no transitive information flow $o_i \rightarrow o_j\rightarrow o_k$, i.e. consultant(s) of $o_i$ must never write to any $o_j\not=o_i$
- This is actually more restrictive than necessary: $o_j\rightarrow o_k$ and afterwards $o_i\rightarrow o_j$ would be fine! (no information can actually flow from $o_i$ to $o_k$)
- In other words: Criticality of an IF depends on existence of earlier flows.
@ -2701,12 +2694,12 @@ Approach:
> LR-CW Model
>
> The Least-Restrictive model of the CW policy is a deterministic $automaton ⟨S,O,F,\zeta,Q,\sigma,\delta,q_0⟩$ where
> The Least-Restrictive model of the CW policy is a deterministic $automaton \langleS,O,F,\zeta,Q,\sigma,\delta,q_0\rangle$ where
> - S and O are sets of subjects (consultants) and data objects,
> - F is the set of client companies,
> - $\zeta:O\rightarrow F$ ("zeta") is a function mapping each object to its company,
> - $Q=2^C \times 2^H$ is the state space where
> - $C\subseteq F\times F$ is the conflict relation: $⟨f,f′⟩\in C\Leftrightarrow f$ and $f′$ are competitors,
> - $C\subseteq F\times F$ is the conflict relation: $\langlef,f′\rangle\in C\Leftrightarrow f$ and $f′$ are competitors,
> - $H=\{Z_e\subseteq F|e\in S\cup O\}$ is the history set: $f\in Z_e\Leftrightarrow e$ contains information about $f(Z_e$ is the "history label" of $e$),
> - $\sigma=OP\times X$ is the input alphabet where
> - $OP=\{read,write\}$ is the set of operations,
@ -2725,10 +2718,10 @@ Approach:
Inside the STS
- a reading operation
- requires that no conflicting information is accumulated in the subject potentially increases the amount of information in the subject
- command read(s,o) ::= if $\forall f,f′\in Z_s \cup Z_o:⟨f,f′⟩\not\in C$ then $Z_s:=Z_s\cup Z_o$ fi
- command read(s,o) ::= if $\forall f,f′\in Z_s \cup Z_o:\langlef,f′\rangle\not\in C$ then $Z_s:=Z_s\cup Z_o$ fi
- a writing operation
- requires that no conflicting information is accumulated in the object potentially increases the amount of information in the object
- command write(s,o) ::= if $\forall f,f′\in Z_s\cup Z_o:⟨f,f′⟩\not\in C$ then $Z_o:=Z_o\cup Z_s$ fi
- command write(s,o) ::= if $\forall f,f′\in Z_s\cup Z_o:\langlef,f′\rangle\not\in C$ then $Z_o:=Z_o\cup Z_s$ fi
Model Achievements
- Applicability: more writes allowed in comparison to Brewer-Nash (note that this still complies with the general CW policy)
@ -2749,7 +2742,7 @@ Conflict relation is
- symmetric: competition is always mutual
- not necessarily transitive: any company might belong to more than one conflict class $\Rightarrow$ if a competes with b and b competes with c, then a and c might still be in different conflict classes (= no competitors) $\rightarrow$ Cannot be modeled by a lattice!
Reminder:In a lattice$⟨C,\leq⟩$,$\leq$ is a partial order:
Reminder:In a lattice$\langleC,\leq\rangle$,$\leq$ is a partial order:
1. reflexive $(\forall a\in C:a \leq a)$
2. anti-symmetric $(\forall a,b \in C:a \leq b \wedge b \leq a\Rightarrow a=b)$
3. transitive $(a,b,c \in C:a \leq b \wedge b \leq c \Rightarrow a \leq c)$
@ -2815,37 +2808,37 @@ What we have
![](Assets/Systemsicherheit-model-family.png)
In Formal Words ...
- HRU: $⟨ Q, \sum , \delta, q_0 , R ⟩$
- $DRBAC_0$ : $⟨ Q, \sum , \delta, q_0 , R, P, PA ⟩$
- DABAC: $⟨ A , Q ,\sum , \delta, q_0 ⟩$
- TAM: $⟨ Q , \sum , \delta, q_0 , T, R ⟩$
- BLP: $⟨ S, O, L, Q , \sum , \delta, q_0 , R ⟩$
- NI: $⟨ Q , \sum , \delta, \lambda ,q_0 , D, A, dom, =_{NI} , Out ⟩$
- HRU: $\langle Q, \sum , \delta, q_0 , R \rangle$
- $DRBAC_0$ : $\langle Q, \sum , \delta, q_0 , R, P, PA \rangle$
- DABAC: $\langle A , Q ,\sum , \delta, q_0 \rangle$
- TAM: $\langle Q , \sum , \delta, q_0 , T, R \rangle$
- BLP: $\langle S, O, L, Q , \sum , \delta, q_0 , R \rangle$
- NI: $\langle Q , \sum , \delta, \lambda ,q_0 , D, A, dom, =_{NI} , Out \rangle$
Core Model (Common Model Core)
- HRU: $⟨ Q, \sum , \delta, q_0 , \not R ⟩$
- $DRBAC_0$ : $⟨ Q, \sum , \delta, q_0 , \not R, \not P, \not PA ⟩$
- DABAC: $⟨ \not A , Q ,\sum , \delta, q_0 ⟩$
- TAM: $⟨ Q , \sum , \delta, q_0 , \not T, \not R ⟩$
- BLP: $⟨ \not S, \not O, \not L, Q , \sum , \delta, q_0 , \not R ⟩$
- NI: $⟨ Q , \sum , \delta, \not \lambda ,q_0 , \not D, \not A, \not dom, \not =_{NI} , \not Out ⟩$
- $\rightarrow ⟨ Q ,\sum , \delta, q_0 ⟩$
- HRU: $\langle Q, \sum , \delta, q_0 , \not R \rangle$
- $DRBAC_0$ : $\langle Q, \sum , \delta, q_0 , \not R, \not P, \not PA \rangle$
- DABAC: $\langle \not A , Q ,\sum , \delta, q_0 \rangle$
- TAM: $\langle Q , \sum , \delta, q_0 , \not T, \not R \rangle$
- BLP: $\langle \not S, \not O, \not L, Q , \sum , \delta, q_0 , \not R \rangle$
- NI: $\langle Q , \sum , \delta, \not \lambda ,q_0 , \not D, \not A, \not dom, \not =_{NI} , \not Out \rangle$
- $\rightarrow \langle Q ,\sum , \delta, q_0 \rangle$
Core Specialization
- HRU: $⟨ Q, \sum , \delta, q_0 , R ⟩ \Rightarrow Q = 2^S \times 2^O \times M$
- $DRBAC_0$ : $⟨ Q, \sum , \delta, q_0 , R, P, PA ⟩ \Rightarrow Q = 2^U\times 2^{UA}\times 2^S \times USER \times ROLES$
- DABAC: $⟨ A , Q ,\sum , \delta, q_0 ⟩ \Rightarrow Q = 2^S\times 2^O \times M\times ATT$
- TAM: $⟨ Q , \sum , \delta, q_0 , T, R ⟩ \Rightarrow Q = 2^S\times 2^O\times TYPE \times M$
- BLP: $⟨ S, O, L, Q , \sum , \delta, q_0 , R ⟩ \Rightarrow Q = M \times CL$
- NI: $⟨ Q , \sum , \delta, \lambda ,q_0 , D, A, dom, =_{NI} , Out ⟩$
- HRU: $\langle Q, \sum , \delta, q_0 , R \rangle \Rightarrow Q = 2^S \times 2^O \times M$
- $DRBAC_0$ : $\langle Q, \sum , \delta, q_0 , R, P, PA \rangle \Rightarrow Q = 2^U\times 2^{UA}\times 2^S \times USER \times ROLES$
- DABAC: $\langle A , Q ,\sum , \delta, q_0 \rangle \Rightarrow Q = 2^S\times 2^O \times M\times ATT$
- TAM: $\langle Q , \sum , \delta, q_0 , T, R \rangle \Rightarrow Q = 2^S\times 2^O\times TYPE \times M$
- BLP: $\langle S, O, L, Q , \sum , \delta, q_0 , R \rangle \Rightarrow Q = M \times CL$
- NI: $\langle Q , \sum , \delta, \lambda ,q_0 , D, A, dom, =_{NI} , Out \rangle$
Core Extensions
- HRU: $⟨ Q, \sum , \delta, q_0 , R ⟩ \Rightarrow R$
- $DRBAC_0$ : $⟨ Q, \sum , \delta, q_0 , R, P, PA ⟩ \Rightarrow R,P,PA$
- DABAC: $⟨ A , Q ,\sum , \delta, q_0 ⟩ \Rightarrow A$
- TAM: $⟨ Q , \sum , \delta, q_0 , T, R ⟩ \Rightarrow T,R$
- BLP: $⟨ S, O, L, Q , \sum , \delta, q_0 , R ⟩ \Rightarrow S,O,L,R$
- NI: $⟨ Q , \sum , \delta, \lambda ,q_0 , D, A, dom, =_{NI} , Out ⟩ \Rightarrow \lambda,D,A,dom,=_{NI},Out$
- HRU: $\langle Q, \sum , \delta, q_0 , R \rangle \Rightarrow R$
- $DRBAC_0$ : $\langle Q, \sum , \delta, q_0 , R, P, PA \rangle \Rightarrow R,P,PA$
- DABAC: $\langle A , Q ,\sum , \delta, q_0 \rangle \Rightarrow A$
- TAM: $\langle Q , \sum , \delta, q_0 , T, R \rangle \Rightarrow T,R$
- BLP: $\langle S, O, L, Q , \sum , \delta, q_0 , R \rangle \Rightarrow S,O,L,R$
- NI: $\langle Q , \sum , \delta, \lambda ,q_0 , D, A, dom, =_{NI} , Out \rangle \Rightarrow \lambda,D,A,dom,=_{NI},Out$
- $\rightarrow R, P, PA, A , T , S , O , L , D , dom , =_{NI} , ...$
Glue
@ -2955,8 +2948,8 @@ Tools
##### Example: Specification of a DRBAC_0 Model
$DRBAC_0 = RBAC_0 + Automaton \rightarrow$
$RBAC_0 = ⟨ U , R , P , S , UA , PA , user , roles ⟩$
$DRBAC_0 = ⟨ Q , \sum, \delta, q_0 , R , P , PA ⟩$
$RBAC_0 = \langle U , R , P , S , UA , PA , user , roles \rangle$
$DRBAC_0 = \langle Q , \sum, \delta, q_0 , R , P , PA \rangle$
$Q = 2^U \times 2^S \times 2^{UA}\times ...$
Policy Specification in EBNF
@ -4449,7 +4442,7 @@ Principal Architecture Components
- Based on key shared between TGS and respective server
- Result: ticket(s) for server(s)
- Kerberos database
- Contains for each user and server a mapping $⟨user, server⟩\rightarrow$ authentication key
- Contains for each user and server a mapping $\langleuser, server\rangle\rightarrow$ authentication key
- Used by AS
- Is multiply replicated (availability, scalability)
@ -4542,7 +4535,7 @@ Authentication (bidirectional)
- This can only be a server that can extract the session key from the ticket $Ticket_{Alice/Server}=\{Alice,Server ,..., SessionKey_{Alice/Server}\}_{K_{TGS/Server}}$
Getting a Ticket for a Server
- Are valid for a pair ⟨client, server⟩
- Are valid for a pair \langleclient, server\rangle
- Are issued (but for TGS-Ticket itself) only by TGS
- Ticket request to TGS: $(server, TGS ticket, authenticator)$