런타임 검증 모니터 합성

RV monitor 구조

런타임 검증(RV) 기법 적용의 출발점은 검사 대상 시스템에서 원하는 동작 또는 원하지 않는 동작을 명세하거나 모델링하는 것이다.

형식 표현은 시스템 trace 분석에 사용할 monitor로 합성해야 한다. monitor는 system event를 specification event로 변환하는 instrumentation을 통해 시스템에 연결된다.

Linux에서 runtime verification monitor는 `RV monitor` 추상화 안에 캡슐화된다. 이 추상화에는 per-CPU, per-task 등의 monitor instance 집합, monitor를 system reference model에 연결하는 helper function, event parsing과 exception에 반응하는 trace output이 포함된다.

Runtime Verification Monitor Synthesis
======================================

The starting point for the application of runtime verification (RV) techniques
is the *specification* or *modeling* of the desired (or undesired) behavior
of the system under scrutiny.

The formal representation needs to be then *synthesized* into a *monitor*
that can then be used in the analysis of the trace of the system. The
*monitor* connects to the system via an *instrumentation* that converts
the events from the *system* to the events of the *specification*.


In Linux terms, the runtime verification monitors are encapsulated inside
the *RV monitor* abstraction. The RV monitor includes a set of instances
of the monitor (per-cpu monitor, per-task monitor, and so on), the helper
functions that glue the monitor to the system reference model, and the
trace output as a reaction to event parsing and exceptions, as depicted
below::

 Linux  +----- RV Monitor ----------------------------------+ Formal
  Realm |                                                   |  Realm
  +-------------------+     +----------------+     +-----------------+
  |   Linux kernel    |     |     Monitor    |     |     Reference   |
  |     Tracing       |  -> |   Instance(s)  | <-  |       Model     |
  | (instrumentation) |     | (verification) |     | (specification) |
  +-------------------+     +----------------+     +-----------------+
         |                          |                       |
         |                          V                       |
         |                     +----------+                 |
         |                     | Reaction |                 |
         |                     +--+--+--+-+                 |
         |                        |  |  |                   |
         |                        |  |  +-> trace output ?  |
         +------------------------|--|----------------------+
                                  |  +----> panic ?
                                  +-------> <user-specified>

RV monitor 합성

명세를 Linux `RV monitor` 추상화로 합성하는 과정은 `rvgen` 도구와 monitor 생성 공통 코드를 담은 header file로 자동화된다.

RV monitor synthesis
--------------------

The synthesis of a specification into the Linux *RV monitor* abstraction is
automated by the rvgen tool and the header file containing common code for
creating monitors. The header files are:

  * rv/da_monitor.h for deterministic automaton monitor.
  * rv/ltl_monitor.h for linear temporal logic monitor.

rvgen

`rvgen` utility는 specification을 C 표현으로 변환하고 C로 작성된 kernel monitor skeleton을 생성한다.

[1]의 `wip.dot` model을 per-CPU monitor로 변환하는 명령은 다음과 같다.

$ rvgen monitor -c da -s wip.dot -t per_cpu

명령은 `wip/` 디렉터리를 만들고 C로 표현한 wip model인 `wip.h`와 RV monitor인 `wip.c`를 생성한다. `wip.c`에는 monitor declaration과 system instrumentation을 작성할 출발점이 들어 있다.

linear temporal logic monitor도 같은 방식으로 생성할 수 있다.

$ rvgen monitor -c ltl -s pagefault.ltl -t per_task

이 명령은 `pagefault/` 디렉터리에 명세 검증용 비결정적 상태 기계인 Buchi automaton을 담은 `pagefault.h`와 RV monitor skeleton인 `pagefault.c`를 생성한다.

rvgen
-----

The rvgen utility converts a specification into the C presentation and creating
the skeleton of a kernel monitor in C.

For example, it is possible to transform the wip.dot model present in
[1] into a per-cpu monitor with the following command::

  $ rvgen monitor -c da -s wip.dot -t per_cpu

This will create a directory named wip/ with the following files:

- wip.h: the wip model in C
- wip.c: the RV monitor

The wip.c file contains the monitor declaration and the starting point for
the system instrumentation.

Similarly, a linear temporal logic monitor can be generated with the following
command::

  $ rvgen monitor -c ltl -s pagefault.ltl -t per_task

This generates pagefault/ directory with:

- pagefault.h: The Buchi automaton (the non-deterministic state machine to
  verify the specification)
- pagefault.c: The skeleton for the RV monitor

Monitor header file

`rv/da_monitor.h`와 `rv/ltl_monitor`는 monitor instance 구현을 위한 공통 macro와 static function을 포함한다.

공통 기능을 하나의 header file에 모으면 코드 중복을 줄이고, bug fix와 개선을 쉽게 하며, 개발자가 model을 비표준 방식으로 조작하려고 monitor core code를 변경하는 일을 피할 수 있다.

Monitor header files
--------------------

The header files:

- `rv/da_monitor.h` for deterministic automaton monitor
- `rv/ltl_monitor` for linear temporal logic monitor

include common macros and static functions for implementing *Monitor
Instance(s)*.

The benefits of having all common functionalities in a single header file are
3-fold:

  - Reduce the code duplication;
  - Facilitate the bug fix/improvement;
  - Avoid the case of developers changing the core of the monitor code to
    manipulate the model in a (let's say) non-standard way.

rv/da_monitor.h

초기 구현은 global, per-CPU, per-task의 세 가지 deterministic automaton monitor instance 유형을 제공한다.

#define DECLARE_DA_MON_GLOBAL(name, type)
#define DECLARE_DA_MON_PER_CPU(name, type)
#define DECLARE_DA_MON_PER_TASK(name, type)

첫 macro는 global deterministic automaton monitor용 함수를, 두 번째는 per-CPU instance용 함수를, 세 번째는 per-task instance용 함수를 선언한다.

모든 경우 `name` argument는 monitor 식별 문자열이고 `type` argument는 `rvgen`이 model의 C 표현에 사용한 data type이다.

state 2개와 event 3개인 wip model은 `unsigned char`에 저장할 수 있다. preemption control은 per-CPU 동작이므로 `wip.c`의 선언은 다음과 같다.

DECLARE_DA_MON_PER_CPU(wip, unsigned char);

monitor는 아래 함수에 event enum 값을 보내 실행한다.

da_handle_event_$(MONITOR_NAME)($(event from event enum));
da_handle_start_event_$(MONITOR_NAME)($(event from event enum));
da_handle_start_run_event_$(MONITOR_NAME)($(event from event enum));

`da_handle_event_$(MONITOR_NAME)()`은 monitor가 event를 처리 중일 때 전달받은 event를 처리하는 일반 경로이다.

monitor를 enable하면 automaton의 initial state에 놓이지만 실제 system도 initial state인지는 알 수 없다.

`da_handle_start_event_$(MONITOR_NAME)()`은 system이 initial state로 돌아가고 있음을 알려, monitor가 다음 event부터 감시를 시작하게 한다.

`da_handle_start_run_event_$(MONITOR_NAME)()`은 system이 initial state임이 알려진 경우 현재 event까지 처리하면서 감시를 시작하게 한다.

wip model에서 `preempt_disable`과 `sched_waking`은 다음 일반 handler로 보낸다.

da_handle_event_wip(preempt_disable_wip);
da_handle_event_wip(sched_waking_wip);

`preempt_enabled` event는 system이 initial state로 돌아감을 알려 system과 monitor를 동기화해야 하므로 다음 start handler를 사용한다.

da_handle_start_event_wip(preempt_enable_wip);

rv/da_monitor.h
+++++++++++++++

This initial implementation presents three different types of monitor instances:

- ``#define DECLARE_DA_MON_GLOBAL(name, type)``
- ``#define DECLARE_DA_MON_PER_CPU(name, type)``
- ``#define DECLARE_DA_MON_PER_TASK(name, type)``

The first declares the functions for a global deterministic automata monitor,
the second for monitors with per-cpu instances, and the third with per-task
instances.

In all cases, the 'name' argument is a string that identifies the monitor, and
the 'type' argument is the data type used by rvgen on the representation of
the model in C.

For example, the wip model with two states and three events can be
stored in an 'unsigned char' type. Considering that the preemption control
is a per-cpu behavior, the monitor declaration in the 'wip.c' file is::

  DECLARE_DA_MON_PER_CPU(wip, unsigned char);

The monitor is executed by sending events to be processed via the functions
presented below::

  da_handle_event_$(MONITOR_NAME)($(event from event enum));
  da_handle_start_event_$(MONITOR_NAME)($(event from event enum));
  da_handle_start_run_event_$(MONITOR_NAME)($(event from event enum));

The function ``da_handle_event_$(MONITOR_NAME)()`` is the regular case where
the event will be processed if the monitor is processing events.

When a monitor is enabled, it is placed in the initial state of the automata.
However, the monitor does not know if the system is in the *initial state*.

The ``da_handle_start_event_$(MONITOR_NAME)()`` function is used to notify the
monitor that the system is returning to the initial state, so the monitor can
start monitoring the next event.

The ``da_handle_start_run_event_$(MONITOR_NAME)()`` function is used to notify
the monitor that the system is known to be in the initial state, so the
monitor can start monitoring and monitor the current event.

Using the wip model as example, the events "preempt_disable" and
"sched_waking" should be sent to monitor, respectively, via [2]::

  da_handle_event_wip(preempt_disable_wip);
  da_handle_event_wip(sched_waking_wip);

While the event "preempt_enabled" will use::

  da_handle_start_event_wip(preempt_enable_wip);

To notify the monitor that the system will be returning to the initial state,
so the system and the monitor should be in sync.

rv/ltl_monitor.h와 atom 갱신

`rv/ltl_monitor.h`는 `rvgen`이 생성한 `$(MODEL_NAME).h`와 결합해야 완전한 monitor가 된다. 예를 들어 `pagefault.c`는 다음 두 header를 include해야 하며, `rvgen`이 생성한 skeleton에는 이미 포함되어 있다.

#include "pagefault.h"
#include <rv/ltl_monitor.h>

`pagefault.h` 같은 `$(MODEL_NAME).h`는 LTL specification을 검증하는 비결정적 상태 기계인 Buchi automaton 구현을 담는다. `rv/ltl_monitor.h`는 Buchi automaton과 상호 작용하고 RV monitor를 구현하는 공통 helper function을 담는다.

`$(MODEL_NAME).h`의 중요한 정의는 LTL specification에 존재하는 atomic proposition 목록이다. 이름 충돌을 피하도록 `LTL_` prefix를 붙이고 마지막에 `LTL_NUM_ATOM`을 둔다.

enum ltl_atom {
    LTL_$(FIRST_ATOMIC_PROPOSITION),
    LTL_$(SECOND_ATOMIC_PROPOSITION),
    ...
    LTL_NUM_ATOM
};

이 `enum`은 Buchi automaton과 상호 작용하는 함수에 전달된다.

`rvgen`은 code generation 중 atomic proposition의 실제 의미를 이해할 수 없으므로 개발자가 수동으로 연결해야 한다. 권장 방식은 atomic proposition이 바뀌는 위치에 tracepoint를 추가하고 handler에서 다음 함수로 Buchi automaton을 실행하는 것이다.

void ltl_atom_update(struct task_struct *task, enum ltl_atom atom, bool value)

이 함수는 atomic proposition `atom`의 현재 값이 `value`임을 Buchi automaton에 알린다. automaton은 LTL specification이 여전히 만족되는지 검사하고, 위반을 발견하면 monitor error tracepoint와 reactor를 호출한다.

rv/ltl_monitor.h
++++++++++++++++
This file must be combined with the $(MODEL_NAME).h file (generated by `rvgen`)
to be complete. For example, for the `pagefault` monitor, the `pagefault.c`
source file must include::

  #include "pagefault.h"
  #include <rv/ltl_monitor.h>

(the skeleton monitor file generated by `rvgen` already does this).

`$(MODEL_NAME).h` (`pagefault.h` in the above example) includes the
implementation of the Buchi automaton - a non-deterministic state machine that
verifies the LTL specification. While `rv/ltl_monitor.h` includes the common
helper functions to interact with the Buchi automaton and to implement an RV
monitor. An important definition in `$(MODEL_NAME).h` is::

  enum ltl_atom {
      LTL_$(FIRST_ATOMIC_PROPOSITION),
      LTL_$(SECOND_ATOMIC_PROPOSITION),
      ...
      LTL_NUM_ATOM
  };

which is the list of atomic propositions present in the LTL specification
(prefixed with "LTL\_" to avoid name collision). This `enum` is passed to the
functions interacting with the Buchi automaton.

While generating code, `rvgen` cannot understand the meaning of the atomic
propositions. Thus, that task is left for manual work. The recommended practice
is adding tracepoints to places where the atomic propositions change; and in the
tracepoints' handlers: the Buchi automaton is executed using::

  void ltl_atom_update(struct task_struct *task, enum ltl_atom atom, bool value)

which tells the Buchi automaton that the atomic proposition `atom` is now
`value`. The Buchi automaton checks whether the LTL specification is still
satisfied, and invokes the monitor's error tracepoint and the reactor if
violation is detected.

ltl_atom_fetch()

가능하면 tracepoint와 `ltl_atom_update()`를 사용해야 하지만 항상 가장 편리한 것은 아니다. kernel의 여러 위치에서 바뀌는 atomic proposition은 모든 위치를 trace하기 번거롭고, 정확한 갱신 시점이 중요하지 않을 수도 있다.

RULE = always (RT imply not PAGEFAULT)

이 LTL은 real-time task가 page fault를 발생시키지 않는다는 뜻이다. `PAGEFAULT`가 true일 때 `RT` 값만 올바르면 되므로 `RT`가 정확히 언제 바뀌는지는 중요하지 않다.

이 사례를 위해 Buchi automaton이 trigger될 때마다 호출되는 fetch 함수가 도입되었다.

void ltl_atom_fetch(struct task_struct *task, struct ltl_monitor *mon)

`RT` 값을 가져오는 구현은 다음과 같다.

void ltl_atom_fetch(struct task_struct *task, struct ltl_monitor *mon)
{
    ltl_atom_set(mon, LTL_RT, rt_task(task));
}

결과적으로 `ltl_atom_update()`로 `PAGEFAULT`를 갱신할 때 `RT`도 함께 fetch된다. 따라서 `RT`가 바뀌는 모든 위치를 trace하지 않고도 LTL specification을 검증할 수 있다.

Tracepoints and `ltl_atom_update()` should be used whenever possible. However,
it is sometimes not the most convenient. For some atomic propositions which are
changed in multiple places in the kernel, it is cumbersome to trace all those
places. Furthermore, it may not be important that the atomic propositions are
updated at precise times. For example, considering the following linear temporal
logic::

  RULE = always (RT imply not PAGEFAULT)

This LTL states that a real-time task does not raise page faults. For this
specification, it is not important when `RT` changes, as long as it has the
correct value when `PAGEFAULT` is true.  Motivated by this case, another
function is introduced::

  void ltl_atom_fetch(struct task_struct *task, struct ltl_monitor *mon)

This function is called whenever the Buchi automaton is triggered. Therefore, it
can be manually implemented to "fetch" `RT`::

  void ltl_atom_fetch(struct task_struct *task, struct ltl_monitor *mon)
  {
      ltl_atom_set(mon, LTL_RT, rt_task(task));
  }

Effectively, whenever `PAGEFAULT` is updated with a call to `ltl_atom_update()`,
`RT` is also fetched. Thus, the LTL specification can be verified without
tracing `RT` everywhere.

ltl_atom_pulse()

event처럼 작동하는 atomic proposition은 보통 값을 설정한 직후 다시 지우거나, 지운 직후 다시 설정해야 한다. 이를 간편하게 하는 함수는 다음과 같다.

void ltl_atom_pulse(struct task_struct *task, enum ltl_atom atom, bool value)

이 함수는 아래 두 번의 update와 동등하다.

ltl_atom_update(task, atom, value);
ltl_atom_update(task, atom, !value);

For atomic propositions which act like events, they usually need to be set (or
cleared) and then immediately cleared (or set). A convenient function is
provided::

  void ltl_atom_pulse(struct task_struct *task, enum ltl_atom atom, bool value)

which is equivalent to::

  ltl_atom_update(task, atom, value);
  ltl_atom_update(task, atom, !value);

atomic proposition 초기화

atomic proposition을 초기화하려면 다음 함수를 구현해야 한다.

ltl_atoms_init(struct task_struct *task, struct ltl_monitor *mon, bool task_creation)

monitor를 enable할 때 실행 중인 모든 task에 대해 호출되며, enable 뒤 새로 생성되는 task에도 호출된다. 가능한 많은 atomic proposition을 초기화해야 한다.

void ltl_atom_init(struct task_struct *task, struct ltl_monitor *mon, bool task_creation)
{
    ltl_atom_set(mon, LTL_RT, rt_task(task));
    if (task_creation)
        ltl_atom_set(mon, LTL_PAGEFAULT, false);
}

`ltl_atom_init()`에서 초기화하지 않은 atomic proposition은 관련 tracepoint가 발생할 때까지 unknown state로 남으며 시간이 걸릴 수 있다.

task의 모든 atomic proposition을 알기 전에는 그 task를 monitor할 수 없다. 따라서 monitor enable 전에 이미 실행 중이던 task의 검증 시작이 늦어질 수 있으므로, 관심 task는 monitor를 enable한 뒤 시작하는 것을 권장한다.

To initialize the atomic propositions, the following function must be
implemented::

  ltl_atoms_init(struct task_struct *task, struct ltl_monitor *mon, bool task_creation)

This function is called for all running tasks when the monitor is enabled. It is
also called for new tasks created after the enabling the monitor. It should
initialize as many atomic propositions as possible, for example::

  void ltl_atom_init(struct task_struct *task, struct ltl_monitor *mon, bool task_creation)
  {
      ltl_atom_set(mon, LTL_RT, rt_task(task));
      if (task_creation)
          ltl_atom_set(mon, LTL_PAGEFAULT, false);
  }

Atomic propositions not initialized by `ltl_atom_init()` will stay in the
unknown state until relevant tracepoints are hit, which can take some time. As
monitoring for a task cannot be done until all atomic propositions is known for
the task, the monitor may need some time to start validating tasks which have
been running before the monitor is enabled. Therefore, it is recommended to
start the tasks of interest after enabling the monitor.

마무리와 참고 사항

header file과 `rvgen`을 이용한 monitor synthesis가 마련되면 개발자의 작업은 system instrumentation으로 제한된다. 이는 전체 접근 방식의 신뢰도를 높인다.

deterministic automaton 형식과 표현 사이의 변환은 `Documentation/trace/rv/deterministic_automata.rst`를 참고한다.

`rvgen`은 BPF program이 사용하는 global `vmlinux.h`를 export할 때 변수 충돌을 피하도록 event enum에 monitor 이름 suffix를 붙인다.

Final remarks
-------------

With the monitor synthesis in place using the header files and
rvgen, the developer's work should be limited to the instrumentation
of the system, increasing the confidence in the overall approach.

[1] For details about deterministic automata format and the translation
from one representation to another, see::

  Documentation/trace/rv/deterministic_automata.rst

[2] rvgen appends the monitor's name suffix to the events enums to
avoid conflicting variables when exporting the global vmlinux.h
use by BPF programs.