From f9b917e3135b27caf54d4e595e30cbe7ece935ae Mon Sep 17 00:00:00 2001 From: Andrew Guschin Date: Tue, 6 Aug 2024 23:54:54 +0400 Subject: =?UTF-8?q?=D0=9B=D0=B5=D0=BA=D1=86=D0=B8=D0=B8=20=D0=BF=D0=BE=20?= =?UTF-8?q?=D0=BC=D0=BE=D0=B4=D0=B5=D0=BB=D1=8F=D0=BC=20=D0=B1=D0=B5=D0=B7?= =?UTF-8?q?=D0=BE=D0=BF=D0=B0=D1=81=D0=BD=D0=BE=D1=81=D1=82=D0=B8=20=D0=B8?= =?UTF-8?q?=20=D0=BC=D0=B5=D1=82=D0=BE=D0=B4=D0=B0=D0=BC=20=D0=B0=D0=BB?= =?UTF-8?q?=D0=B3=D0=B5=D0=B1=D1=80=D0=B0=D0=B8=D1=87=D0=B5=D1=81=D0=BA?= =?UTF-8?q?=D0=BE=D0=B9=20=D0=B3=D0=B5=D0=BE=D0=BC=D0=B5=D1=82=D1=80=D0=B8?= =?UTF-8?q?=D0=B8?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit --- security-models/lectures/lecture10.tex | 131 ++++++++++++++++++++ security-models/lectures/lecture12.tex | 218 +++++++++++++++++++++++++++++++++ security-models/lectures/lecture4.tex | 159 ++++++++++++++++++++++++ security-models/lectures/lecture5.tex | 2 + security-models/lectures/lecture6.tex | 182 +++++++++++++++++++++++++++ security-models/lectures/lecture7.tex | 65 ++++++++++ security-models/lectures/lecture8.tex | 148 ++++++++++++++++++++++ security-models/lectures/lecture9.tex | 2 + security-models/security-models.pdf | Bin 186791 -> 330655 bytes security-models/security-models.tex | 11 ++ 10 files changed, 918 insertions(+) create mode 100644 security-models/lectures/lecture10.tex create mode 100644 security-models/lectures/lecture12.tex create mode 100644 security-models/lectures/lecture4.tex create mode 100644 security-models/lectures/lecture5.tex create mode 100644 security-models/lectures/lecture6.tex create mode 100644 security-models/lectures/lecture7.tex create mode 100644 security-models/lectures/lecture8.tex create mode 100644 security-models/lectures/lecture9.tex (limited to 'security-models') diff --git a/security-models/lectures/lecture10.tex b/security-models/lectures/lecture10.tex new file mode 100644 index 0000000..3a0a0d7 --- /dev/null +++ b/security-models/lectures/lecture10.tex @@ -0,0 +1,131 @@ +% Лекция 10 (24.11.23) + +%% NOTE: 2.3 + +Устовия применения де-факто правил в исходном состоянии $G = (S, O, E \cup F)$ +и результаты их применения в результирующем состоянии $G' = (S, O, E \cup F')$ +приведены в таблице. + +%% TODO: таблица 1 - Де-факто правила расширенной модели Take-Grant + +\begin{table}[H] + \smallsize + \centering + \caption{} + \begin{tabular}{|c|p{6cm}|p{6cm}|} + \hline + Правило & + Исходное состояние $G = (S, O, E \cup F)$ & + Результирующее состояние $G' = (S, O, E \cup F')$ \\ \hline + + Первое правило & + $x \in S; y \in O; (x, y, r) \in E \cup F$ & + $F' = F \cup \set{(y, x, w), (x, y, r)}$ \\ \hline + + Второе правило & + $x \in S; y \in O; (x, y, w) \in E \cup F$ & + $F' = F \cup \set{(y, x, r), (x, y, w)}$ \\ \hline + + $\fn{spy}(x, y, z)$ & + $x, y \in S; x \neq z; \set{(x, y, r), (y, z, r)} \subset E \cup F$ & + $F' = F \cup \set{(x, z, r), (z, x, w)}$ \\ \hline + + $\fn{find}(x, y, z)$ & + $x, y \in S; z \in O; x \neq z; \set{(x, y, w), (y, z, w)} \subset E \cup F$ & + $F' = F \cup \set{(x, z, w), (z, x, r)}$ \\ \hline + + $\fn{post}(x, y, z)$ & + $x, z \in S; y \in O; x \neq z; \set{(x, y, r), (z, y, w)} \subset E \cup F$ & + $F' = F \cup \set{(x, z, r), (z, x, w)}$ \\ \hline + + $\fn{pass}(x, y, z)$ & + $y \in S; x, z \in O; x \neq z; \set{(y, x, w), (y, z, r)} \subset E \cup F$ & + $F' = F \cup \set{(x, z, r), (z, x, w)}$ \\ \hline + \end{tabular} +\end{table} + +Из определения де-факто правил следует, что для анализа информационных потоков +достаточно рассматривать потоки одного вида: либо на чтение, либо на запись. + +Будем рассматривать только информационные потоки на запись. Будем предполагать, +что при возникновении информационного потока не накладывается ограничений на +кооперацию субъектов системы, участвующих в этом процессе. + +Пусть $x, y \in O_0$, $x \neq y$, --- различные объекты графа доступов и +информационных потоков $G_0 = (S_0, O_0, E_0 \cup F_0)$. Определим предикат +$\fn{can_write}(x, y, G_0)$, который будет истинным $\iff$ $\exists$ графы $G_1 += (S_1, O_1, E_1 \cup F_1), \dots, G_N = (S_N, O_N, E_N \cup F_N)$ и де-юре +или де-факто правила $op_1, \dots, op_N$, где $N \geq 0$, такие, что $G_0 +\vdash_{op_1} G_1 \vdash_{op_2} \dots \vdash_{op_N} G_N$ и $(x, y, w) \subset +F_N$. + +%% NOTE: 2.8 +\begin{theorem} + Пусть $G_0 = (S_0, O_0, E_0 \cup F_0)$ --- граф доступов и информационных + потоков, $x, y \in O_0$, $x \neq y$. Тогда предикат $\fn{can_write}(x, y, G_0)$ + истинен $\iff$ существуют объекты $o_1, \dots, o_m \in O_0$, где $o_1 = x, + o_m = y$, такие, что или $m = 2$ и $(x, y, w) \in F_0$, или для $i = 1, \dots, + m - 1$ выполняется одно из трёх условий: + \begin{enumerate} + \item + $o_i \in S_0$ и или истинен предикат $\fn{can_share}(\set{w}, o_i, o_{i + + 1}, G_0)$, или $(o_i, o_{i + 1}, w) \in E_0 \cup F_0$; + \item + $o_{i + 1} \in S_0$ и или истинен предикат $\fn{can_share}(\set{r}, o_{i + + 1}, o_i, G_0)$, или $(o_{i + 1}, o_i, r) \in E_0 \cup F_0$; + \item + $o_i, o_{i + 1} \in S_0$ и или истинен предикат $\fn{can_share}(\alpha, + o_i, o_{i + 1}, G_0)$, или истинен предикат $\fn{cna_share}(\alpha, o_{i + + 1}, o_i, G_0)$, где $\alpha \in \set{t, g}$, или существует объект + $o_i' \in O_0$ такой, что либо истинны предикаты $\fn{can_share}(\set{t}, + o_i, o_i', G_0)$, $\fn{can_share}(\set{g}, o_{i + 1}, o_i', G_0)$, + либо истинны предикаты $\fn{can_share}(\set{g}, o_i, o_i', G_0)$, + $\fn{can_share}(\set{t}, o_{i + 1}, o_i', G_0)$. + \end{enumerate} + + \label{thm:2.8} +\end{theorem} + +\paragraph{Алгоритм построения замыкания графа доступов и информационных потоков.} + +Для проверки истинности предиката $\fn{can_share}(\alpha, x, y, G_0)$ или +$\fn{can_write}(x, y, G_0)$ для многих пар вершин неэффективно использовать +алгоритмы проверки условий теорем \ref{thm:2.6}, \ref{thm:2.8}. + +Эффективнее применять алгоритмы, позволяющие осуществлять проверку истинности +данных предикатов сразу для всех пар вершин. Такие алгоритмы реализуют +преобразование графа доступов и информационных потоков в его замыкание. + +Пусть $G = (S, O, E \cup F)$ --- граф доступов и информационных потоков такой, +что для каждого субъекта $s \in S$ существует объект $o \in O$ такой, что +выполняется условие $(s, o, \set{t, g, r, w}) \in E$. + +\emph{Замыканием} (или \emph{де-факто замыканием}) графа $G$ называется граф +доступов и информационных потоков $G^* = (S, O, E^* \cup F^*)$, полученный из +$G$ применением последовательности правил take, grant и де-факто правил. При +этом применение к графу $G^*$ указанных правил не приводит к появлению в нём +новых дуг. + +$tg$-замыканием графа $G$ называется граф доступов и информационных +потоков $G^{tg} = (S, O, E^{tg} \cup F)$, полученный из $G$ применением +последовательности правил take или grant. + +При этом каждое ребро $(o_1, o_2, \alpha) \in E^{tg} - E$ имеет вид $(o_1, o_2, +t)$ или $(o_1, o_2, g)$, и применение к графу $G^{tg}$ правил take или grant не +приводит к появлению в нём новых дуг указанного вида. + +\emph{Де-юре замыканием} графа $G$ называется граф доступов и информационных +потоков $G^\text{де-юре} = (S, O, E^\text{де-юре} \cup F)$, полученный из $G$ +применением последовательности правил take или grant. При этом применение в +графу $G^\text{де-юре}$ правил take или grant не приводит к появлению в нём +новых дуг. + +Алгоритм построения замыкания графа доступов состоит из трёх этапов: +\begin{enumerate} + \item построение $tg$-замыкания; + \item построение де-юре-замыкания; + \item построение замыкания. +\end{enumerate} + +Алгоритм построения $tg$-замыкания графа доступов и информационных потоков +$G = (S, O, E \cup F)$. diff --git a/security-models/lectures/lecture12.tex b/security-models/lectures/lecture12.tex new file mode 100644 index 0000000..8aad472 --- /dev/null +++ b/security-models/lectures/lecture12.tex @@ -0,0 +1,218 @@ +% Лекция 12 (04/08.12.23) + +%% NOTE: 3.1 +% \subsection{Модель Белла-ЛаПадулы} + +$M = \set{m_{|S| \times |O|}}$ --- множество возможных матриц доступов, где +$m_{|S| \times |O|}$ --- матрица доступов, $m[s, o] \subseteq R$ --- права +доступа субъекта $s$ к объекту $o$; + +$(f_s, f_o, f_c) \in F = L^S \times L^O \times L^S$ --- тройка функций +%% TODO: дописать + +\begin{itemize} + \item $V = B \times M \times F$ --- множество состояний системы; + \item $Q$ --- множество запросов системе; + \item + $D$ --- множество ответов по запросам, например, $D = \set{yes, no, error}$; + \item + $W \subseteq Q \times D \times V \times V$ --- множество действий системы, + где $(q, d, v^*, v) \in W$, означает, что системы по запросу $q$ с ответом + $d$ перешла из состояния $v$ в состояние $v^*$; + \item + $\NN_0 = \set{0, 1, 2, \dots}$ --- множество значений времени; + \item + $X$ --- множество функций $x : \NN_0 \to Q$, задающих все возможные + последовательности запросов к системе; + \item + $Y$ --- множество функций $y : \NN_0 \to D$, задающих все возможные + последовательности ответов системы по запросам; + \item + $Z$ --- множество функций $z : \NN_0 \to V$, задающих все возможные + последовательности состояний системы. +\end{itemize} + +$\Sigma (Q, D, W, z_0) \subseteq X \times Y \times Z$ называется \emph{системой}, +когда для каждого $(x, y, z) \in \Sigma (Q, D, W, z_0)$ выполняется условие: +для $t \in \NN_0 \; (x_t, y_t, z_{t + 1}, z_t) \in W$, где $z_0$ --- начальное +состояние системы. + +При этом каждый набор $(x, y, z) \in \Sigma (Q, D, W, z_0)$ называется +\emph{реализацией} системы, а $(x_t, y_t, z_{t + 1}, z_t) \in W$ --- +\emph{действием} системы в момент времени $t \in \NN_0$. + +В классической модели Белла-ЛаПадулы рассматриваются следующие запросы, входящие +в множество $Q$: +\begin{enumerate} + \item запросы изменения множества текущих доступов $b$; + \item запросы изменения функций $f$; + \item запросы изменения прав доступа в матрице $m$. +\end{enumerate} + +Следующий список описывает изменения каждого элемента состояния системы. +Конкретное решение по запросу включает возможность производить следующие +изменения в состоянии системы. +\begin{enumerate} + \item + Изменение текущих доступов: + \begin{enumerate} + \item + получить доступ (добавить тройку (субъект, объект, вид доступа) в + текущее множество доступов $b$); + \item + отменить доступ (удалить аналогично). + \end{enumerate} + \item + Изменение значений функций уровней конфиденциальности и доступа: + \begin{enumerate} + \item изменить уровень конфиденциальности объекта; + \item изменить уровень доступа субъекта. + \end{enumerate} + \item + Изменение прав доступа: + \begin{enumerate} + \item + дать разрешение на доступ (добавить право доступа в соответствующий + элемент матрицы доступов $m$); + \item + отменить разрешение на доступ (удалить аналогично). + \end{enumerate} +\end{enumerate} + +Безопасность системы определяется с помощью трёх свойств: +\begin{itemize} + \item + ss --- свойства простой безопасности (simple security, безопасность по + чтению); + \item + * --- свойства <<звезда>> (безопасность по записи); + \item + ds --- свойства дискреционной безопасности (discretionary security, + безопасность (разрешённость) по матрице доступа). +\end{itemize} + +Доступ $(s, o, r) \in S \times O \times R$ обладает ss-свойством относительно +$f = (f_s, f_o, f_c) \in F$, когда выполняется одно из условий: +\begin{enumerate} + \item $r \in \set{execute, append}$; + \item $r \in {read, write} \land f_s(s) \geq f_o(o)$. +\end{enumerate} + +Состояние системы $(b, m, f) \in V$ обладает ss-свойством, когда каждый элемент +$(s, o, r) \in b$ обладает ss-свойством относительно $f$. + +Доступ $(s, o, r) \in S \times O \times R$ обладает *-свойством относительно +$f = (f_s, f_o, f_c) \in F$, когда выполняется одно из условий: +\begin{enumerate} + \item $r = execute$; + \item $r = append \land f_o(o) \geq f_c(s)$; + \item $r = read \land f_c(s) \geq f_o(o)$; + \item $r = write \land f_c(s) = f_o(o)$. +\end{enumerate} + +Состояние системы $(b, m, f) \in V$ обладает *-свойством, когда каждый элемент +$(s, o, r) \in b$ обладает *-свойством относительно $f$. + +Состояние системы $(b, m, f) \in V$ обладает *-свойством относительно +подмножества $S' \subseteq S$, когда каждый элемент $(s, o, r) \in b$, где +$s \in S'$, обладает *-свойством относительно $f$. + +При этом $S \backslash S'$ называется \emph{множеством доверенных субъектов}, +то есть субъектов, имеющих право нарушать требования *-свойства. + +Состояние системы $(b, m, f) \in V$ обладает ds-свойством, когда для каждого +доступа $(s, o, r) \in b$ выполняется условие $r \in m[s, o]$. + +Состояние системы $(b, m, f)$ называется \emph{безопасным}, когда оно обладает +*-свойством относительно $S'$, ss-свойством и ds-свойством. + +Реализация системы $(x, y, z) \in \Sigma (Q, D, W, z_0)$ обладает ss-свойством +(*-свойством, ds-свойством), когда в последовательности $(z_0, z_1, \dots)$ +каждое состояние обладает ss-свойством (*-свойством, ds-свойством). + +Система $\Sigma (Q, D, W, z_0)$ обладает ss-свойством (*-свойством, ds-свойством), +когда каждая её реализация обладает ss-свойством (*-свойством, ds-свойством). + +Система $\Sigma (Q, D, W, z_0)$ нащывается \emph{безопасной}, когда она обладает +ss-свойством, *-свойством, ds-свойством одновременно. + +Описанные свойства можно пояснить следующим образом: +\begin{enumerate} + \item + из обладания доступом *-свойством относительно $f$ следует обладание этим + доступом ss-свойством относительно $f$; + \item + из обладания ss-свойством следует, что в модели Белла-ЛаПадулы выполняется + запрет на чтение вверх, требуемый мандатной политикой безопасности. + + Кроме того, ss-свойство не допускает модификацию с использованием доступа + write, когда $f_s(s) < f_o(o)$. + + Таким образом, функция $f_s(s)$ задаёт для субъекта $s$ верхний уровень + конфиденциальности объектов, к которым он потенциально может получить доступ + read или write; + \item + если субъект $s$ может понизить свой текущий уровень доступа до $f_c(s) = + f_o(o)$, то он может получить доступ write к объекту $o$, но не доступ + read к объектам $o'$, чей уровень $f_o(o') > f_c(s)$. + + Хотя при этом, возможно, справедливо неравенство $f_s(s) \geq f_o(o')$, и + в каких-то других состояниях системы субъект $s$ может получить доступ + read к объекту $o'$. + + Таким образом, *-свойство исключает появление в системе запрещённого + информационного потока <<сверху вниз>> и соответствует требованиям мандатной + политики безопасности (см. рис. 3.1). + + %% TODO: рис 1 (3.1): Иллюстрация *-свойства +\end{enumerate} + +%% NOTE: 3.1 +\begin{theorem} + Система $\Sigma(Q, D, W, z_0)$ обладает ss-свойством для любого начального + состояния $z_0$, обладающего ss-свойством $\iff$ для каждого действия + $(q, d, (b^*, m^*, f^*), (b, m, f)) \in W$ выполняется два условия: + \begin{enumerate} + \item + каждый доступ $(s, o, r) \in b^* \backshash b$ обладает ss-свойством + относительно $f^*$; + \item + если $(s, o, r) \in b$ и не обладает ss-свойством относительно $f^*$, + то $(s, o, r) \not\in b^*$. + \end{enumerate} +\end{theorem} + +\begin{theorem} + Система $\Sigma(Q, D, W, z_0)$ обладает *-свойством относительно $S' \subseteq S$ + для любого начального состояния $z_0$, обладающего *-свойством относительно + $S'$ $\iff$ для каждого действия $(q, d, (b^*, m^*, f^*), (b, m, f)) \in W$ + выполняются два условия: + \begin{enumerate} + \item + для $s \in S'$ доступ $(s, o, r) \in b^* \backslash b$ обладает *-свойством + относительно $f^*$; + \item + для $s \in S'$, если $(s, o, r) \in b$ и не обладает *-свойством + относительно $f^*$, то $(s, o, r) \not\in b^*$. + \end{enumerate} +\end{theorem} + +\begin{theorem} + Система $\Sigma(Q, D, W, z_0)$ обладает ds-свойством для любого начального + состояния $z_0$, обладающего ds-свойством $\iff$ для каждого действия + $(q, d, (b^*, m^*, f^*), (b, m, f)) \in W$ выполняется два условия: + \begin{enumerate} + \item + для каждого $(s, o, r) \in b^* \backslash b$ выполняется условие + $r \in m^*[s, o]$; + \item + если доступ $(s, o, r) \in b \land r \not\in m^*[s, o] \implies (s, o, r) + \not\in b^*$. + \end{enumerate} +\end{theorem} + +%% NOTE: 3.4 +\begin{theorem}[Базовая теорема безопасности] + Система $\Sigma(Q, D, W, z_0)$ безопасна для безопасного $z_0$ $\iff$ + множество действий системы $W$ удовлетворяет условиям теорем 3.1 -- 3.3. +\end{theorem} diff --git a/security-models/lectures/lecture4.tex b/security-models/lectures/lecture4.tex new file mode 100644 index 0000000..aefcb56 --- /dev/null +++ b/security-models/lectures/lecture4.tex @@ -0,0 +1,159 @@ +% Лекция 4 (13.10.23) + +\subsection{Модель типизированной матрицы доступов} + +Дискреционная модель, получившая название <<типизированная матрица доступов>> +(ТМД), представляет собой развитие модели ХРУ, дополненной концепцией типов, +что позволяет несколько смягчить те условия, для которых возможно доказательство +безопасности системы. + +Формальное описание модели включает в себя следующие элементы: +\begin{itemize} + \item $O$ --- множество объектов системы; + \item $S$ --- множество субъектов системы ($S \subseteq O$); + \item $R$ --- множество прав доступа субъектов к объектам; + \item $M$ --- матрица доступов; + \item $C$ --- множество команд; + \item $T$ --- множество типов объектов; + \item $t: O \to T$ --- функция, ставящая в соответствие каждому объекту его тип; + \item $q = (S, O, t, M)$ --- состояние системы; + \item $Q$ --- множество состояний системы. +\end{itemize} + +Состояния системы изменяются в результате применения к ним команд множества $C$. + +\begin{align*} + comm&and c(x_1 : t_1, \dots, x_k : t_k) \\ + &if (r_1 \in M[x_{s_1}, x_{o_1} and \dots and r_m \in M[x_{s_m}, x_{o_m}]) then \\ + & a_1; \\ + & \dots \\ + & a_n; \\ + &endif \\ + & end. +\end{align*} + +Перед выполнением команды происходит проверка типов фактических параметров, и, +если они не совпадают с указанными в определении команды, то команда не +выполняется. + +В модели ТМД используются 6 видов примитивных операторов, отличающихся от +аналогичных операторов модели ХРУ только использованием типизированных +параметров. + +%% TODO: таблица +Примитивный оператор / Исходное состояние $q = (S, O, t, M)$ / Результирующее состояние $q' = (S', O', t', M')$ +<<внести>> право $r$ в $M[s, o]$ / $s \in S, o \in O, r \in R$ / $S' = S, O' = O, t' = t, M'[s, o] = M[s, o] \cup \set{r}$, если $(s', o') \neq (s, o)$, то $M'[s', o'] = M[s', o']$. +<<удалить>> право $r$ из $M[s, o]$ / $s \in S, o \in O, r \in R$ / $S' = S, O' = O, t' = t, M'[s, o] = M[s, o] - \set{r}$, если $(s', o') \neq (s, o)$, то $M'[s', o'] = M[s', o']$. +<<создать>> субъект $s'$ с типом $t_s$ / $s' \not\in O$ / $S' = S \cup \set{s'}, O' = O \cup \set{s'}$, если $o \in O$, то $t'(o) = t(o), t'(s') = t_s$, если $(s, o) \in S \times O$, то $M'[s, o] = M[s, o]$, если $o \in O'$, то $M'[s', o] = \varempty$, если $s \in S'$, то $M'[s, s'] = \varempty$. +<<создать>> объект $o'$ с типом $t_o$ / $o' \not\in O$ / $S' = S, O' = O \cup \set{o'}$, если $o \in O$, то $t'(o) = t(o), t'(o') = t_o$, если $(s, o) \in S \times O$, то $M'[s, o] = M[s, o]$, если $s \in S'$, то $M'[s, o'] = \varempty$. +<<уничтожить>> субъект $s'$ / $s' \in O$ / $S' = S - \set{s'}, O' = O - \set{s'}$, если $o \in O$, то $t'(o) = t(o)$, если $(s, o) \in S' \times O'$, то $M'[s, o] = M[s, o]$. +<<уничтожить>> объект $o'$ / $o' \in O, o' \in S$ / $S' = S, O' = O - \set{o'}$, если $o \in O'$, то $t'(o) = t(o)$, если $(s, o) \in S' \times O'$, то $M'[s, o] = M[s, o]$. + +Таким образом, ТМД является обобщением модели ХРУ, которую можно рассматривать +как частный случай ТМД с одним единственным типом для всех субъектов и объектов. + +С другой стороны, любую ТМД можно выразить через систему ХРУ, введя для +обозначения типов специальные права доступа, а проверку типов в командах +заменив проверкой наличия соответствующих прав доступа. + +Пусть $c(x_1 : t_1, \dots, x_k : t_k)$ --- некоторая команда системы ТМД. Будем +говорить, что $x_i$ является \emph{дочерним параметром}, а $t_i$ является +\emph{дочерним типом} в $c(x_1 : t_1, \dots, x_k : t_k)$, где $1 \leq i \leq k$, +в случае, когда в ней имеется один из следующих примитивных операторов: +\begin{itemize} + \item <<создать>> субъект $x_i$ с типом $t_i$; + \item <<создать>> объект $x_i$ с типом $t_i$. +\end{itemize} + +В противном случае будем говорить, что $x_i$ является \emph{родительским +параметром}, а $t_i$ является \emph{родительским типом} в команде +$c(x_1 : t_1, \dots, x_k : t_k)$. + +Заметим, что в одной команде тип может быть одновременно и родительским и +дочерним. + +Например, +\begin{align*} + &command foo(s_1: u, s_2: u, s_3: v, o_1: w, o_2: b) \\ + & \text{<<создать>> субъект } s_2 \text{с типом } u; \\ + & \text{<<создать>> объект } s_3 \text{с типом } v; \\ + &end. +\end{align*} + +Здесь $u$ является + + +\emph{Система монотонной ТМД} (МТМД) --- система ТМД, в командах которой +отсутствуют немонотонные примитивные операторы вида <<удалить>> и +<<уничтожить>>. + +\emph{Каноническая форма системы МТМД} (КФМТМД) --- система МТМД, в которой +команды, содержащие примитивные операторы вида <<создать>>, не содержат +условий и примитивных операторов вида <<внести>>. + +\begin{theorem} %% NOTE: 2.3 + Для каждой системы МТМД существует эквивалентная ей система КФМТМД. +\end{theorem} +\begin{proof} + Пусть задана система МТМД, в которой определены множества $R, T, Q, C$. + Построим эквивалентную ей систему КФМТМД, определив множества $R^*, T^*, + Q^*, C^*$. + + Зададим множества + \begin{align*} + R^* &= R \cup \set{active}; \\ + T^* &= T \cup \set{t_{active}}. + \end{align*} + + В каждом состоянии $q^* = (S^*, O^*, t^*, M^*)$, соответствующем состоянию + $q = (S, O, t, M)$, справедливы равенства: + \begin{align*} + S^* &= S \cup \set{s_{active}}; \\ + O^* &= O \cup \set{s_{active}}. + \end{align*} + + Пусть также для каждого $o \in O$ справедливо равенство $t^*(o) = t(o)$ и + $s_{active}$ --- единственный объект такой, что $t^*(s_{active}) = t_{active}$. + + Кроме того, для $s \in S, o \in O$ справедливо равенство $M^*[s, o] = M[s, o]$, + и в начальном состоянии $q_0^* = (S_0^*, O_0^*, t_0^*, M_0^*)$ системы КФМТМД + для $o \in O_0$ справедливо равенство $M_0^*[s_{active}, o] = \set{active}$. + + Таким образом, право доступа $active$ обозначает активизированные субъекты и объекты + КФМТМД. + + Каждую команду $c(x_1: t_1, \dots, x_k: t_k) \in C$ системы МТМД, не содержащую + примитивные операторы <<создать>>, представим командой $c(x_1: t_1, \dots, x_k: + t_k, x: active)$ системы КФМТМД, полученной из исходной команды добавлением + условий проверки $active \in M[x, x_i], i = 1, \dots, k$. + + Каждую команду $c(x_1: t_1, \dots, x_k: t_k)$ системы МТМД, содержащую + примитивные операторы <<создать>>, представим монотонными командами КФМТМД: + \begin{itemize} + \item + $c'_{x_i}(x_{j_1}: t_{j_1}, \dots x_{j_m}: t_{j_m})$ --- команды без + проверки условий, каждая из которых соответствуют одному дочернему + параметру $x_i$ команды $c(x_1: t_1, \dots, x_k: t_k)$, содержит все её + родительские параметры и параметр $x_i$ и содержит соответствующий + примитивный оператор вида <<создать>>; + \item + $c''(x_1: t_1, \dots, t_k: t_k, x: t_{active})$ --- команда, содержащая + условия и примитивные операторы <<внести>> команды $c(x_1: t_1, \dots, + x_k: t_k)$, условия проверки $active \in M[x, x_i]$, для всех + родительских параметров $x_i$, примитивные операторы <<внести>> право + $active$ в $M[x, x_i]$ для всех дочерних параметров $x_i$. + \end{itemize} + + Таким образом, только <<активизированные>> объекты (в том числе и субъекты) + системы КФМТМД соответствуют объектам системы МТМД, а все преобразования над + ними в системе КФМТМД, соответствуют преобразованиям системы МТМД. +\end{proof} + +\emph{Граф создания системы МТМД} --- ориентированный граф с множеством вершин +$T$, в котором дуга от вершина $u$ к вершине $v$ существует $\iff$ в системе +имеется команда, в которой $u$ является родительским типом, а $v$ --- дочерним +типом. + +Система МТМД (КФ МТМД) называется \emph{ациклической} (АМТМД или, соответственно, +АКФМТМД) $\iff$ её граф создания не содержит циклов; в противном случае система +является \emph{циклической}. diff --git a/security-models/lectures/lecture5.tex b/security-models/lectures/lecture5.tex new file mode 100644 index 0000000..72ba78b --- /dev/null +++ b/security-models/lectures/lecture5.tex @@ -0,0 +1,2 @@ +% Лекция 5 (20.10.23) + diff --git a/security-models/lectures/lecture6.tex b/security-models/lectures/lecture6.tex new file mode 100644 index 0000000..856d7f7 --- /dev/null +++ b/security-models/lectures/lecture6.tex @@ -0,0 +1,182 @@ +% Лекция 6 (27.10.23) + +Третий шаг алгоритма всегда будет иметь конечную сложность. Так как множество +объектов не изменяется, то необходимо перебрать все последовательности различных +команд, а их конечное число. + +Наибольшую трудоёмкость в общем случае представляет разработка алгоритма +построения <<развёрнутого>> состояния. + +Однако для АМТМД или АКФМТМД такой алгоритм существует. + +Пусть $\alpha$ и $\beta$ --- две различные команды системы МТМД, содержащие +примитивные операторы <<создать>>, \dots. Будем считать, что $\alpha < \beta \iff$ +для некоторого дочернего типа команды $\alpha$ в графе создания найдётся путь +в некоторый родительский тип команды $\beta$. + +В системе АМТМД отношение <<$<$>> на множестве команд, содержащих примитивные +операторы <<создать>>, \dots, является отношением строгого порядка + +%% TODO +\textbf{Алгоритм 2.2} \emph{Алгоритм построения <<развёрнутого>> состояния для +системы АКФМТМД.} +\begin{enumerate} + \item + Упорядочить в списке все команды, содержащие примитивные операторы вида + <<создать>>, \dots (команда $\alpha$ следует в списке перед командой $\beta + \iff \alpha < \beta \; \lor$ $\alpha$ и $\beta$ не сравнимы). + \item + Начиная с начального состояния, применять команды в соответствии с созданным + на шаге 1 списком, при этом каждая команда применяется со всеми возможными + для неё наборами родительских объектов. +\end{enumerate} + +%% NOTE: 2.4 +\begin{theorem} + Существует алгоритм проверки безопасности систем АМТМД. +\end{theorem} +%% NOTE: 2.2 +\begin{corollary} + Алгоритм проверки безопасности систем АМТМД имеет экспоненциальную сложность. +\end{corollary} + +Для АМТМД, в которых каждая команда имеет не более трёх параметров, доказано, +что алгоритм проверки их безопасности имеет полиномиальную сложность. + +%% NOTE: 2.3 +\subsection{Модель распространения прав доступа Take-Grant} + +\subsubsection{} + +Классическая модель Take-Grant ориентирована на анализ путей распространения +прав доступа в системе дискреционного управления доступом. + +Основными элементами модели Take-Grant являются: +\begin{itemize} + \item $O$ --- множество объектов; + \item $S \subseteq O$ --- множество субъектов; + \item + $R = \set{r_1, r_2, \dots, r_m} \cup \set{t, g}$ --- множество видов прав + доступа, где $t$ (take) --- право брать права доступа, $g$ (grant) --- право + давать права доступа; + \item + $G = (S, O, E)$ --- конечный помеченный ориентированный без петель граф + доступов, описывающий состояние системы. +\end{itemize} + +Элементы множеств $S$ и $O$ являются вершинами графа, которые обозначаются +$\otimes$ --- объекты (элементы множества $O - S$) и $\cdot$ --- субъекты +соответственно. + +Элементы множества $E \subseteq O \times O \times R$ являются дугами графа. +Каждая дуга помечена непустым подмножеством множества видов прав доступа $R$. +Состояние системы описывается соответствующим ему графом доступов. + +В отличие от подели ХРУ в модели Take-Grant возможно наличие прав доступов не +только у субъектов к объектам, но и у объектов к объектам. + +Основная цель классической модели Take-Grant --- определение и обоснование +алгоритмически проверяемых условий проверки возможности утечки права доступа по +исходному графу доступов, соответствующего некоторому состоянию системы. + +Порядок перехода системы модели Take-Grant из состояния в состояние определяется +правилами преобразования графа доступов, которые в классической модели носят +название де-юре правил. + +Преобразование графа $G$ в граф $G'$ в результате выполнения правила $op$ +обозначается через $G \vdash_{op} G'$. + +В классической модели Take-Grant рассматриваются следующие четыре де-юре +правила преобразования графа, выполнение каждого из которых может быть +инициировано только субъектом, являющимся активной компонентой системы: +\begin{enumerate} + \item + $take$ --- брать права доступа (см. рис 2.1): субъект $x$ берёт у объекта + $y$ права $\alpha$ на объект $z$; + %% TODO: рис. 1 + \item + $grant$ --- давать права доступа (см. рис. 2.2): субъект $x$ даёт объекту + $y$ права $\alpha$ на объект $z$; + %% TODO: рис. 2 + \item + $create$ --- создать новый объект или субъект, при этом субъект создатель + может взять на созданный субъект любые права доступа (по умолчанию + предполагается, что создаётся объект, создание субъекта оговаривается особо) + (см. рис. 2.3); + %% TODO: рис. 3 + \item + $remove$ --- удалять права доступа (см. рис. 4): субъект $x$ удаляет из + своих прав доступа на объект $y$ набор прав $\alpha$. + %% TODO: рис. 4 +\end{enumerate} + +%% TODO: нумерация +В таблице 2.3 приведены условия применения де-юре правил в исходном состоянии +$G = (S, O, E)$ и результаты их применения в результирующем состоянии +$G' = (S', O', E')$. + +%% TODO: таблица 2.3 --- Де-юре правила классической модели Take-Grant +Правила | Исходное состояние $G = (S, O, E)$ | Результирующее состояние $G' = (S', O', E')$ +$take(\alpha, x, y, z)$ | $x \in S, \; y, z \in O, \; (x, y, \set{t}) \subset E, \; (y, z, \beta) \subset E, \; x \neq z, \; \alpha \subseteq \beta$ | $S' = S, O' = O, E'= E \cup \set{(x, z, \alpha)}$ + +\begin{itemize} + \item $grant(\alpha, x, y, z)$ + \item + $x \in S, \; y, z \in O, \; (x, y, \set{g}) \subset E, \; (x, z, \beta) + \subset E, \; y \neq z, \; \alpha \subseteq \beta$ + \item $S' = S, O' = O, E'= E \cup \set{(y, z, \alpha)}$ +\end{itemize} +\begin{itemize} + \item $create(\beta, x, y)$ + \item $x \in S, \; y \not\in O, \beta \neq \varnothing$ + \item $O' = O \cup \set{y}$, если $y$ субъект, то $S' = S \cup \set{y}$, + иначе $S' = S, \; E' = E \cup \set{(x, y, \beta)}$ +\end{itemize} +\begin{itemize} + \item $remove(\alpha, x, y)$ + \item $x \in S, \; y \in O, \; (x, y, \beta) \subset E, \; \alpha \subseteq \beta$ + \item $S' = S, \; O' = O, \; E' = E - \set{(x, y, \alpha)}$ +\end{itemize} + +Рассмотрим условия, при которых в системе возможно распространение прав доступа. + +Пусть дан граф доступов $G_0 = (S_0, O_0, E_0), \; x, y \in O_0, \; x \neq y, \; +\alpha \subseteq R$. Определим предикат $\fn{can_share}(\alpha, x, y, G_0)$, +который будет истинным $\iff \exists G_1 = (S_1, O_1, E_1), \dots, G_N = (S_N, +O_N, E_N)$ и правила $op_1, \dots, op_N, \; N \geq 0 : G_0 \vdash_{op_1} G_1 +\vdash_{op_2} \dots \vdash_{op_N} G_N \land (x, y, \alpha \subset E_N$. + +Определение истинности предиката $\fn{can_share}(\alpha, x, y, G_0)$ +непосредственно по определению является в общем случае алгоритмически +неразрешимой задачей, так как требует проверки всех траекторий функционирования +системы. + +По этой причине для проверки истинности предиката $\fn{can_share}(\alpha, x, y, +G_0)$ следует определить необходимые и достаточные условия, проверка которых +возможна. Решение этой задачи будет выполнено в два этапа: +\begin{enumerate} + \item %% TODO: дописать + \item Определены и обоснованы условия истинности предиката для произвольных + графов. +\end{enumerate} + +Пусть $G = (S, S, E)$ --- граф доступов, все вершины которого являются субъектами. +Говорят, что вершины графа доступов являются $tg$-связными или что они соединены +$tg$-путём, когда, без учёта направления рёбер, в графе между ними существует +путь такой, что каждое ребро этого пути помечено $t$ или $g$. + +\begin{theorem} + Пусть $G_0 = (S_0, O_0, E_0)$ --- граф доступов, содержащий только вершины + субъекты, $x, y \in S_0, \; x \neq y$. + + Тогда предикат $\fn{can_share}(\alpha, x, y, G_0)$ истинен $\iff$ выполняются + следующие два условия: + \begin{enumerate} + \item + существуют субъекты $s_1, \dots, s_m \subset S_0 : (s_i, y, \gamma_i) + \subset E_0$, где $i = 1, \dots, m$ и $\alpha = \gamma_1 \cup \dots \cup + \gamma_m$; + \end{enumerate} +\end{theorem} + +%% TODO: дописать diff --git a/security-models/lectures/lecture7.tex b/security-models/lectures/lecture7.tex new file mode 100644 index 0000000..9134d9e --- /dev/null +++ b/security-models/lectures/lecture7.tex @@ -0,0 +1,65 @@ +% Лекция 7 (03.11.23) + +% 2.4 (9) Постройте графы создания для систем МТМД со следующими наборами команд. +% +% а) +% command a1(x: $\alpha$, y: $\beta$, z: $\beta$) +% <<создать>> субъект x с типом $\alpha$; +% end; +% command a2(x: $\alpha$, y: $\gamma$, z: $\beta$, s: $\delta$) +% <<создать>> субъект y с типом $\gamma$; +% <<создать>> субъект s с типом $\delta$; +% end; +% command a3(x: $\varepsilon$, y: $\delta$, z: $\beta$, s: $\gamma$, o: $\delta$) +% <<создать>> субъект o с типом $\delta$; +% <<создать>> субъект x с типом $\varepsilon$; +% end; + +\emph{Начальным пролётом моста} в графе доступов $G_0$ называется $tg$-путь, +началом которого является вершина субъект, концом --- объект, проходящий +через вершины объекты, словарная запись которого имеет вид $\vec{t}^* \vec{g}$. + +\emph{Конечным пролётом моста} в графе доступов $G_0$ называется $tg$-путь, +началом которого является вершина субъект, концом --- объект, проходящий через +вершины объекты, словарная запись которого имеет вид $\vec{t}^*$. + +%% NOTE: 2.6 +\begin{theorem} + Пусть $G_0 = (S_0, O_0, E_0)$ --- произвольный граф доступов, $x, y \in O_0, + x \neq y$. Предикат $\fn{can_share}(\alpha, x, y, G_0)$ истинен $\iff$ или + $(x, y, \alpha) \subset E_0$, или выполняются следующие три условия: + \begin{enumerate} + \item + существуют объекты $s_1, \dots, s_m \in O_0: (s_i, y, \gamma_i) \subset + E_0$ для $i = 1, \dots, m$ и $\alpha = \gamma_1 \cup \dots \cup \gamma_m$; + \item + существуют субъекты $x_1', \dots, x_m', s_1', \dots, s_m' \in S_0$ : + \begin{enumerate} + \item + $x = x_i'$ или $x_i'$ соединён с $s_i$ конечным пролётом моста в графе + $G_0$, где $i = 1, \dots, m$; + \item + $s_i = s_i'$ или $s_i'$ соединён с $s_i$ конечным пролётом моста в + $графе G_0$, где $i = 1, \dots, m$; + \end{enumerate} + \item + в графе $G_0$ для каждой пары $(x_i', s_i')$, $i = 1, \dots, m$, + существуют острова $I_{i,1}, \dots, I_{i,u_i}$, где $u_i \geq 1$, такие, + что $x_i' \in I_{i,1}, s_i' \in I_{i,u_i}$, и существуют мосты между + островами $I_{i,j}$ и $I_{i,j + 1}$, $j = 1, \dots, u_i - 1$. + \end{enumerate} +\end{theorem} + +Смысл теоремы состоит в том, что если в системе разграничения доступа в +начальном состоянии между двумя какими-либо объектами имеется $tg$-путь, +включающий, в том числе, мосты между островами, то найдётся такая +последовательность команд вида <>, <>, <>, в результате +которой первый объект получит необходимые права доступа над другим объектом. +Существенным при этом является отсутствие каких-либо ограничений на кооперацию +субъектов и объектов доступа, в частности, отсутствие запретов на передачу прав +доступа к объекту субъектами, изначально обладающими необходимыми правами на +объект, представляющий интерес для других субъектов. Говоря иначе, подобный +порядок вещей характеризует идеальное сотрудничество и доверие между субъектами +доступа. + + diff --git a/security-models/lectures/lecture8.tex b/security-models/lectures/lecture8.tex new file mode 100644 index 0000000..afc6c39 --- /dev/null +++ b/security-models/lectures/lecture8.tex @@ -0,0 +1,148 @@ +% Лекция 8 (10.11.23) + +Похищение прав доступа является примером случая, когда передача прав доступа +к объекту осуществляется без содействия субъекта, изначально обладавшего +передаваемыми правами, таким образом, не все субъекты системы кооперируют друг с +другом. + +Пусть $x, y \in O_0, \, x \neq y$ --- различные объекты графа доступов $G_0 = +(S_0, O_0, E_0),\, \alpha \subseteq R$. Определим предикат $\fn{can_steal}( +\alpha, x, y, G_0)$, который будет истинным $\iff (x, y, \alpha) \cap E_0 = +\varnothing$, существуют графы $G_1 = (S_1, O_1, E_1)$, $\dots$, $G_N = (S_N, +O_N, E_N)$ и правила $op_1, \dots, op_N$, где $N \geq 1$, такие, что $G_0 +\vdash_{op_1} G_1 \vdash_{op_2} \dots \vdash_{op_N} G_N$ и $(x, y, \alpha) +\subset E_N$, при этом, если существует $(s, y, \gamma) \subset E_0$, где +$\gamma \subseteq \alpha$, то справедливо неравенство $op_k \neq \fn{grant}( +\gamma, s, z, y)$, где $z \in O_{K - 1}, K = 1, \dots, N$. + +Говоря иначе, согласно определению похищением прав является процесс получения +прав доступа на какой-либо объект без представления прав третьим субъектам со +стороны субъекта, обладающего в начальном состоянии требуемыми правами на +объект <<интересе>>. + +%% NOTE: 2.7 +\begin{theorem} + Пусть $G_0 = (S_0, O_0, E_0)$ --- произвольный граф доступов, $x, y \in O_0$, + $x \neq y$. Предикат $\fn{can_steal}(\alpha, x, y, G_0)$ истинен $\iff$ + выполняются следующие четыре условия: + \begin{enumerate} + \item $(x, y, \alpha) \cap E_0 = \varnothing$; + \item существуют объекты $s_1, \dots, s_m \in O_0$ такие, что $(s_i, y, + \gamma_i) \subset E_0$ для $i = 1, \dots, m$ и $\alpha = \gamma_1 \cup + \dots \cup \gamma_m$; + \item являются истинными предикаты $\fn{can_share}(\set{t}, x, s_i, G_0)$, + где $i = 1, \dots, m$; + \item + для $i = 1, \dots, m$ граф доступов $G_0$ не является графом вида, + приведённого на рисунке 2.7 + %% TODO: рис 1 (2.7) + %% TODO: Условие 4 теоремы 2.5 + \end{enumerate} +\end{theorem} + +Данная теорема означает, что если политика разграничения доступа в компьютерной +системе запрещает субъектам, имеющим в исходном состоянии права доступа к +определённым объектам, непосредственно предоставлять эти права другим субъектам +(то есть такие потоки, для которых в графе доступов $G_0$ нет дуг <<$g$>> от +этих субъектов), которые изначально такими правами не обладают, то тем не менее, +такие первоначально <<обделённые>> субъекты могут получить данные права при +наличии в графе доступов возможностей получения доступа с правом $t$ к первым +субъектам. + +Таким образом, модель \emph{take-grant} играет важную методологическую роль, +предоставляя теоретико-графовый инструмент анализа систем разграничения доступа +с точки зрения санкционированного и несанкционированного со стороны определённых +субъектов распространения прав доступа в рамках дискреционной политики. + +Правила де-юре контролируют только передачу полномочий, они ничего не говорят о +передач информации, поэтому на основе классической модели \emph{Take-Grant} +были разработаны её расширения, которые предлагают новые механизмы анализа, в +большей степени применимые к современным системам защиты информации. + +Рассмотрим некоторые расширения модели. + +%% NOTE: 1 +\paragraph{Де-факто правила, предназначенные для поиска и анализа информационных +потоков.} + +Вместо прав доступа take и grant в расширенной модели в первую очередь +рассматриваются права read и write, наличие которых у субъектов системы является +причиной возникновения информационных потоков. + +Основные элементы (дополнения): +\begin{itemize} + \item + $R = \set{r_1, r_2, \dots, r_m} \cup \set{t, g} \cup \set{r, w}$ --- + множество видов прав доступа информационных потоков, где r (read) --- право + на чтение или информационный поток на чтение, w (write) --- право на запись + или информационный поток на запись; + \item + $G = (S, O, E \cup F)$ --- граф доступов и информационных потоков; + \item + Элементы множества $E \subseteq O \times O \times R$ являются <<реальными>> + дугами графа, соответствующими правам доступа, и в графе доступов + обозначается сплошными линиями; + \item + Элементы множества $F \subseteq O \times O \times \set{r, w}$ являются + <<мнимыми>> дугами, соответствующими информационным потокам, и в графе + доступов обозначаются пунктирными линиями. + \item + Каждая <<реальная>> дуга помечена непустым подмножеством множества всех видов + прав доступа $R$, каждая <<мнимая>> дуга помечена непустым подмножеством + множества $\set{r, w}$; + \item + Порядок перехода системы расширенной модели \emph{Take-Grant} из состояния + в состояние определяется де-юре и де-факто правилами преобразования графов + доступов и информационных потоков; + \item + Преобразование графа $G$ в граф $G'$ в результате выполнения правила $op$ + обозначается $G \vdash_{op} G'$. +\end{itemize} + +Определение де-юре правил take, grant, create, remove совпадает с определением +этих правил в классической модели Take-Grant. + +Де-юре правила применяются только к <<реальным>> дугам (элементам множества +$E$). Де-факто правила применяются к <<реальным>> или <<мнимым>> дугам +(элементам множества $E \cup F$), помеченным $r$ или $w$. + +Результатом применения де-факто правил является добавление новых <<мнимых>> дуг +в множество $F$. Рассматриваются шесть де-факто правил: два вспомогательных и +четыре основных + +\begin{itemize} + \item + См. рисунок 2.8: субъект $x$ получает возможность записи (в себя) информации, + осуществляя доступ $r$ к объекту $y$. + %% TODO: рис. 2 (2.8) + %% TODO: Применение первого де-факто правила + \item + См. рисунок 2.8: субъект $x$ получает возможность чтения информации, + осуществляя доступ $w$ к объекту $y$. + %% TODO: рис. 3 (2.9) + %% TODO: Применение второго де-факто правила + \item + \emph{Spy} (шпион) (см. рисунок 2.10): субъект $x$ получает возможность + чтения информации из объекта $z$, осуществляя доступ $r$ к субъекту $y$, + который, в свою очередь, осуществляет доступ $r$ к объекту $z$, при этом + также у субъекта $x$ возникает возможность записи к себе информации из + объекта $z$. + + Получается, $x$ шпионит за $z$, используя $y$, другими словами, $x$ <<смотрит + через плечо>> $y$, чтобы следить за $z$. + %% TODO: рис. 4 (2.10) + %% TODO: Применение правила spy(x, y, z) + \item + \emph{Find} (находить) (см. рисунок 2.11): субъект $x$ получает возможность + чтения информации из объекта $z$, осуществляя доступ $w$ к субъекту $y$, + который, в свою очередь, осуществляет доступ $w$ к объекту $z$, при этом + также у субъекта $x$ возникает возможность записи к себе информации из + объекта $z$. + %% TODO: рис. 5 (2.11) + %% TODO: Применение правила spy(x, y, z) + \item + \emph{Post} (почта) (см. рисунок 2.12): субъект $x$ получает возможность чтения + информации от (из) другого субъекта $z$, осуществляя доступ $r$ к объекту + $y$, к которому субъект $z$ осуществляет доступ $w$, а субъект $z$, в + свою очередь. +\end{itemize} diff --git a/security-models/lectures/lecture9.tex b/security-models/lectures/lecture9.tex new file mode 100644 index 0000000..357dc2c --- /dev/null +++ b/security-models/lectures/lecture9.tex @@ -0,0 +1,2 @@ +% Лекция 9 (17.11.23) + diff --git a/security-models/security-models.pdf b/security-models/security-models.pdf index 91b4dc6..9a85d02 100644 Binary files a/security-models/security-models.pdf and b/security-models/security-models.pdf differ diff --git a/security-models/security-models.tex b/security-models/security-models.tex index 7d25199..571d40c 100644 --- a/security-models/security-models.tex +++ b/security-models/security-models.tex @@ -16,6 +16,17 @@ \newpage % Семестр 1 +% 1 \input{lectures/lecture2.tex} +% 3 +\input{lectures/lecture4.tex} +% \input{lectures/lecture5.tex} +\input{lectures/lecture6.tex} +\input{lectures/lecture7.tex} +\input{lectures/lecture8.tex} +% \input{lectures/lecture9.tex} +\input{lectures/lecture10.tex} +% 11 +\input{lectures/lecture12.tex} \end{document} -- cgit v1.2.3