% =========================================================================
%  Pointer Flow Integrity (PFI) — формальная спецификация на языке Z
%  Файл: PFI_Specification_Z.ru.tex
%  Назначение: самодостаточная Z-спецификация, компилируемая стандартными
%              пакетами TeX Live (без редкого zed.sty). Схемы рисуются
%              средствами array + amsmath.
%
%  Сборка:  pdflatex PFI_Specification_Z.ru.tex   (нужны шрифты T2A)
%           xelatex PFI_Specification_Z.ru.tex     (тоже работает)
%
%  Примечание: на машине-источнике движок LaTeX отсутствовал, поэтому
%              файл не компилировался локально; синтаксис следует
%              канону Z (ISO/IEC 13568).
%
%  Источник теории : pfi.pdf (Indy, 2022)
%  Верификация     : ядро Windows 11 ARM64, build 26100
%                    (nt!KiServiceInternal / KiSystemService / KiSystemServiceCopyEnd)
% =========================================================================
\documentclass[11pt,a4paper]{article}

\usepackage[T2A]{fontenc}
\usepackage[utf8]{inputenc}
\usepackage[russian,english]{babel}
\usepackage{amsmath,amssymb,amsthm}
\usepackage{mathtools}
\usepackage{array}
\usepackage{booktabs}
\usepackage{longtable}
\usepackage{geometry}
\geometry{margin=2.1cm}
\usepackage{hyperref}

% ----------------------------- символы Z ---------------------------------
\newcommand{\Znum}{\mathbb{N}}
\newcommand{\Zint}{\mathbb{Z}}
\newcommand{\Power}{\mathbb{P}}
\newcommand{\fun}{\to}
\newcommand{\pfun}{\rightharpoonup}        % частичная функция
\newcommand{\rel}{\leftrightarrow}          % отношение
\newcommand{\Zdom}{\operatorname{dom}}
\newcommand{\Zran}{\operatorname{ran}}
\newcommand{\Zseq}{\operatorname{seq}}
\newcommand{\Shift}{\operatorname{Shift}}   % адресная арифметика (не ⊕ !)
\newcommand{\PageOf}{\operatorname{PageOf}}
\newcommand{\Protect}{\operatorname{Protect}}

% --------------------- рендеринг Z-схем через array ---------------------
% Именованная схема:  \zschema{Имя}{объявления}{предикат}
\newcommand{\zschema}[3]{%
\[
\begin{array}{|l|}
\hline
\;\mathrm{#1} \\
\hline
\begin{array}{l} #2 \end{array} \\
\hline
\begin{array}{l} #3 \end{array} \\
\hline
\end{array}
\]}
% Аксиоматическое определение (без имени):  \zaxdef{объявления}{предикат}
\newcommand{\zaxdef}[2]{%
\[
\begin{array}{|l|}
\hline
\begin{array}{l} #1 \end{array} \\
\hline
\begin{array}{l} #2 \end{array} \\
\hline
\end{array}
\]}
% Блок определений / свободные типы:  \zblock{...}
\newcommand{\zblock}[1]{\[\begin{array}{l} #1 \end{array}\]}

% ------------------------------- теоремы ---------------------------------
\newtheorem{thm}{Теорема}
\newtheorem*{sketch}{Доказательство (набросок)}

\title{\textbf{Pointer Flow Integrity} \\ \large Формальная спецификация на языке~Z}
\author{Сессия отладки ядра Windows 11 ARM64 (build 26100)}
\date{2026-07-25}

\begin{document}
\selectlanguage{russian}
\maketitle

\section{Назначение и статус}
PFI формализует, как \emph{визор} (DBI/секвенсор) наблюдает и изолирует
управление и поток данных задачи и как он обнаруживает нелегитимный перехват
со стороны эмуляторов антивирусов (AVM) и виртуализационных прослоек
(VMP / VM-call). Документ содержит:
\begin{enumerate}
  \item абстрактную модель секвенции против машинного потока, графа потока
        указателей (PFG) и инварианта целостности данных (DFI);
  \item перенаправление IDP (программный анклав), предикат обнаружения AVM и
        подмену адреса возврата S-route для атомарных шлюзов;
  \item конкретную инстанциацию на верифицированной диспетчерской таблице
        ядра с теоремами.
\end{enumerate}

\textbf{Замечание о гигиене Z:} для адресной арифметики используется
функция $\Shift$ --- \emph{не} символ~$\oplus$, поскольку в~Z $\oplus$
обозначает overriding функций/отношений.

\section{Базовые множества и определения}
\zblock{
[ADDR,\; INSTR,\; REF,\; REG,\; VAL,\; SSN,\; EC,\; Process] \\[6pt]
ATOM    ::= syscall \mid sysenter \mid indirectCall \mid vmcall \mid gate \\
Mode    ::= User \mid Kernel \\
Access  ::= Rd \mid Wr \mid Ex \\
Prot    ::= ReadOnly \mid RW \\[6pt]
FlowElem == INSTR \cup ATOM \\
RetGate  == \{\, syscall,\; sysenter \,\} \\
GateAtom == ATOM \\[6pt]
EA  == ADDR \\
Ptr == ADDR \\[6pt]
Bool       ::= true \mid false \\
PACKey     == ADDR \times ADDR \\
SignedAddr == ADDR \\[6pt]
EVENT ::= Enter\langle ATOM \times ADDR\rangle \;\mid\; Exit\langle ATOM \times ADDR\rangle
}

Глобальные сигнатуры (фиксируются семантикой ISA):
\zaxdef{
Accesses : FlowElem \rel ADDR \quad \text{--- отношение <<элемент обращается по адресу>>} \\
Select   : FlowElem \fun \Znum \quad\;\; \text{--- размер выборки (байты)} \\
Shift    : ADDR \times \Zint \fun ADDR \quad \text{--- адресный сдвиг} \\
\PageOf  : ADDR \fun ADDR \quad\;\;\; \text{--- база страницы (здесь: large page / PDE)} \\
\Protect : ADDR \fun Prot \\
WriteFault : \Power\, ADDR \quad \text{--- адреса, запись в которые вызывает отказ} \\
Exec       : ADDR \fun Bool \quad\;\, \text{--- страница исполняемая}
}{}

\section{Поток управления: секвенция против машинного потока}
Визор производит \emph{секвенированный} поток $Cf$ (исполняется из буфера
визора), процессор исполняет \emph{машинный} поток $Xf$. Они расходятся на
атомах, когда исполнение покидает буфер (смена адреса снимает хуки
AV-эмулятора).

\zschema{Sequencing}{
Cf : \Zseq\, FlowElem \\
Xf : \Zseq\, FlowElem
}{
Cf \neq \langle\rangle
}

\zschema{Diverges}{
a? : ATOM \\
k  : \Znum
}{
Cf\, k = a? \\
Xf\, k \neq a? \;\;\lor\;\; \#Xf \neq \#Cf
}
Атом~$a?$ в позиции~$k$ потока $Cf$ \emph{расходится}, если машинный поток в
этой позиции не равен~$a?$ или длины потоков различны --- формальная запись
утверждения <<атомы уходят из-под секвенсора>>.

\section{Состояние задачи}
\zschema{TS}{
regs     : REG \pfun VAL \\
frame    : \Zseq\, VAL \\
prevMode : Mode \\
lr       : ADDR \\
retSlot  : ADDR
}{
prevMode \in \{User,\; Kernel\}
}
Поле $retSlot$ --- адрес, по которому возобновляется исполнение после
системного атома; на верифицированном ядре это пара $lr/fp$, восстанавливаемая
в~\texttt{KiSystemServiceCopyEnd+0x38} инструкцией \texttt{ldp fp,lr,[sp,\#0x50]}.

\section{Граф потока указателей (PFG)}
\zschema{PFG}{
ts      : TS \\
CS      : \Power\, Ptr \\
IS      : FlowElem \fun \Power\, Ptr \\
enclave : \Power\, ADDR \\
\delta   : \Zint
}{
enclave \neq \varnothing
}
$CS$ --- текущее множество живых указателей, $IS$ --- разрешённое входное
множество на элемент потока, $enclave$ --- изолированная область (программный
анклав), $\delta$ --- смещение перенаправления IDP.

\section{Инвариант целостности данных (DFI)}
Центральное свойство: любое обращение в память, выполняемое секвенированным
элементом, должно быть по адресу из текущего множества или из входного
множества этого элемента.

\zschema{DFI}{PFG}{
\forall e : FlowElem;\; ea : EA \,@ \\
\qquad (e \mapsto ea) \in Accesses \;\Rightarrow\; ea \in CS \cup IS(e)
}
Обращение, чьего $EA$ нет ни в одном из множеств, не может быть порождено
санкционированным потоком --- это сигнатура внедрённого перехвата
(критерий фиксации AVM / OP-инжектов).

\section{IDP --- перенаправление EA в программный анклав}
\zschema{Redirect}{
ea? : EA \\
ea! : EA
}{
ea! = \Shift(ea?,\; \delta) \\
ea! \in enclave
}
При секвенции визор сдвигает эффективный адрес на~$\delta$, направляя выборку
данных в изолированный анклав; эмулятор АВ, читающий \emph{исходный} адрес,
не видит трафика.

\section{Обнаружение AVM / эмулятора}
\zschema{AVMDetected}{
e?  : FlowElem \\
ea? : EA
}{
(e? \mapsto ea?) \in Accesses \;\land\; ea? \notin CS \cup IS(e?)
}
Свидетельство $\mathrm{AVMDetected}$ в ходе секвенции $\Rightarrow$ присутствует
нелегитимная эмуляция/перехват. Это двойник инварианта DFI: DFI утверждает
отрицание для санкционированного потока.

\section{Атомы и S-route}
\zaxdef{ enabled : \Power\, ATOM \quad \text{--- множество наблюдаемых атомов} }{}

Наблюдение атомов (ядерный аналог --- \texttt{KiTrackSystemCallEntry/Exit},
включается битом~0 по \texttt{PpmPolicyConfigTable+0xD00}):
\zschema{ObserveAtom}{
a?      : ATOM \\
target? : ADDR \\
evt!    : EVENT
}{
a? \in enabled \\
evt! = Enter(a?,\; target?)
}

S-route: для возвратного атома визор сохраняет исходный адрес возврата и
подменяет его своей заглушкой, чтобы управление вернулось в секвенсор, а не в
API эмулятора АВ.
\zaxdef{
STUB   : ADDR \quad \text{--- заглушка возобновления S-route} \\
OK     : EC \\
NtCode : \Power\, ADDR \quad \text{--- кодовая область обработчиков \texttt{nt!Nt*}}
}{}

\zschema{SRoute}{
\Delta PFG \\
a?     : ATOM \\
saved! : ADDR
}{
a? \in RetGate \\
saved! = ts.retSlot \\
ts.retSlot' = STUB \\
CS' = CS;\; IS' = IS;\; enclave' = enclave;\; \delta' = \delta
}

\zschema{RestoreReturn}{
\Delta PFG \\
saved? : ADDR
}{
ts.retSlot' = saved?
}

\section{Конкретная инстанциация ядром (верифицировано)}
Значения сняты непосредственно с живого ядра.

\zaxdef{
KiServiceTableBase   : ADDR \\
KiArgTable           : ADDR \\
KiServiceLimitValue  : \Znum \\
DescriptorAddr       : ADDR \\
InvalidSvcEC         : EC
}{
KiServiceLimitValue = 489
}
\begin{tabular}{@{}ll@{}}
% доказательства (hex), снятые отладчиком:
% KiServiceTableBase  = 0xFFFFF8004BC96C28   (KeServiceDescriptorTable.Base)
% KiArgTable          = 0xFFFFF8004BC973D0   (таблица размеров аргументов)
% KiServiceLimitValue = 0x1E9 = 489          (KiServiceLimit)
% DescriptorAddr      = 0xFFFFF8004CC01900   (сам дескриптор KeServiceDescriptorTable)
% InvalidSvcEC        = 0xC000001C           (STATUS_INVALID_SYSTEM_SERVICE)
\end{tabular}

Функция декодирования реализует инструкцию \texttt{add x11,x11,x10,asr\#4}:
\zaxdef{
Decode : ADDR \times \Znum \fun ADDR
}{
\forall b : ADDR;\; e : \Znum \,@ \\
\qquad Decode(b,\; e) = \Shift(b,\; e \div 16)
}

\subsection{Дескриптор и таблица сервисов}
\zschema{ServiceTable}{
base   : ADDR \\
limit  : \Znum \\
number : ADDR \\
table  : SSN \pfun \Znum
}{
base = KiServiceTableBase \\
limit = KiServiceLimitValue \\
number = KiArgTable
}

\subsection{Диспетчеризация (успешный путь)}
Реализует \texttt{cmp x8,x10; bhs fail} и \texttt{ldrsw}/\texttt{add ... asr\#4}
из \texttt{KiSystemService}:
\zschema{Dispatch}{
ServiceTable \\
ssn?     : SSN \\
handler! : ADDR \\
status!  : EC
}{
ssn? < limit \\
ssn? \in \Zdom\, table \\
handler! = Decode(base,\; (table\, ssn?) \div 16) \\
status! = OK
}

\subsection{Выход за пределы (путь ошибки)}
Реализует \texttt{mov x0,\#0x1C; movk x0,\#0xC000,lsl\#0x10} в
\texttt{KiSystemServiceCopyEnd+0x88}:
\zschema{InvalidService}{
ServiceTable \\
ssn?    : SSN \\
status! : EC
}{
ssn? \geq limit \\
status! = InvalidSvcEC
}

\subsection{Целостность таблицы (отображение только для чтения)}
Проверено командой \texttt{!pte fffff8004bc96c28}: атрибуты PDE
\texttt{-R-GA-K-LV} (large page, \textbf{без W}), тогда как обёртка-дескриптор
по адресу \texttt{fffff8004cc01900}: \texttt{-W-GADK-LV} (доступна для записи):
\zschema{TableIntegrity}{ServiceTable}{
\Protect(\PageOf(base)) = ReadOnly \\
\Protect(\PageOf(DescriptorAddr)) = RW
}
Сама таблица смещений обработчиков отображена read-only на уровне PDE
(large page); запись в неё из ядра вызывает data abort. Это ядерный аналог
IDP-защиты визора.

\section{Дополнительная верификация: аппаратная и ядерная реализация целостности}

\subsection{Trap-фрейм}
\zschema{TrapFrame}{
pc   : ADDR \\
spsr : ADDR \\
regs : REG \pfun VAL
}{}

\subsection{PAC --- аутентификация указателей (ARMv8.3)}
Аппаратный аналог целостности указателей из pfi.pdf. Функции ядра подписывают
адрес возврата в прологе инструкцией \texttt{pacibsp} (PAC, B-ключ, модификатор
SP); \texttt{paciasp}/\texttt{pacibsp} одновременно служит landing pad для BTI.
\zaxdef{
Sign     : ADDR \cross PACKey \fun SignedAddr \\
Auth     : SignedAddr \cross PACKey \fun ADDR \\
PACKeyOf : Process \pfun PACKey \\
EnIBOf   : Process \fun Bool
}{}

\zschema{PACSign}{
lr? : ADDR \\
k?  : PACKey \\
lr! : SignedAddr
}{
lr! = Sign(lr?,\; k?)
}
\textit{Свидетельство (дизассемблер):} \texttt{nt!NtClose}, \texttt{nt!NtQueryInformationProcess},
\texttt{nt!KiTrackSystemCallEntry} начинаются с \texttt{d503237f pacibsp}.

\zschema{KernelCtxt}{
apdbKey : PACKey \\
enIB    : Bool
}{}

\zschema{PACContextSwitch}{
\Delta KernelCtxt \\
p? : Process
}{
apdbKey' = PACKeyOf(p?) \\
enIB'    = EnIBOf(p?)
}
\textit{Свидетельство:} в \texttt{nt!KiSystemServiceExit} --- \texttt{mrs SCTLR\_EL1},
переключение бита \texttt{EnIB} (bit~30) по флагу процесса, загрузка
\texttt{APDBKeyLo/Hi} (\texttt{S3\_0\_C2\_C1\_2/3}), \texttt{isb}. Ключи PAC
переключаются по процессам.

\textit{Аутентификация (полный цикл PAC):} \texttt{nt!KiTrackSystemCallExit}
завершается инструкцией \texttt{d50323ff autibsp} непосредственно перед
\texttt{ret} --- пара подпись~(\texttt{pacibsp}) на входе $\to$
аутентификация~(\texttt{autibsp}) на возврате подтверждена.

\textit{Входная конфигурация (зеркало выхода):} \texttt{nt!KiConfigPointerAuthKernelEntry}
на входе в ядро --- \texttt{mrs SCTLR\_EL1}; \texttt{bfi} бита \texttt{EnIB}
по флагу \texttt{[+0x880]} (bit~2); загрузка ключей из \texttt{[+0x8F0]} в
\texttt{APDBKeyLo/Hi} (\texttt{S3\_0\_C2\_C1\_2/3}); \texttt{isb}. Источник
ключей и флаг \texttt{EnIB} --- per-process.

\subsection{Возврат в R3: ELR\_EL1 --- точка подмены S-route}
\zschema{SystemCallReturn}{
tf    : TrapFrame \\
elr'  : ADDR \\
spsr' : ADDR
}{
elr'  = tf.pc \\
spsr' = tf.spsr
}
\textit{Свидетельство:} \texttt{msr ELR\_EL1,x2}, где $x2 \leftarrow [sp,\#0x140]$
(trap-фрейм), затем очистка регистров/SIMD и \texttt{eret} по адресу
\texttt{fffff8004c236068}. Именно \texttt{tf.pc}~$\to$~\texttt{ELR\_EL1} есть
целевой адрес возврата в~R3 --- объект подмены S-route. Перед возвратом
вызывается \texttt{nt!KiPreflightReturnToUserMode} --- preflight проверки
целостности.

\subsection{Теневая и фильтрующая таблицы}
\zschema{ShadowServiceTable}{
ntBase   : ADDR;\; ntLimit  : \Znum \\
guiBase  : ADDR;\; guiLimit : \Znum
}{
ntBase   = KiServiceTableBase \\
ntLimit  = 489 \\
guiLimit = 1493
}
\textit{Свидетельство:} \texttt{KeServiceDescriptorTableShadow} --- дескриптор[0]~=~nt
($489$), дескриптор[1]~=~\texttt{win32k.sys} (\texttt{Limit}=0x5D5=1493);
\texttt{KeServiceDescriptorTableFilter} --- отдельный base для win32k (sandbox).
Выбор per-thread: \texttt{tst x10,\#0x80}; \texttt{tst x10,\#0x200000} в
\texttt{KiSystemService}.

\subsection{Наблюдение атомов: KiTrackSystemCallEntry}
Схему \texttt{ObserveAtom} уточняем верифицированными деталями: чтение
\texttt{PreviousMode} (\texttt{ldrsb w0,[x8,\#0x252]} --- поле
\texttt{\_KTHREAD+0x252}); фильтр \texttt{nt!KeIsTraceCallbackAllowed}; поиск по
ключу-обработчику в \texttt{nt!KiSystemServiceTraceTable}; атомарный счётчик
(\texttt{ldaddal}).

\subsection{Граница user/kernel и Probe (DFI)}
\zaxdef{ MMUserProbe : ADDR }{}
\textit{Свидетельство:} \texttt{nt!ProbeForRead} --- проверка выравнивания
(\texttt{tst x8,x0}) и диапазона против константы \texttt{0x7FFFFFFF0000}
(\texttt{mov x8,\#0x7FFFFFFF0000}; \texttt{cmp x9,x8}; \texttt{ccmpls}), затем
принудительный fault по пробуемому адресу (\texttt{ldr w8,[x8]});
\texttt{nt!ProbeForWrite} --- read/write-touch (\texttt{ldrsb}/\texttt{strb})
через границы страниц. Гейт по \texttt{PreviousMode} находится в вызывающей
Nt-функции, а не в самой \texttt{Probe*}: в \texttt{nt!NtQueryInformationProcess} ---
\texttt{ldr x8,[xpr,\#0x988]}; \texttt{ldrsb w21,[x8,\#0x252]} (чтение
\texttt{PreviousMode}); \texttt{cbnz w21,...} (ветвление в user-путь с пробингом
через \texttt{0x7FFFFFFF0000}).

\zschema{ProbeRead}{
ptr? : ADDR \\
len? : \Znum
}{
ptr? + len? \leq MMUserProbe
}

\subsection{Копирование аргументов: Input Set}
\zaxdef{ Number : SSN \fun \Znum }{ \text{--- число доп. аргументов на user-стеке} }
\zschema{ArgCopy}{
ssn? : SSN \\
n!   : \Znum
}{
n! = Number(ssn?)
}
\textit{Свидетельство:} счётчик из \texttt{Number}-таблицы управляет computed
branch \texttt{adr x8,CopyEnd; sub x10,x8,x10,lsl\#3; br x10} в лестницу
\texttt{ldr/str} (\texttt{nt!KiSystemServiceCopyStart}) --- копируется ровно
столько qword с user-стека, сколько декларировано во входном множестве вызова.

\subsection{Атом syscall на ARM64 --- SVC}
На ARM64 атом системного вызова (вместо x86 \texttt{sysenter}/\texttt{syscall})
--- инструкция \texttt{SVC}. Цепочка входа разрешена:
\texttt{SVC}~$\to$~\texttt{nt!HvlUserSyntheticExceptionHandler} (вектор
lower-EL/AArch64, trap-фрейм 0x370)~$\to$~\texttt{nt!KiConfigPointerAuthKernelEntry}
(конфигурация PAC на входе)~$\to$~\texttt{nt!KiBuildTrapFrame}~$\to$
\texttt{nt!KiSyntheticException}~$\to$~\texttt{nt!KiSystemService}.

\subsection{PAN/UAO --- не используются (отрицательное заключение)}
На данном билде PAN/UAO в тракте syscall не применяются. Проверены конфигураторы
PAC на входе/выходе (\texttt{nt!KiConfigPointerAuthKernelEntry},
\texttt{nt!KiSystemServiceExit}) и сами функции syscall --- ни одного
\texttt{msr pan}/\texttt{msr uao}/\texttt{ldtr}. Копирование user-стека и пробинг
выполняются обычными \texttt{ldr}/\texttt{str}. Разделение user/kernel здесь
обеспечивается \emph{программно}: гейт \texttt{PreviousMode}~+~
\texttt{ProbeForRead/Write}~+~граница \texttt{MM\_USER\_PROBE\_ADDRESS}; отказы при
user-доступе ловит SEH-обработчик \texttt{nt!KiSystemServiceHandler}~$\to$
\texttt{nt!RtlUnwindEx} (для fault-PC в диапазоне
\texttt{KiSystemServiceExit..CopyEnd}).

\subsection{Контроль цели косвенного вызова (CFG/CET)}
В \texttt{nt!KiTrackSystemCallExit} перед \texttt{blr x15} вызывается
\texttt{nt!KscpCfgCheckUserCallTargetEs} --- проверка цели вызова по конфигурации
CFG (Control Flow Guard): косвенный вызов санкционируется отдельно, поверх
PAC/BTI. Дополнительный механизм целостности потока управления.

\subsection{W\^{}X и очистка состояния}
\textit{Свидетельство:} кодовая страница \texttt{nt!NtClose} --- PDE
\texttt{-RXGA-K-LV} (исполняемая, без~W $\Rightarrow$ W\^{}X). На выходе из
системного вызова ядро обнуляет SIMD v0--v31 и x1--x15 перед \texttt{eret}
(DFI: отсутствие утечки данных ядра через регистры).

\section{Теоремы}

\begin{thm}[Корректность диспетчеризации]
Ограниченный, присутствующий в таблице SSN разрешается в nt-обработчик.
\[
\vdash\; \forall\, ServiceTable;\; Dispatch \,@\; handler! \in NtCode
\]
\textit{Свидетельство:} \texttt{KiServiceTable[0]} $\to$ \texttt{nt!NtAccessCheck},
$[1]\to$ \texttt{nt!NtWorkerFactoryWorkerReady}.
\end{thm}

\begin{thm}[Отклонение вне диапазона]
Любой SSN не меньше лимита даёт верифицированный код ошибки.
\[
\vdash\; \forall\, ServiceTable;\; InvalidService \,@\; status! = InvalidSvcEC
\]
\end{thm}

\begin{thm}[Принудительная целостность]
Отображение read-only вызывает отказ при любой записи на страницу таблицы.
\[
\vdash\; \forall\, ServiceTable;\; TableIntegrity \,@\;
\Protect(\PageOf(base)) = ReadOnly \;\Rightarrow\; \PageOf(base) \in WriteFault
\]
\end{thm}

\begin{thm}[DFI исключает AVM]
При выполнении DFI ни одна пара (элемент, адрес) не удовлетворяет предикату
обнаружения.
\[
\vdash\; DFI \;\Rightarrow\; \neg \bigl(\exists\, e : FlowElem;\; ea : EA \,@\; AVMDetected(e,\; ea)\bigr)
\]
\end{thm}
\begin{sketch}
Раскрывая определения: $DFI$ даёт $(e \mapsto ea)\in Accesses \Rightarrow ea \in CS \cup IS(e)$,
что прямо противоречит посылке $ea \notin CS \cup IS(e)$ из~$AVMDetected$. \qed
\end{sketch}

\begin{thm}[S-route удерживает управление секвенсора]
После S-route над возвратным атомом слот возврата ядра не равен исходному,
поэтому управление после атома не может уйти в API эмулятора.
\[
\vdash\; \forall\, SRoute \,@\; ts.retSlot' \neq ts.retSlot
\]
\end{thm}
\begin{sketch}
$ts.retSlot' = STUB$, причём $STUB$ контролируется визором, откуда
$STUB \neq saved! = ts.retSlot$. \qed
\end{sketch}

\begin{thm}[Целостность возврата по PAC]
Адрес возврата, подписанный ключом процесса, нельзя подменить на произвольный
адрес без отказа аутентификации.
\[
\vdash\; \forall\, PACSign;\; p? : Process \,@\;
PACKeyOf(p?) = k? \;\Rightarrow\; \forall\, a \neq lr? \,@\; Auth(lr!,\; k?) \neq a
\]
\end{thm}

\begin{thm}[W\^{}X]
Исполняемые страницы ядра недоступны для записи.
\[
\vdash\; \forall\, a : NtCode \,@\; \Protect(\PageOf(a)) = ReadOnly \;\land\; Exec(\PageOf(a))
\]
\end{thm}

\begin{thm}[Граница user/kernel]
Любая попытка probes диапазоном, выходящим за \texttt{MM\_USER\_PROBE\_ADDRESS},
отклоняется (fault).
\[
\vdash\; \forall\, ProbeRead \,@\; (ptr? + len? > MMUserProbe) \;\Rightarrow\; (ptr? + len? \in WriteFault)
\]
\end{thm}

\section{Таблица соответствия понятий}
\begin{longtable}{@{}p{0.27\textwidth} p{0.34\textwidth} p{0.33\textwidth}@{}}
\toprule
Понятие \emph{pfi.pdf} & Схема / определение Z & Якорь в ядре (верифицировано) \\
\midrule
Секвенция $Cf$ против потока $Xf$ & \texttt{Sequencing}, \texttt{Diverges} & буфер визора против \texttt{blr x11} \\
Атом & \texttt{ATOM} (свободный тип) & шлюз \texttt{syscall/sysenter} в \texttt{KiSystemService} \\
TS (состояние задачи) & \texttt{TS} & trap-фрейм, prevMode \texttt{\_KTHREAD+0x252} \\
CS / IS / EA / P & компоненты \texttt{PFG} & входы декодирования \texttt{KiServiceTable} \\
Инвариант DFI & \texttt{DFI} & \texttt{ProbeForRead/Write} (prevMode=User) \\
IDP + анклав & \texttt{Redirect}, $enclave$, $\delta$ & со стороны визора; ядерный аналог --- read-only таблица \\
Обнаружение AVM & \texttt{AVMDetected} & критерий рассогласования InputSet \\
S-route & \texttt{SRoute}, \texttt{RestoreReturn}, \texttt{STUB} & \texttt{[sp,\#0x50]} retSlot, \texttt{KiSystemServiceCopyEnd+0x38} \\
Диспетчерская таблица & \texttt{ServiceTable}, \texttt{Dispatch}, \texttt{Decode} & \texttt{KiServiceTable}, $\Shift(b,\cdot\div 16)$ \\
Лимит сервисов & \texttt{ServiceTable.limit} $=489$ & \texttt{KiServiceLimit} $= 0\times1E9$ \\
Неверный сервис & \texttt{InvalidService} & $0\times C000001C$ \\
Целостность таблицы & \texttt{TableIntegrity}, \texttt{\textbackslash Protect} & PDE \texttt{-R-GA-K-LV} (read-only large page) \\
Наблюдение атомов & \texttt{ObserveAtom}, \texttt{enabled} & \texttt{KiTrackSystemCallEntry/Exit} (бит~0), \texttt{+0x252} \\
Целостность указателей (PAC) & \texttt{PACSign}, \texttt{PACContextSwitch} & \texttt{pacibsp}, \texttt{APDBKey}, \texttt{SCTLR\_EL1.EnIB} \\
Возврат в R3 / S-route & \texttt{SystemCallReturn} (\texttt{ELR\_EL1}) & \texttt{msr ELR\_EL1,[sp,\#0x140]}; \texttt{eret} \\
Preflight & \texttt{KiPreflightReturnToUserMode} & проверка перед возвратом в~R3 \\
Теневые/фильтр.\ таблицы & \texttt{ShadowServiceTable} & Shadow(win32k~1493)/Filter; \texttt{tst} per-thread \\
BTI / W\^{}X & \texttt{Exec}, \texttt{\textbackslash Protect} & PDE \texttt{-RXGA-K-LV}; \texttt{pacibsp} как landing pad \\
Очистка состояния & (гигиена / DFI no-leak) & v0--v31, x1--x15 $\to 0$ перед \texttt{eret} \\
Граница user/kernel (DFI) & \texttt{ProbeRead}, \texttt{MMUserProbe} & \texttt{ProbeForRead/Write}, \texttt{0x7FFFFFFF0000} \\
Input Set (копирование арг.) & \texttt{ArgCopy}, \texttt{Number} & \texttt{br x10} в лестницу \texttt{ldr/str}, \texttt{CopyStart} \\
Атом syscall (ARM64) & \texttt{SVC} $\to$ \texttt{HvlUserSyntheticExceptionHandler} $\to$ \texttt{KiSystemService} & вместо x86 \texttt{sysenter}/\texttt{syscall} \\
PAN/UAO & --- (не используется) & программный гейт: PreviousMode + Probe + \texttt{MM\_USER\_PROBE\_ADDRESS} \\
SEH syscall & \texttt{KiSystemServiceHandler} $\to$ \texttt{RtlUnwindEx} & fault при user-доступе $\to$ исключение \\
Входная конфигурация PAC & \texttt{KiConfigPointerAuthKernelEntry} & ключи \texttt{[+0x8F0]}, \texttt{EnIB} \texttt{[+0x880]} bit~2 \\
PAC: аутентификация & \texttt{Auth} & \texttt{autibsp} перед \texttt{ret} (\texttt{KiTrackSystemCallExit}) \\
DFI: гейт PreviousMode & (Nt-вызывающий) & \texttt{ldrsb [+0x252]}; \texttt{cbnz} в \texttt{NtQueryInformationProcess} \\
CFG (цель вызова) & --- & \texttt{KscpCfgCheckUserCallTargetEs} перед \texttt{blr} \\
\bottomrule
\end{longtable}

\vfill\noindent\small\textit{Конец спецификации.}
\end{document}