Разработка медиатора¶

Задача медиатора — построить «модельную» трассу. Это трасса, которая повторяет собранную монитором трассу, но вместо системных сущностей определяет и использует модельные сущности.

Модельная трасса состоит из последовательности событий модели с указанием параметров и ожидаемое значение охранного условия события (истина или ложь).

Соответствие между трассами такое:

событиям соответствуют операции в трассе монитора;
параметрам события соответствуют аргументы операции, результаты операции, части состояния;
ожидаемому значению охранного условия соответствует значению кода завершения операции (например, 0 означает истинное значение охранного условия, не-0 означает ложное значение).

Интерфейсы классов¶

Главный класс медиатора — это класс TraceTranslator. Доступ к нему должен осуществляться так: from mediator import TraceTranslator. Для этого можно создать модуль mediator.py в модельной workspace folder и поместить туда этот класс. Если структура медиатора более сложная, можно сделать mediator именем пакета и в __init__.py указать доступ до имени класса TraceTranslator. Например, если TraceTranslator размещен в модуле translator.py внутри пакета mediator, то в __init_.py надо написать:

from .translator import TraceTranslator

Класс TraceTranslator должен содержать:

конструктор;
методы, соответствующие системным операциям.

Конструктор класса TraceTranslator должен иметь 3 параметра:

потребитель модельной трассы (модельная трасса не строится как структура в памяти, а передается поэлементно в потребитель)
начальное окружение трассы
машина

В коде это будет выглядеть так:

from typing import Any
from anis.stages.mediator import ModelTraceConsumer
from anis.model.machine import Machine

class TraceTranslator:

  def __init__(self, model_trace: ModelTraceConsumer, initial: dict[str, Any], m: Machine):
    self._model_trace = model_trace
    self._m = m
    ...

Потребитель модельной трассы — это библиотечный класс ModelTraceConsumer. Его определение такое:

from typing import Protocol, Callable, Any
from anis.model.lazy import Event

class ModelTraceConsumer(Protocol):
  def add(self, event_function: Callable[..., Event], *, expected: bool, skip_coverage: bool=False, **args: Any):
     ...

Конкретная реализация класса ModelTraceConsumer будет подставлена самим АНИС.

Метод add класса ModelTraceConsumer добавляет новый элемент модельной трассы. Его аргументы:

event_function — событие (представляется функцией из модуля пакета anis.model.events, сгенерированной для события);
args — пары «параметр=значение»;
expected — ожидаемое значение охранного условия события;
skip_coverage — включать ли это событие в покрытие по модели.

Конструктор класса TraceTranslator должен оттранслировать начальное окружение в начало модельной трассы. Соответствующие элементы должны быть добавлены в model_trace.

Методы класса TraceTranslator соответствуют операциям из трассы и должны дополнять модельную трассу соответствующими элементами. К методам предъявляются следующие требования:

Название метода должно совпадать с именем соответствующий операции.
Аргументы метода должны быть типизированы при помощи типовых подсказок (type hints), метод должен возвращать None
Одним из аргументов должен быть retval: int, это целочисленный код завершения операции, остальные аргументы должны быть атрибутами операции в трассе, типы значений атрибутов операции должны совпадать с типовыми подсказками аргументов метода
Если атрибут операции является опциальным (например, если операция создания файла неуспешна, то нет информации о новом файле, так как файл не создан), то типовая подсказка должны быть Optional[T]

Пример метода:

from anis.model.events.fchdir import fchdir

class TraceTranslator:
  ...

  def fchdir(self, *, fd: int, pid: int, retval: int):

     self._model_trace.add(fchdir, fd=fd, proc=pid, expected=(retval == 0))

В этом примере транслируется операция fchdir. Она соответствует событию fchdir. У события есть параметры fd и proc. Параметр-звездочка помогает не ошибиться при вызове метода, так как требует явного указания имени аргумента рядом со значением аргумента.

Для каждой трассы создается свой экземпляр класса TraceTranslator. Он используется так:

from mediator import TraceTranslator
from anis.model.machine import Machine
from anis.stages.systrace import Trace

def check_trace(trace: Trace, m: Machine):
    model_trace = ModelTraceChecker(m)
    tt = TraceTranslator(model_trace, trace.initial, m)
    for operation in trace.operation:
        getattr(tt, operation.name)(operation.args, retval=operation.ret)

Методика разработки медиатора¶

Составить отображение реальных операций на события модели; отдельные ветви функциональности операции могут быть представлены отдельными событиями
Разделить параметры событий на те, что соответствуют аргументам операции, и те, которые соответствуют результатам операции
Перечислить все модельные сущности
Составить однозначное соответствие между модельными сущностями и реальными данными
Для модельных событий составить множество реальных данных, необходимых для получения всех параметров событий
В итоге, для каждой операции известны два множества аргументов: те, которые есть в трассе, и те, которые нужны для вычисления параметров; если не все аргументы второго множества присутствуют в первом множестве, выполнить следующий шаг
Составить отображение аргументов первого множества и, возможно, аргументов предыдущих элементов трассы на аргументы второго множества; если аргументы предыдущих элементов трассы необходимы, включить их в список данных, составляющих состояние медиатора, составить алгоритмы инициализации и наполнения состояния медиатора

После того, как все эти шаги выполнены, нужно запрограммировать полученные алгоритмы и структуры данных.

Пример применения методики¶

Разрабатывается медиатор для модели ядра Linux. В модели описываются операции open() и close().

В модели операция open() представлена двумя событиями: open_create и open_exists. Событие open_create означает операцию open() для несуществующего файла, а событие open_exists – для существующего файла. Операция close() представлена одним событием close. Мы описали соответствие операций и событий и, тем самым, выполнили первый шаг методики.

У события open_create следующие параметры:

proc — процесс, вызывающий open
parent — родительская директория создаваемого файла
file — создаваемый файл
name — имя создаваемого файла
flags — флаги, с которыми будет создан файл
mode — права доступа, переданные в качестве параметра open
fd — файловый дескриптор, который вернет open
fdNumber — номер файлового дескриптора
group — группа, которую получил файл
perms — права доступа, которые получил файл

На следующем шаге нужно разделить параметры события на два множества:

к аргументам операции open() относятся параметры proc, parent, name, flags, mode
к результатам операции open() относятся параметры file, fd, fdNumber, group, perms

На следующем шаге нужно перечислить модельные сущности, сопоставим параметрам событий их несущие множества (для этого смотрим на типы параметров из охранных условий события):

PROCS: proc
FILES: parent, file
STRINGS: name
OPEN_FLAGS ∊ POW(INT): flags
POW(PERMISSIONS): mode, perms
FILE_DESCRIPTORS_EXTENDED: fd
GROUPS: group

На следующем шаге составляем однозначное соответствие между реальными данными и модельными:

модельные	реальные
`PROCS`	`pid: int` (идентификатор процесса)
`FILES`	`(dev: int, ino: int)` (номер устройства, номер inode)
`STRINGS`	`text: str` (сам текст)
`POW(INT) (OPEN_FLAGS)`	`flag: int` (одна из констант флагов)
`PERMISSIONS`	`perm: int` (одна из констант прав на файл)
`FILE_DESCRIPTORS_EXTENDED`	`(pid: int, fd: int)` (идентификатор процесса, номер файлового дескриптора)
`GROUPS`	`gid: int` (номер группы)

На следующем шаге составляем множество реальных данных, необходимых для параметров события. Это множество уже представлено в таблице выше.

На следующем шаге надо сравнить аргументы операции и необходимые данные с предыдущего шага:

аргументы операции	необходимые данные для события
`pathname: str` `mode: int` `flags: int`	`pid: int` `file_dev: int, file_ino: int` `parent_dev: int, parent_ino: int` `file_name: str` множество битов из `flags: int` множество битов из `mode: int` множество битов из `perms: int` `fd: int` `gid: int` (созданного файла)

аргументы операции

необходимые данные для события

pathname: str

mode: int

flags: int

pid: int

file_dev: int, file_ino: int

parent_dev: int, parent_ino: int

file_name: str

множество битов из flags: int

множество битов из mode: int

множество битов из perms: int

fd: int

gid: int (созданного файла)

Сравнивая эти данные, видим много расхождений. По каждому из них нужно принять решение об их источниках: в трассе, генерируемой монитором, или в состоянии медиатора (то есть среди атрибутов предыдущих операций в трассе). В таблице ниже представлено одно из решений. Распределение в нем сделано так, чтобы требования к монитору были минимальными.

Данные	Источник
`pid: int`	Монитор
`file_dev: int, file_ino: int`	Монитор
`parent_dev: int, parent_ino: int`	Медиатор (на основе `pathname` и сохраненного отображения путей в `(dev, ino)`)
`file_name: str`	Медиатор (на основе `pathname`)
множество битов из `flags: int`	Медиатор (на основе `flags` и констант машины)
множество битов из `mode: int`	Медиатор (на основе `mode` и констант машины)
множество битов из `perms: int`	Монитор (`perms`) и Медиатор (на основе `perms` и констант машины)
`fd: int`	Медиатор (равно `retval`)
`gid: int` (созданного файла)	Монитор

Получаем следующие структуры данных для состояния медиатора:

отображение pid: int в элементы PROCS
отображение gid: int в элементы GROUPS
отображение пар (dev: int, ino: int) в элементы FILES
отображение name: str в элементы STRINGS
отображение pathname: str в пары (dev: int, ino: int)
отображение одиночного флага открытия файлов в константу из OPEN_FLAGS
отображение одиночного флага режима (прав) в константу из PERMISSIONS
отображение пар (pid: int, fd: int) в элементы FILE_DESCRIPTORS_EXTENDED

Спроектируем алгоритмы работы с этими структурами данных:

отображение pid: int в элементы PROCS:
- в конструкторе отображение инициализировать пустым и добавить в отображение константы типа PROCS (для каждой нужно восстановить значение pid)
- в событиях, где создается процесс, добавить отображение pid в m.ProcsItem()
- в событиях, где завершается процесс, удалить ключ pid из отображения
- в событии, где используется существующий процесс (например, в open_create), получить объект класса m.ProcsItem как значение по ключу pid
отображение gid: int в элементы GROUPS
- аналогично предыдущей структуре данных
отображение пар (dev: int, ino: int) в элементы FILES
- аналогично предыдущей структуре данных
отображение text: str в элементы STRINGS
- в конструкторе отображение инициализировать пустым и добавить в отображение константы типа STRINGS (для каждой нужно восстановить значение text)
- в событии получить объект класса m.StringsItem как значение по ключу text, а если ключа нет, то предварительно создать новый экземпляр класса m.StringsItem и сохранить его в отображение для клююча text
отображение pathname: str в пары (dev: int, ino: int)
- аналогично структуре данных про процессы
отображение одиночного флага открытия файлов в константу из OPEN_FLAGS
- в конструкторе отображение инициализировать отображением всех одиночных флагов (целых чисел) в константы из множества OPEN_FLAGS
- при запросе множества одиночных флагов (битового вектора) выделить отдельные биты-флаги, получить для них соответствующие константы из OPEN_FLAGS и составить множество из полученных констант
отображение одиночного флага режима (права) в константу из PERMISSIONS
- аналогично предыдущей структуре данных
отображение пар (pid: int, fd: int) в элементы FILE_DESCRIPTORS_EXTENDED
- аналогично структуре данных про процессы

Программная реализация медиатора¶

Отображения данных необходимо запрограммировать в классе TraceTranslator вручную. Для этого удобно использовать dict. Для отображений в элементы несущих множеств удобно использовать defaultdict (конструктор класса несущего множество, при помощи которого создаются элементы несущих множеств,, не имеет аргументов).

from collections import defaultdict
from typing import Any, Optional
from os.path import basename, dirname, isabs

from anis.model.machine import Machine
from anis.model.events.open_exists import open_exists
from anis.model.events.open_create import open_create
from anis.stages.mediator import ModelTraceConsumer


class TraceTranslator:

  def __init__(self, model_trace: ModelTraceConsumer, initial: dict[str, Any], m: Machine):
    self._model_trace = model_trace
    self._m = m
    # empty initialisation using defaultdict
    self._model_procs = defaultdict[int, m.ProcsItem](m.ProcsItem)
    # add constant
    self._model_procs[0] = m.INIT
    ...
    # empty initialisation without defaultdict
    self._inodes = dict[str, tuple[int, int]]()
    # add initialisation (root info should be captured by monitor)
    self._inodes['/'] = (initial.root_dev, initial.root_ino)

  def open(self, *, pathname: str, flags: int, mode: int, pid: int,
          dev: Optional[int], ino: Optional[int],
          uid: Optional[int], gid: Optional[int],
          perms: Optional[int], retval: int) -> None:

     if not isabs(pathname):
         raise ValueError('Relative pathname is unsupported yet')

     # append model trace
     if pathname in self._inodes:
         self._model_trace.add(open_exists,
             _proc = self._model_procs[pid],
             _parent = self._model_files[self._inodes[dirname(pathname)]],
             _file = self._inodes[pathname],
             _name = self._model_strings[basename(pathname)],
             _flags = self._translate_open_flags(flags),
             _fd = self._model_fd[(pid, retval,)] if retval >= 0 else None,
             _fdNumber = retval if retval >= 0 else None,
             expected = retval >= 0,)
     else:
         self._model_trace.add(open_create,
             _proc = self._model_procs[pid],
             _parent = self._model_files[self._inodes[dirname(pathname)]],
             _file = self._model_files[(dev, ino)] if ino is not None else None,
             _name = self._model_strings[self._inodes[basename(pathname)]],
             _flags = self._translate_open_flags(flags),
             _mode = self._translate_permissions(mode),
             _fd = self._model_fd[(pid, retval,)] if retval >= 0 else None,
             _fdNumber = retval if retval >= 0 else None,
             _group = self._model_groups[gid] if gid is not None else None,
             _perms = self._translate_permissions(perms) if perms is not None else None,
             expected = retval >= 0,)

     # update mediator state (self._inodes because of file creation)
     if retval >= 0:
         if pathname not in self._inodes:
             if dev is None or ino is None:
                 raise ValueError('Not enough data in the trace')
             self._inodes[pathname] = (dev, ino)

defaultdict позволяет сократить те фрагменты кода, где нужно проверять наличие ключа и в случае отсутствия создавать новое отображение.

Приведенный пример подлежит уточнению. Он предполагает, что пути к файлам являются абсолютными. Для устравнения этого ограничения нужно дополнить состояние медиатора отображением процессов в их текущие рабочие директории. Для этого отображения нужно выбрать структуру данных и составить алгоритмы работы аналогично уже рассмотренным структурам данных.

Другим событиям могут потребоваться атрибуты файла, которые известны в трассе только в момент создания файлов. Поэтому состояние медиатора будет еще расширено отображением файлов (номера устройства и индексного дескриптора) в кортеж с атрибутами.

Для операций, которые получают на вход файловые дескрипторы вместо путей (например, openat или fchdir), потребуется отображение файлового дескриптора в файл (номер устройства и индексного дескриптора).

Тем самым, состояние медиатора может быть довольно сложным. Поэтому имеет смысл оформить его в виде отдельного класса с удобным интерфейсом.

Есть еще одно наблюдение: одни и те же события могут добавляться в модельную трассу в нескольких методах медиатора, причем код добавления идентичный (вызов метода add с трансляцией аргументов в модельные сущности при помощи отображений). Поэтому имеет смысл отделить это добавление в свой класс.