런타임 검증

런타임 검증 개요

Runtime Verification(RV)은 model checking이나 theorem proving 같은 고전적인 전수 검증 기법을 보완하는 가볍지만 엄밀한 방법으로, 복잡한 시스템에 더 실용적으로 적용할 수 있다.

RV는 instruction 수준에서 시스템을 다시 구현한 세밀한 model에 의존하지 않는다. 실제 시스템 실행 trace를 분석하고 이를 시스템 동작의 formal specification과 비교한다.

주요 장점은 modeling language로 전체 시스템을 다시 구현할 때 생기는 문제 없이, 감시 대상의 runtime 동작에 관한 정확한 정보를 얻는다는 점이다.

효율적인 monitoring 방법이 있다면 system을 online으로 검증할 수 있다. 예상하지 못한 event에 즉시 reaction하여 safety-critical system에서 failure가 전파되는 일을 막을 수 있다.

====================
Runtime Verification
====================

Runtime Verification (RV) is a lightweight (yet rigorous) method that
complements classical exhaustive verification techniques (such as *model
checking* and *theorem proving*) with a more practical approach for complex
systems.

Instead of relying on a fine-grained model of a system (e.g., a
re-implementation at instruction level), RV works by analyzing the trace of the
system's actual execution, comparing it against a formal specification of
the system behavior.

The main advantage is that RV can give precise information on the runtime
behavior of the monitored system, without the pitfalls of developing models
that require a re-implementation of the entire system in a modeling language.
Moreover, given an efficient monitoring method, it is possible to execute an
*online* verification of a system, enabling the *reaction* for unexpected
events, avoiding, for example, the propagation of a failure on safety-critical
systems.

Runtime monitor와 reactor

monitor는 system runtime verification의 중심이다. 원하는 또는 원하지 않는 동작의 formal specification과 실제 system trace 사이에 위치한다.

Linux에서는 runtime verification monitor를 `RV monitor` 추상화 안에 캡슐화한다. RV monitor는 system reference model, per-CPU·per-task 등의 monitor instance 집합, trace를 통해 monitor와 system을 연결하는 helper function을 포함한다.

monitor는 system을 검증하고 감시하는 데 그치지 않고 unexpected event에 반응할 수 있다. reaction은 event 발생을 log하는 수준부터 올바른 동작을 강제하는 것, failure 전파를 막기 위해 system을 내리는 극단적인 동작까지 다양하다.

Linux에서 `reactor`는 RV monitor가 사용할 수 있는 reaction 방법이다. 모든 monitor는 기본적으로 자신의 동작을 trace output으로 제공해야 하며, 이것도 하나의 reaction이다. 사용자가 필요에 따라 활성화할 수 있는 추가 reaction도 제공된다.

runtime verification 원리와 Linux 적용에 관한 추가 자료로 Bartocci 외의 `Introduction to runtime verification`, Falcone 외의 RV tool taxonomy, Daniel Bristot de Oliveira의 2020년 박사 학위 논문을 제시한다.

Runtime Monitors and Reactors
=============================

A monitor is the central part of the runtime verification of a system. The
monitor stands in between the formal specification of the desired (or
undesired) behavior, and the trace of the actual system.

In Linux terms, the runtime verification monitors are encapsulated inside the
*RV monitor* abstraction. A *RV monitor* includes a reference model of the
system, a set of instances of the monitor (per-cpu monitor, per-task monitor,
and so on), and the helper functions that glue the monitor to the system via
trace, 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>

In addition to the verification and monitoring of the system, a monitor can
react to an unexpected event. The forms of reaction can vary from logging the
event occurrence to the enforcement of the correct behavior to the extreme
action of taking a system down to avoid the propagation of a failure.

In Linux terms, a *reactor* is an reaction method available for *RV monitors*.
By default, all monitors should provide a trace output of their actions,
which is already a reaction. In addition, other reactions will be available
so the user can enable them as needed.

For further information about the principles of runtime verification and
RV applied to Linux:

  Bartocci, Ezio, et al. *Introduction to runtime verification.* In: Lectures on
  Runtime Verification. Springer, Cham, 2018. p. 1-33.

  Falcone, Ylies, et al. *A taxonomy for classifying runtime verification tools.*
  In: International Conference on Runtime Verification. Springer, Cham, 2018. p.
  241-262.

  De Oliveira, Daniel Bristot. *Automata-based formal analysis and
  verification of the real-time Linux kernel.* Ph.D. Thesis, 2020.

Online RV monitor

monitor는 offline과 online으로 분류한다. offline monitor는 event가 발생한 뒤 system이 생성한 trace를 처리하며, 보통 영구 저장 장치에서 실행 trace를 읽는다. online monitor는 system 실행 중에 trace를 처리한다.

online monitor가 event processing을 system 실행에 붙여 monitoring 동안 system을 막으면 synchronous이다. 반대로 asynchronous monitor는 system 실행과 분리되어 동작한다.

각 유형에는 장점이 있다. offline monitor는 다른 machine에서 실행할 수 있지만 log를 file로 저장하는 작업이 필요하다. synchronous online 방식은 violation이 발생한 바로 그 순간 반응할 수 있다.

event 분석 overhead도 중요하다. system의 event 생성 빈도가 같은 system에서 monitor가 처리할 수 있는 속도보다 빠르면 offline 방법만 가능하다.

반대로 event 하나를 monitor가 직접 처리하는 비용보다 event tracing 자체의 비용이 더 크다면 synchronous online monitor의 overhead가 더 낮다.

De Oliveira, Cucinotta, De Oliveira의 2019년 연구는 `Deterministic Automata`에 기반한 deterministic automaton model에서 kernel 안의 synchronous event processing이 같은 event를 trace buffer에 저장하는 것보다 overhead가 낮음을 보였다. userspace 분석을 위한 trace 수집 비용은 이 비교에 포함하지도 않았다.

이 결과가 in-kernel online monitor interface 개발의 동기가 되었다. automaton으로 Linux kernel 동작을 modeling하는 추가 자료로 PREEMPT_RT Linux kernel의 thread synchronization model 논문을 제시한다.

Online RV monitors
==================

Monitors can be classified as *offline* and *online* monitors. *Offline*
monitor process the traces generated by a system after the events, generally by
reading the trace execution from a permanent storage system. *Online* monitors
process the trace during the execution of the system. Online monitors are said
to be *synchronous* if the processing of an event is attached to the system
execution, blocking the system during the event monitoring. On the other hand,
an *asynchronous* monitor has its execution detached from the system. Each type
of monitor has a set of advantages. For example, *offline* monitors can be
executed on different machines but require operations to save the log to a
file. In contrast, *synchronous online* method can react at the exact moment
a violation occurs.

Another important aspect regarding monitors is the overhead associated with the
event analysis. If the system generates events at a frequency higher than the
monitor's ability to process them in the same system, only the *offline*
methods are viable. On the other hand, if the tracing of the events incurs
on higher overhead than the simple handling of an event by a monitor, then a
*synchronous online* monitors will incur on lower overhead.

Indeed, the research presented in:

  De Oliveira, Daniel Bristot; Cucinotta, Tommaso; De Oliveira, Romulo Silva.
  *Efficient formal verification for the Linux kernel.* In: International
  Conference on Software Engineering and Formal Methods. Springer, Cham, 2019.
  p. 315-332.

Shows that for Deterministic Automata models, the synchronous processing of
events in-kernel causes lower overhead than saving the same events to the trace
buffer, not even considering collecting the trace for user-space analysis.
This motivated the development of an in-kernel interface for online monitors.

For further information about modeling of Linux kernel behavior using automata,
see:

  De Oliveira, Daniel B.; De Oliveira, Romulo S.; Cucinotta, Tommaso. *A thread
  synchronization model for the PREEMPT_RT Linux kernel.* Journal of Systems
  Architecture, 2020, 107: 101729.

사용자 인터페이스와 사용 가능 항목

사용자 인터페이스는 의도적으로 tracing interface와 닮았으며 현재 `/sys/kernel/tracing/rv/`에 있다.

`available_monitors`를 읽으면 사용 가능한 monitor가 한 줄에 하나씩 표시된다.

# cat available_monitors
wip
wwnr

`available_reactors`를 읽으면 사용 가능한 reactor가 한 줄에 하나씩 표시된다.

# cat available_reactors
nop
panic
printk

The user interface
==================

The user interface resembles the tracing interface (on purpose). It is
currently at "/sys/kernel/tracing/rv/".

The following files/folders are currently available:

**available_monitors**

- Reading list the available monitors, one per line

For example::

   # cat available_monitors
   wip
   wwnr

**available_reactors**

- Reading shows the available reactors, one per line.

For example::

   # cat available_reactors
   nop
   panic
   printk

enabled_monitors

`enabled_monitors`를 읽으면 활성화된 monitor가 한 줄에 하나씩 나온다. monitor 이름을 쓰면 활성화하고, `!` prefix를 붙인 이름을 쓰면 비활성화한다. file을 truncate하면 활성화된 모든 monitor를 비활성화한다.

# cat enabled_monitors
# echo wip > enabled_monitors
# echo wwnr >> enabled_monitors
# cat enabled_monitors
wip
wwnr
# echo '!wip' >> enabled_monitors
# cat enabled_monitors
wwnr
# echo > enabled_monitors
# cat enabled_monitors
#

둘 이상의 monitor를 동시에 활성화할 수 있다.

**enabled_monitors**:

- Reading lists the enabled monitors, one per line
- Writing to it enables a given monitor
- Writing a monitor name with a '!' prefix disables it
- Truncating the file disables all enabled monitors

For example::

   # cat enabled_monitors
   # echo wip > enabled_monitors
   # echo wwnr >> enabled_monitors
   # cat enabled_monitors
   wip
   wwnr
   # echo '!wip' >> enabled_monitors
   # cat enabled_monitors
   wwnr
   # echo > enabled_monitors
   # cat enabled_monitors
   #

Note that it is possible to enable more than one monitor concurrently.

monitoring_on

`monitoring_on`은 monitoring 전체의 on/off switch이며 trace interface의 `tracing_on` switch와 비슷하다.

이 switch는 enabled monitor를 disable하지 않는다. system에서 받은 event를 per-entity monitor가 처리하는 동작만 멈춘다.

**monitoring_on**

This is an on/off general switcher for monitoring. It resembles the
"tracing_on" switcher in the trace interface.

- Writing "0" stops the monitoring
- Writing "1" continues the monitoring
- Reading returns the current status of the monitoring

Note that it does not disable enabled monitors but stop the per-entity
monitors monitoring the events received from the system.

reacting_on

`reacting_on`은 reaction 실행을 전체적으로 제어한다. `0`을 쓰면 reaction을 막고 `1`을 쓰면 허용하며, 읽으면 현재 reaction 상태를 반환한다.

**reacting_on**

- Writing "0" prevents reactions for happening
- Writing "1" enable reactions
- Reading returns the current status of the reaction

monitors 디렉터리

각 monitor는 `monitors/` 안에 자신의 디렉터리를 가지며 monitor별 file이 그 안에 나타난다. `monitors/`는 tracefs의 `events` 디렉터리와 비슷하다.

# cd monitors/wip/
# ls
desc  enable
# cat desc
wakeup in preemptive per-cpu testing monitor.
# cat enable
0

**monitors/**

Each monitor will have its own directory inside "monitors/". There the
monitor-specific files will be presented. The "monitors/" directory resembles
the "events" directory on tracefs.

For example::

   # cd monitors/wip/
   # ls
   desc  enable
   # cat desc
   wakeup in preemptive per-cpu testing monitor.
   # cat enable
   0

monitor별 파일과 reactor 선택

`monitors/MONITOR/desc`를 읽으면 해당 `MONITOR`의 설명을 보여 준다.

`monitors/MONITOR/enable`에 `0`을 쓰면 monitor를 비활성화하고 `1`을 쓰면 활성화한다. 읽으면 현재 monitor 상태를 반환한다.

`monitors/MONITOR/reactors`는 사용 가능한 reactor를 나열하고, 해당 monitor에 선택된 reaction은 `[]` 안에 표시한다. 기본값은 아무 동작도 하지 않는 `nop` reactor이다. reactor 이름을 쓰면 그 monitor에 해당 reactor를 활성화한다.

# cat monitors/wip/reactors
[nop]
panic
printk
# echo panic > monitors/wip/reactors
# cat monitors/wip/reactors
nop
[panic]
printk

**monitors/MONITOR/desc**

- Reading shows a description of the monitor *MONITOR*

**monitors/MONITOR/enable**

- Writing "0" disables the *MONITOR*
- Writing "1" enables the *MONITOR*
- Reading return the current status of the *MONITOR*

**monitors/MONITOR/reactors**

- List available reactors, with the select reaction for the given *MONITOR*
  inside "[]". The default one is the nop (no operation) reactor.
- Writing the name of a reactor enables it to the given MONITOR.

For example::

   # cat monitors/wip/reactors
   [nop]
   panic
   printk
   # echo panic > monitors/wip/reactors
   # cat monitors/wip/reactors
   nop
   [panic]
   printk