Лекции по моделям безопасности и методам алгебраической геометрии

10 files changed, 918 insertions, 0 deletions

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$-путь,
+включающий, в том числе, мосты между островами, то найдётся такая
+последовательность команд вида <<take>>, <<grant>>, <<create>>, в результате
+которой первый объект получит необходимые права доступа над другим объектом.
+Существенным при этом является отсутствие каких-либо ограничений на кооперацию
+субъектов и объектов доступа, в частности, отсутствие запретов на передачу прав
+доступа к объекту субъектами, изначально обладающими необходимыми правами на
+объект, представляющий интерес для других субъектов. Говоря иначе, подобный
+порядок вещей характеризует идеальное сотрудничество и доверие между субъектами
+доступа.
+
+
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
--- a/security-models/security-models.pdf
+++ b/security-models/security-models.pdf
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}