Применяем TLA+ на практике

Привет, Хабр! Меня зовут Сергей, я работают в компании InfoWatch разработчиком на продукте ARMA Стена (NGFW). Подробнее о том, что такое ARMA Стена, можно прочитать тут.

В этой статье я хочу поделиться опытом применения метода формальной верификации в решении практической бизнес-задачи.

Сразу оговорюсь, что в статье используется TLA+, без введения в инструмент, чтобы не увеличивать объём статьи. Подробнее про инструмент вы можете почитать на сайте создателя, тут и тут. Необходимые объяснения даются по ходу изложения.

Статья состоит из двух частей:

1. Что такое формальная верификация и где она применятся

2. Решение бизнес-задачи в NGFW

Начинаем!

Что такое формальная в��рификация

Верификация — это процесс, при котором подтверждается, что заданные требования полностью выполнены.

Уточняя для программ — это процесс, при котором мы подтверждаем, что код программы выполняет то, что заявлено для него по спецификациям. Например, для программы, которая авторизует пользователей, должны быть тесты, которые проверят, что она действительно этих пользователей авторизует.

Верификация использует различные методы для проверки этих требований:

• статические (анализаторы)

• динамические (тестирование)

• формальные (проверка моделей)

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

Нам же больше интересны именно формальные методы, которые также называются формальной верификацией (или методами формальной верификации).

Формальная верификация — это процесс, при котором доказывается или опровергается корректность алгоритма по заданной спецификации.

Используемым языком спецификации является математика. С её помощью мы описываем сам алгоритм и его свойства, которые требуется доказать или опровергнуть. Каким образом происходит доказательство — зависит от конкретного метода формальной верификации.

В этой статье мы рассмотрим метод Model-checking и связанный с ним инструмент TLA+, который в своей основе использует конечный автомат для проверки алгоритма по спецификации. Схематично процесс ФВ методом Model-checking можно представить себе таким образом (рисунок ниже).

Инструмент TLA+ был разработан Лесли Лэмпортом для верификации параллельных систем, но при этом может использоваться и для верификации алгоритмов в целом. На официальном сайте есть раздел, посвящённый учебным материалам по этому инструменту.

Говоря о том где именно применяется TLA+, то зарубежом это Intel, Amazon, Microsoft, OpenComRTOS. А в России это Yandex, ITooLabs.

Если говорить о формальны методах вообще, то на GitHub есть репозиторий, в котором собраны примеры использования в разных компаниях (включая российские).

Решаем задачу в NGFW

Постановка задачи

Итак, заказчик попросил реализовать функционал, который позволяет администратору блокировать / разблокировать пользователей в заданный период времени. Например, если сотрудник увольняется, то администратор задаёт дату блокировки — его последний рабочий день — и начиная с этого момента учётная запись блокируется навсегда. Краткая формулировка этой же задачи выглядит так:

Реализовать механизм блокировки / разблокировки пользователей в указанный период времени

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

Исследуем задачу

Казалось бы, всё звучит довольно просто? Можно уже сразу представить в голове такое решение:

cron, который дёргает скрипт, который уже блокирует / разблокирует пользователей

Или можно прийти к решениям, которые используют pam_time или сторонний пакет. Однако, при детальном их изучении мы выясним, что pam_time ограничивает время по дням и времени. А сторонний пакет мало того, что потребует затянуть новые зависимости, так и ещё расширит поверхность атаки, если в нём будут уязвимости.

Поэтому первое решение, которое пришло нам в голову, вроде бы неплохое, но требует тщательного обдумывания. Давайте найдём алгоритм, который лежит в основе задачи. Механизм подразумевает то, что нам надо работать со временем, то есть:

• У нас есть текущий момент времени

• У нас есть период блокировки

С первым всё понятно, а со вторым у нас такая типология:

• полный период (когда указаны его начало и конец)

• неполный период (когда указано только начало или только конец)

В зависимости от времени и периода, механизм принимает решение:

• блокировать

• разблокировать

• ничего не делать

И всё это совершается над пользователями, то есть мы имеем список пользователей.

Что получаем

Уже можно чуть-чуть формализовать исходную задачу.

Механизм блокировки / разблокировки работает с:

• текущим временем

• временными периодами

• списком пользователей

Механизм блокировки / разблокировки выполняет действия:

• блокировать

• разблокировать

• ничего не делать

И данный механизм будет запускаться регулярно с помощью cron.

Ограничения

Теперь подумаем об ограничениях, которые накладываются на задачу:

• В системе должен быть хотя бы один пользователь

• В нашей системе есть суперадминистратор, он никогда не должен быть заблокирован и его нельзя заблокировать

• Нужно проверять интервалы блокировки

  • Для полного периода

    • Задано начало и окончание блокировки

    • Начало всегда меньше окончания

  • Неполный период

    • Может быть задано только начало блокировки

    • Может быть задано только окончание блокировки

• Нужно гарантировать

  • что в период блокировки пользов��тель заблокирован

  • что вне периода блокировки пользователь разблокирован

И вот мы можем уже сформулировать алгоритм. С периодичностью (скажем, 1 минута) выполнять следующие шаги:

1. получить список пользователей

2. для каждого пользователя

   1. проверить ограничения

   2. проверить период блокировки

      1. выполнить действие

Раскроем подробнее проверки периода блокировки.

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

Рассмотрим на примере неполного периода, когда у нас текущее время, например, 2015.01.01 12:00, а окончание периода блокировки — 2017.01.01 13:00. Что это значит? Что до времени окончания блокировки пользователь должен быть заблокирован, а значит, наш механизм должен его блокировать до этого времени включительно. Понимаете, да? Наглядно это можно представить прямой, на которой движутся точки.

Ещё раз, по пунктам, что будет делать механизм для каждого из случая на прямой:

1. блокировка

2. блокировка

3. ничего

Полностью уяснив пример выше, аналогичное проделаем для неполного периода с началом блокировки и для полного периода. См соответствующие картинки ниже.

Действия механизма

1. ничего

2. блокировка

3. блокировка

Действия механизма

1. ничего

2. блокировка

3. блокировка

4. блокировка

5. разблокировка

Как видно, мы описали именно алгоритм, без привязки к операционной системе и деталям технической реализации. Всё, что у нас есть, это базовая идея алгоритма, его ограничения и свойства.

Написание спецификации

Теперь, получив чёткое понимание алгоритма, переложим его на язык спецификации TLA+, используя математические определения, и попросим модель доказать или опровергнуть наши измышления. Спецификация будет написана на языке PlusCal, который выглядит как Pascal, но умеет описывать математические формулы.

Этапы написания спецификации:

1. Дать базовые определения

   1. Классы

   2. Статусы

   3. Пользователи

2. Описать логику работы времени

   1. Имитируем минуты

   2. Делаем возможность параметризации

3. Описать механизм проверки

   1. Полный интервал

   2. Неполный интервал

4. Описать asserts и инварианты

5. Добавить в алгоритм

Перед тем как мы приступим, кратко расскажу, из чего состоит TLA+ (см. рисунок ниже). TLA — основной язык спецификации, на котором описывается алгоритм. TLC — программа, которая запускает проверку модели по описанной спецификации TLA. 
PlusCal — упрощённый pascal-подобный язык, который транслируется в TLA. Мы будем использовать упрощённый язык, чтобы было чётко виден наш алгоритм (собственно, он и был придуман для того, чтобы писать спецификации было легче).

Первый этап

Здесь мы даём базовые определения тому, что у нас есть в системе и с чем по факту работает наш алгоритм (пользователи и время). Но при этом мы также добавляем некоторые особенности самого NGFW. Из математики нам нужно вспомнить совсем немного:

• множества — набор элементов с общим признаком

• предикаты — высказывание, которое либо истинно, либо ложно

• /\ - коньюнкция (И)

• \/ - дизьюнкция (ИЛИ)

С помощью множеств определим классы пользователей в системе (определяет набор доступных команд) и статусы этих пользователей.

Затем определим переменную now, которая будет выступать нашим счётчиком времени.

И, наконец, определим список пользователей с такими параметрами:

• имя пользователя

• класс

• статус

• период

Периоды представляет собой минуты блокировки, например, 2 и 8 минут. В этот период пользователь будет заблокирован. Другой пример периода <0, 7>, то есть пользователь будет уже заблокирован до 7-й минуты включительно, после чего он будет разблокирован.

---- MODULE lockout ----
EXTENDS Naturals, TLC, Sequences, Integers
  
(* Наши множества, которые приоткрывают NGFW *)
Classes == {"NGFW_Super_Administrators", "NGFW_Administrators", "NGFW_Security"}
Status == {"locked", "unlocked"}
  
(* --algorithm lockout
  
variables
    now = 0, (* Переменная счётчик времени *)
    userList = << (* Список пользователей *)
        [name |-> "admin", class |-> "NGFW_Super_Administrators", status |-> "unlocked", period |-> <<8,9>>], {* Запись об одном пользователе *}
        [name |-> "test", class |-> "NGFW_Administrators", status |-> "unlocked", period |-> <<2,6>>],
        [name |-> "another", class |-> "NGFW_Administrators", status |-> "unlocked", period |-> <<0,7>>],
        [name |-> "security", class |-> "NGFW_Security", status |-> "unlocked", period |-> <<4,7>>],
        [name |-> "wow", class |-> "NGFW_Security", status |-> "unlocked", period |-> <<5,0>>]
    >>;
  
begin
    print "Hello World";
end algorithm; *)

Алгоритмическая часть проста пока, как две капли воды, выводим сообщение "Hello World".

Второй этап

Как же нам описать логику работы времени? Можно пойти трудным путём, которым я и пошёл изначально. Я описал много PlusCal-кода, который работал с датой и временем, но это оказалось так громоздко и неудобно, что я просто пришёл к мысли об обычном счётчике в цикле.

Всё, что нам надо, это условиться, что счётчик означает минуты, часы или дни, и просто увеличивать его до заранее заданного предела. Для этого объявим константу MAX_TIME, которая будет задаваться при запуске модели, а в алгоритмической части опишем обычный цикл-счётчик.

Метки movement, do, tick позволяет разделить этапы выполнения алгоритма на логические блоки.

---- MODULE lockout ----
EXTENDS Naturals, TLC, Sequences, Integers
  
CONSTANTS MAX_TIME
  
(* --algorithm lockout
  
variables
    now = 0,
    ...
  
begin
    movement:
        while now < MAX_TIME do
            do:
                print now;
            tick:
                now := now +1;
end algorithm; *)

Запустив модель, мы получим на экране просто числа. Можем возгордиться собой и сказать, что мы научились управлять временем!

Третий этап

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

• блокировка

• разблокировка

• ничего

Данные действия описаны в виде предикатов, которые на вход принимают данные о пользователи и меняют статус, кроме предиката NOTHING, который просто возвращает пользователя без изменений.

define
    (* Действия механизма блокировки *)
    LOCK(u) == [name |-> u.name, class |-> u.class, status |-> "locked", period |-> u.period]
    UNLOCK(u) == [name |-> u.name, class |-> u.class, status |-> "unlocked", period |-> u.period]
    NOTHING(u) == u
end define;

Перекладывая вышеописанное в алгоритмическую часть, получим следующее. Т.е. всего навсего вызываем другие процедуры, которые уже далее "разбираются" с пользователем.

---- MODULE lockout ----
EXTENDS Naturals, TLC, Sequences, Integers
  
(* --algorithm lockout
  
(* Наши ранние определения *)
  
define
    (* Действия механизма блокировки *)
    LOCK(u) == [name |-> u.name, class |-> u.class, status |-> "locked", period |-> u.period]
    UNLOCK(u) == [name |-> u.name, class |-> u.class, status |-> "unlocked", period |-> u.period]
    NOTHING(u) == u
end define;
  
begin
    movement:
        while now < MAX_TIME do
            check_users:
                while user_id <= Len(userList) do
                    check_period:
                        if userList[user_id].period[1] = 0 then (* Если задано только окончание блокировки *)
                            call check_stop_period(user_id);
                        elsif userList[user_id].period[2] = 0 then (* Если задано только начало блокировки *)
                            call check_start_period(user_id);
                        elsif userList[user_id].period[1] # 0 /\ userList[user_id].period[2] # 0 then (* Если задан полный период *)
                            call check_full_period(user_id);
                        end if;
                    inc:
                        user_id := user_id + 1;
                end while;
                user_id := 1;
            tick:
                now := now + 1;
        end while;
end algorithm; *)

Код процедуры для неполного периода только с началом.

procedure check_start_period(i)
begin
    (* Проверяем случаи
        1. now < start
        2. now = start
        3. start < now
    *)
    proc:
        if now < userList[i].period[1] then
            userList[i] := userList[i];
        elsif now = userList[i].period[1] then
            if ~IsSuperAdmin(userList[i]) then
                userList[i] := LOCK(userList[i]);
            end if;
        elsif userList[i].period[1] < now then
            if ~IsSuperAdmin(userList[i]) then
                assert UserIsLocked(userList[i]); (* Это наши гаранитии, о которых мы писали выше *)
            end if;
        end if;
    r:
        return;
end procedure;

Код процедуры для неполного периода только с окончанием.

procedure check_stop_period(i)
begin
    (* Проверяем случаи
        1. now < stop
        2. now = stop
        3. stop < now
    *)
    proc:
        if now < userList[i].period[2] then
            if ~IsSuperAdmin(userList[i]) then
                userList[i] := LOCK(userList[i]);
            end if;
        elsif now = userList[i].period[2] then
            if ~IsSuperAdmin(userList[i]) then
                userList[i] := UNLOCK(userList[i]);
            end if;
        elsif userList[i].period[2] < now then
            if ~IsSuperAdmin(userList[i]) then
                assert UserIsUnlocked(userList[i]); (* Это наши гаранитии, о которых мы писали выше *)
            end if;
        end if;
    r:
        return;
end procedure;

Код процедуры для полного периода.

procedure check_full_period(i)
begin
    (* Check cases
        1. now < start < stop
        2. now = start /\ start < stop
        3. start < now < stop
        4. start < now /\ now = stop
        5. start < stop < now
    *)
    proc:
        if now < userList[i].period[1] then
            userList[i] := userList[i];
        elsif now = userList[i].period[1] then
            if ~IsSuperAdmin(userList[i]) then
                userList[i] := LOCK(userList[i]);
            end if;
        elsif userList[i].period[1] < now /\ now < userList[i].period[2] then
            if ~IsSuperAdmin(userList[i]) then
                assert UserIsLocked(userList[i]); (* Это наши гаранитии, о которых мы писали выше *)
            end if;
        elsif now = userList[i].period[2] then
            userList[i] := UNLOCK(userList[i]);
        elsif userList[i].period[2] < now then
            if ~IsSuperAdmin(userList[i]) then
                assert UserIsUnlocked(userList[i]); (* Это наши гаранитии, о которых мы писали выше *)
            end if;
        end if;
    r:
        return;
end procedure;

Четвёртый этап

Поздравляю. Самый крупный этап завершён. Теперь остался самый этап, на котором мы формулируем ограничения и свойства для нашего алгоритма. Вспомним их:

• В нашей системе есть суперадминистратор, и он никогда не должен быть заблокирован и его нельзя заблокирвать

• В системе должен быть хотя бы один пользователь

• Нужно проверять интервалы блокировки

  • Для полного периода

    • Начало всегда меньше окончания

  • Неполный период

    • Может быть задано только начало блокировки

    • Может быть задано только окончание блокировки

• Нужно гарантировать

  • что в период блокировки пользователь заблокирован

  • что вне периода блокировки пользователь разблокирован

Для первого пункта напишем простой предикат, который используется в процедурах проверки периодов. Суть его проста — в нашем NGFW суперадмин идентифицируется как пользователь с именем admin и классом NGFW_Super_Administrators.

IsSuperAdmin(u) == u.name = "admin" /\ u.class = "NGFW_Super_Administrators"

Для четвёртого пункта опишем предикаты, которые будут выступать в роли asserts в процедурых проверки интервалов выше.

UserIsLocked(u) == u.status = "locked"
UserIsUnlocked(u) == u.status = "unlocked"

Сюда же ещё стоит добавить два предиката AllUsersUnlocked и ExistUsersUnlocked. Они появилсь уже в процессе, когда я писал спецификация. Суть их в том, что сформулировать для механизма блокировки следующее:

• перед тем как начнёт работать механизм блокировки, все пользователи разблокированы (это тот случай, когда система была установлена впервые)

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

Вот соответствующие определения ниже. Они будут выполняться до и после самого алгоритма блокировки. \A (for all) означает "для всех", \E (there exists) означает "существует".

AllUsersUnlocked == \A x \in 1..Len(userList): userList[x].status = "unlocked"
      
ExistUsersUnlocked == \E x \in 1..Len(userList): userList[x].status = "unlocked"

Отдельно поговорим об инвариантах. Инвариант это условие, которое должно быть истинным на протяжении всего времени выполнения алгоритма. Ключевыми инвариантами для нашего алгоритма являются ограничения:

• В системе должен быть хотя бы один пользователь

• В нашей системе есть суперадминистратор и он никогда не должен быть заблокирован

Для первого опишем следующее. Довольно всё просто, во время работы нашего алгоритма список не должен оказаться пустым.

UserListInvariant == userList /= <<>>

Для второго опишем следующ��е. Из всех пользователей выбираем admin и убеждаемся, что его статус unlocked. Если наш алгоритм вдруг заблокирует пользователя, то инвариант сразу же нарушится, и это выяснится во время выполнения модели. CHOOSE означает «выбрать элемент по заданному условию».

AdminAlwaysUnlockedInvariant ==
    LET
        Users == {userList[x]: x \in 1..Len(userList)}
        adminUser == CHOOSE x \in Users: IsSuperAdmin(x) = TRUE
    IN
        adminUser.status = "unlocked"

Ещё опишем чистно технический инвариант, что во время выполнения модели наши типы данных сохраняют консистентность. И, самое главное, что мы проверяем полный интервал.

TypeUserInvariant(u) ==
    /\ u.name \in STRING
    /\ u.class \in Classes
    /\ u.status \in Status
    /\ u.period[1] \in Int
    /\ u.period[2] \in Int
    /\ IF u.period[1] # 0 /\ u.period[2] # 0 THEN u.period[1] < u.period[2] ELSE TRUE
  
TypeInvariant ==
    /\ now \in Int
    /\ MAX_TIME \in Int
    /\ now <= MAX_TIME
    /\ \A x \in 1..Len(userList): TypeUserInvariant(userList[x]) = TRUE

Объединив все определения выше, получаем описанные ограничения, предикаты, утверждения и инварианты.

define
    (* Предикаты *)
    IsSuperAdmin(u) == u.name = "admin" /\ u.class = "NGFW_Super_Administrators"
  
    (* Утверждения *)
    AllUsersUnlocked == \A x \in 1..Len(userList): userList[x].status = "unlocked"
    ExistUsersUnlocked == \E x \in 1..Len(userList): userList[x].status = "unlocked"
    UserIsLocked(u) == u.status = "locked"
    UserIsUnlocked(u) == u.status = "unlocked"
  
    (* Инварианты *)
    UserListInvariant == userList /=  <<>>
  
    AdminAlwaysUnlockedInvariant ==
        LET
            Users == {userList[x]: x \in 1..Len(userList)}
            adminUser == CHOOSE x \in Users: IsSuperAdmin(x) = TRUE
        IN
            adminUser.status = "unlocked"
  
    TypeUserInvariant(u) ==
        /\ u.name \in STRING
        /\ u.class \in Classes
        /\ u.status \in Status
        /\ u.period[1] \in Int
        /\ u.period[2] \in Int
        /\ IF u.period[1] # 0 /\ u.period[2] # 0 THEN u.period[1] < u.period[2] ELSE TRUE
  
    TypeInvariant ==
        /\ now \in Int
        /\ MAX_TIME \in Int
        /\ now <= MAX_TIME
        /\ \A x \in 1..Len(userList): TypeUserInvariant(userList[x]) = TRUE
end define;

Пятный этап

Объединив все наши труды мы получаем спецификацию на алгоритм механизма блокировки/разблокировки пользователя для нашего NGFW.

---- MODULE lockout ----
EXTENDS Naturals, TLC, Sequences, Integers
  
CONSTANTS MAX_TIME
  
Classes == {"NGFW_Super_Administrators", "NGFW_Administrators", "NGFW_Security"}
Status == {"locked", "unlocked"}
  
(* --algorithm lockout
  
variables
    now = 0,
    userList = <<
        [name |-> "admin", class |-> "NGFW_Super_Administrators", status |-> "unlocked", period |-> <<8,9>>],
        [name |-> "test", class |-> "NGFW_Administrators", status |-> "unlocked", period |-> <<2,6>>],
        [name |-> "another", class |-> "NGFW_Administrators", status |-> "unlocked", period |-> <<0,7>>],
        [name |-> "security", class |-> "NGFW_Security", status |-> "unlocked", period |-> <<4,7>>],
        [name |-> "wow", class |-> "NGFW_Security", status |-> "unlocked", period |-> <<5,0>>]
    >>,
    user_id = 1;
  
define
    (* Действия механизма блокировки *)
    LOCK(u) == [name |-> u.name, class |-> u.class, status |-> "locked", period |-> u.period]
    UNLOCK(u) == [name |-> u.name, class |-> u.class, status |-> "unlocked", period |-> u.period]
    NOTHING(u) == u
  
    (* Предикаты *)
    IsSuperAdmin(u) == u.name = "admin" /\ u.class = "NGFW_Super_Administrators"
      
    (* Утверждения *)
    AllUsersUnlocked == \A x \in 1..Len(userList): userList[x].status = "unlocked"
    ExistUsersUnlocked == \E x \in 1..Len(userList): userList[x].status = "unlocked"
    UserIsLocked(u) == u.status = "locked"
    UserIsUnlocked(u) == u.status = "unlocked"
  
    (* Инварианты *)
    UserListInvariant == userList /=  <<>>
  
    AdminAlwaysUnlockedInvariant ==
        LET
            Users == {userList[x]: x \in 1..Len(userList)}
            adminUser == CHOOSE x \in Users: IsSuperAdmin(x) = TRUE
        IN
            adminUser.status = "unlocked"
  
    TypeUserInvariant(u) ==
        /\ u.name \in STRING
        /\ u.class \in Classes
        /\ u.status \in Status
        /\ u.period[1] \in Int
        /\ u.period[2] \in Int
        /\ IF u.period[1] # 0 /\ u.period[2] # 0 THEN u.period[1] < u.period[2] ELSE TRUE
  
    TypeInvariant ==
        /\ now \in Int
        /\ MAX_TIME \in Int
        /\ now <= MAX_TIME
        /\ \A x \in 1..Len(userList): TypeUserInvariant(userList[x]) = TRUE
end define;
  
procedure check_full_period(i)
begin
    (* Check cases
        1. now < start < stop
        2. now = start /\ start < stop
        3. start < now < stop
        4. start < now /\ now = stop
        5. start < stop < now
    *)
    proc:
        if now < userList[i].period[1] then
            userList[i] := NOTHING(userList[i]);
        elsif now = userList[i].period[1] then
            if ~IsSuperAdmin(userList[i]) then
                userList[i] := LOCK(userList[i]);
            end if;
        elsif userList[i].period[1] < now /\ now < userList[i].period[2] then
            if ~IsSuperAdmin(userList[i]) then
                assert UserIsLocked(userList[i]);
            end if;
        elsif now = userList[i].period[2] then
            userList[i] := UNLOCK(userList[i]);
        elsif userList[i].period[2] < now then
            if ~IsSuperAdmin(userList[i]) then
                assert UserIsUnlocked(userList[i]);
            end if;
        end if;
    r:
        return;
end procedure;
  
procedure check_start_period(i)
begin
    (* Check cases
        1. now < start
        2. now = start
        3. start < now
    *)
    proc:
        if now < userList[i].period[1] then
            userList[i] := NOTHING(userList[i]);
        elsif now = userList[i].period[1] then
            if ~IsSuperAdmin(userList[i]) then
                userList[i] := LOCK(userList[i]);
            end if;
        elsif userList[i].period[1] < now then
            if ~IsSuperAdmin(userList[i]) then
                assert UserIsLocked(userList[i]);
            end if;
        end if;
    r:
        return;
end procedure;
  
procedure check_stop_period(i)
begin
    (* Check cases
        1. now < stop
        2. now = stop
        3. stop < now
    *)
    proc:
        if now < userList[i].period[2] then
            if ~IsSuperAdmin(userList[i]) then
                userList[i] := LOCK(userList[i]);
            end if;
        elsif now = userList[i].period[2] then
            if ~IsSuperAdmin(userList[i]) then
                userList[i] := UNLOCK(userList[i]);
            end if;
        elsif userList[i].period[2] < now then
            if ~IsSuperAdmin(userList[i]) then
                assert UserIsUnlocked(userList[i]);
            end if;
        end if;
    r:
        return;
end procedure;
  
begin
    init:
        assert AllUsersUnlocked;
    movement:
        while now < MAX_TIME do
            check_users:
                while user_id <= Len(userList) do
                    check_period:
                        if userList[user_id].period[1] = 0 then
                            call check_stop_period(user_id);
                        elsif userList[user_id].period[2] = 0 then
                            call check_start_period(user_id);
                        elsif userList[user_id].period[1] # 0 /\ userList[user_id].period[2] # 0 then
                            call check_full_period(user_id);
                        end if;
                    inc:
                        user_id := user_id + 1;
                end while;
                user_id := 1;
            tick:
                now := now + 1;
        end while;
    final:
        assert ExistUsersUnlocked;
end algorithm; *)

Проверка модели

Теперь мы всё описали — в том смысле, что в процессе написания спеки я часто запускал проверку модели, чтобы понять, двигаюсь ли я в правильном направлении. Сейчас это своего рода финальный тест для всего алгоритма.

В секции CONSTANTS мы указали MAX_TIME = 150. Вспомним, что мы имитируем время через обычный счётчик, и в таком случае MAX_TIME означает, что мы имитируем 150 минут работы нашего алгоритма. А в секции INVARIANT мы указали наши инварианты проверки типов, невозможности заблокировать супердамина и проверки списка.

\* SPECIFICATION
\* Uncomment the previous line and provide the specification name if it's declared
\* in the specification file. Comment INIT / NEXT parameters if you use SPECIFICATION.
 
CONSTANTS
    MAX_TIME = 150
    defaultInitValue = 1
 
INIT Init
NEXT Next
 
\* PROPERTY
\* Uncomment the previous line and add property names
 
INVARIANT
    TypeInvariant
    AdminAlwaysUnlockedInvariant
    UserListInvariant
\* Uncomment the previous line and add invariant names

Результат!

Модель успешно выполнила нашу спецификацию. Теперь мы можем уверенно сказать, что придуманный алгоритм надёжный, как швейцарские часы. Но читатель тут же подумает: «Всё слишком идеально и как по маслу, а что если...". И действительно, если мы уберём (IsSuperAdmin) в процедурах проверки пользователя на суперадмина и тем самым приведём к его блокировке, а затем запустим модель? То инвариант будет нарушен, уведомит нас и покажет, где и когда это случилось.

Посмотрим на ошибку (читаем сверху вниз). Здесь мы видим, что на нашей 8-й минуте при проверке полного интервала мы заблокировали администратора

Убедитесь сами

Для того чтобы самостоятельно запустить данную спеку и убедиться в результате, вам необходимо:

1. Скачать расширение TLA+ в VsCode

2. Создать файл lockout.tla

3. Скопировать в него полное содержимое спеки (приведено выше)

4. Выполнить следующее

   1. Ctrl+Shift+P -> TLA+: Parse Module

   2. В созданный lockout.cfg добавить код выше (где задавали инварианты и константы)

   3. Ctrl+Shift+P -> TLA+: Check Module with TLC

Итог

Мы рассмотрели, как можно применить метод формальной верификации TLA+ для решения практической бизнес-задачи. И вместе с тем мы поломали голову (в хорошем смысле), подумав о задаче как об алгоритме в математических определениях.

Теперь я хочу поговорить с вами вот о чём. Почему формальная верификация, обладая такими преимуществами, не получает широкого распространения в повседневной разработке? Ведь полностью дочитав статью до этой строчки, вы наверняка подумали:

• математика — круто и надёжно

• сколько заняло времени написание спецификации?

• всё слишком гладко написано, явно есть какое-то «НО»

И вы будете правы, если ощущаете подвох. Он, с одной стороны, связан с экономическим вопросом. В решении бизнес-задачи должно быть заложено время на формальную верификацию, а время — это деньги. И бизнес, как правило, стремится к обратному, к уменьшению времени решения бизнес-задач. Не каждая компания готова вкладываться.

С другой стороны, вопрос связан с навыками и мышлением самих разработчиков. Обычно нас учат, что «Код — это результат тщательного анализа и проектирования алгоритма». А реальность показывает обратное, что «Код — это процес анализа и проектирования задачи». Т.е. как-будто алгоритмической части уделяется совсем мало времени и места. Тут я хочу подвести вас к мысли о том, что чаще разработчик думает в парадигме «задача -> код -> программа», а не «задача -> алгоритм -> код -> программа». И когда я начал заниматься темой формальной верификации, я с этим столкнулся.

И из-за этого вышло так, что данная спецификация была написана после того, как я написал саму программу. Посвятив время написанию спецификации по уже готовому коду, я изучил реализованный алгоритм лучше и увидел те свойства, о которых писал выше. И хочу сказать следующее — когда в голове происходит перестройка мышления при решении задачи (алгоритм и его свойства становятся важнее), это даёт большую уверенность в написанной программе. А также расширяет собственные горизонты.

Хочется сказать, что, может быть, метод ФВ не станет повседневным в вашей работе, как, например, статический анализ или тестирование. Но он отлично расширит ваши внутренние горизонты и позволит взглянуть на ваши программы шире, на уровне алгоритмов.

Ряд вопросов, которые не были озвучены в данной статье:

• как теперь переложить спецификацию в реальный код

• какие задачи лучше/хуже подходят для формальной верификации

• как сложно и как долго осваивается TLA+ в частности

• насколько нужно иметь хоршую математическую подготовку и что делать, если есть боязнь математики

• как формальная верификация могла бы быть встроена в ЖЦ ПО и как это отразилось бы на процессах

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

Источники

• Домашняя страница TLA+

• Применение в разных компаниях