선형 시간 논리

소개

런타임 검증 모니터는 커널이 명세를 따르는지 확인하는 검증 기법이다. tracepoint로 커널의 실행 trace를 감시하고, 그 실행 trace가 명세를 만족하는지 검사한다.

처음에는 명세를 결정적 오토마톤(DA) 형식으로만 작성할 수 있었다. 그러나 복잡한 명세의 DA monitor를 구현하는 과정에서 결정적 오토마톤은 명세 언어로 부적합한 경우가 드러났다. 오토마톤이 복잡하고 이해하기 어려우며 오류가 생기기 쉽기 때문이다.

이에 선형 시간 논리(LTL)에 기반한 RV monitor가 도입되었다. 이 유형은 DA 대신 LTL을 명세로 사용하며, 일부 경우에는 LTL 명세가 더 간결하고 직관적이다.

LTL을 자세히 설명하는 자료는 많다. 여기서는 Christel Baier와 Joost-Pieter Katoen의 `Principles of Model Checking`, The MIT Press, 2008을 참고 문헌으로 제시한다.

Linear temporal logic
=====================

Introduction
------------

Runtime verification monitor is a verification technique which checks that the
kernel follows a specification. It does so by using tracepoints to monitor the
kernel's execution trace, and verifying that the execution trace sastifies the
specification.

Initially, the specification can only be written in the form of deterministic
automaton (DA).  However, while attempting to implement DA monitors for some
complex specifications, deterministic automaton is found to be inappropriate as
the specification language. The automaton is complicated, hard to understand,
and error-prone.

Thus, RV monitors based on linear temporal logic (LTL) are introduced. This type
of monitor uses LTL as specification instead of DA. For some cases, writing the
specification as LTL is more concise and intuitive.

Many materials explain LTL in details. One book is::

  Christel Baier and Joost-Pieter Katoen: Principles of Model Checking, The MIT
  Press, 2008.

문법

커널의 LTL 구현 문법은 일부 기존 표기보다 장황하다. LTL에 익숙하지 않은 사람도 명세를 읽을 수 있도록 의도적으로 명시적인 단어를 사용한다.

ltl ::= opd | ( ltl ) | ltl binop ltl | unop ltl

이 문법에는 연산자 우선순위가 정의되어 있지 않아 모호하다. 따라서 의도한 결합 순서를 반드시 괄호로 표시해야 한다.

Grammar
-------

Unlike some existing syntax, kernel's implementation of LTL is more verbose.
This is motivated by considering that the people who read the LTL specifications
may not be well-versed in LTL.

Grammar:
    ltl ::= opd | ( ltl ) | ltl binop ltl | unop ltl

Operands (opd):
    true, false, user-defined names consisting of upper-case characters, digits,
    and underscore.

Unary Operators (unop):
    always
    eventually
    next
    not

Binary Operators (binop):
    until
    and
    or
    imply
    equivalent

This grammar is ambiguous: operator precedence is not defined. Parentheses must
be used.

선형 시간 논리 예

RAIN imply (GO_OUTSIDE imply HAVE_UMBRELLA)

비가 온다면, 밖에 나간다는 것은 우산을 가지고 있음을 뜻한다.

RAIN imply (WET until not RAIN)

비가 온다면, 비가 멎을 때까지 젖은 상태가 이어진다는 뜻이다.

RAIN imply eventually not RAIN

비가 온다면 언젠가는 비가 멎는다는 뜻이다.

위 세 예는 현재 시점만 가리킨다. 커널 검증에서는 어떤 성질이 현재와 모든 미래에 항상 참임을 지정하는 `always` 연산자가 대체로 필요하다.

always (RAIN imply eventually not RAIN)

이 식은 모든 비가 결국 멎는다는 뜻이다. 예에서 `RAIN`, `GO_OUTSIDE`, `HAVE_UMBRELLA`, `WET`은 원자 명제(atomic proposition)이다.

Example linear temporal logic
-----------------------------
.. code-block::

   RAIN imply (GO_OUTSIDE imply HAVE_UMBRELLA)

means: if it is raining, going outside means having an umbrella.

.. code-block::

   RAIN imply (WET until not RAIN)

means: if it is raining, it is going to be wet until the rain stops.

.. code-block::

   RAIN imply eventually not RAIN

means: if it is raining, rain will eventually stop.

The above examples are referring to the current time instance only. For kernel
verification, the `always` operator is usually desirable, to specify that
something is always true at the present and for all future. For example::

    always (RAIN imply eventually not RAIN)

means: *all* rain eventually stops.

In the above examples, `RAIN`, `GO_OUTSIDE`, `HAVE_UMBRELLA` and `WET` are the
"atomic propositions".

모니터 합성

LTL을 커널 monitor로 합성하려면 `tools/verification/rvgen`의 `rvgen` 도구를 사용한다. 명세를 파일로 제공하고 `RULE = LTL` 대입문을 포함해야 한다.

RULE = always (ACQUIRE imply ((not KILLED and not CRASHED) until RELEASE))

이 규칙은 `ACQUIRE`가 발생했다면 `KILLED` 또는 `CRASHED`보다 먼저 `RELEASE`가 발생해야 한다는 뜻이다.

LTL은 하위 표현식으로 나눌 수 있다. 다음 두 줄은 위 규칙과 동등하다.

RULE = always (ACQUIRE imply (ALIVE until RELEASE))
ALIVE = not KILLED and not CRASHED

이 명세에서 `rvgen`은 LTL의 만족 가능성을 검사하는 비결정적 상태 기계인 Buchi automaton의 C 구현을 생성한다. 사용법은 `Documentation/trace/rv/monitor_synthesis.rst`를 참고한다.

Monitor synthesis
-----------------

To synthesize an LTL into a kernel monitor, the `rvgen` tool can be used:
`tools/verification/rvgen`. The specification needs to be provided as a file,
and it must have a "RULE = LTL" assignment. For example::

    RULE = always (ACQUIRE imply ((not KILLED and not CRASHED) until RELEASE))

which says: if `ACQUIRE`, then `RELEASE` must happen before `KILLED` or
`CRASHED`.

The LTL can be broken down using sub-expressions. The above is equivalent to:

   .. code-block::

    RULE = always (ACQUIRE imply (ALIVE until RELEASE))
    ALIVE = not KILLED and not CRASHED

From this specification, `rvgen` generates the C implementation of a Buchi
automaton - a non-deterministic state machine which checks the satisfiability of
the LTL. See Documentation/trace/rv/monitor_synthesis.rst for details on using
`rvgen`.

참고 문헌

모델 검사와 선형 시간 논리의 개론서로 Baier와 Katoen의 `Principles of Model Checking`을 제시한다.

소프트웨어 시험에 LTL을 적용한 사례로 Meng 외 저자의 2022년 ICSE 논문 `Linear-time temporal logic guided greybox fuzzing`과 DOI `10.1145/3510003.3510082`를 제시한다.

커널 LTL monitor 구현은 Gerth, Peled, Vardi, Wolper의 1996년 논문 `Simple On-the-fly Automatic Verification of Linear Temporal Logic`에 기반하며 DOI는 `10.1007/978-0-387-34892-6_1`이다.

References
----------

One book covering model checking and linear temporal logic is::

  Christel Baier and Joost-Pieter Katoen: Principles of Model Checking, The MIT
  Press, 2008.

For an example of using linear temporal logic in software testing, see::

  Ruijie Meng, Zhen Dong, Jialin Li, Ivan Beschastnikh, and Abhik Roychoudhury.
  2022. Linear-time temporal logic guided greybox fuzzing. In Proceedings of the
  44th International Conference on Software Engineering (ICSE '22).  Association
  for Computing Machinery, New York, NY, USA, 1343–1355.
  https://doi.org/10.1145/3510003.3510082

The kernel's LTL monitor implementation is based on::

  Gerth, R., Peled, D., Vardi, M.Y., Wolper, P. (1996). Simple On-the-fly
  Automatic Verification of Linear Temporal Logic. In: Dembiński, P., Średniawa,
  M. (eds) Protocol Specification, Testing and Verification XV. PSTV 1995. IFIP
  Advances in Information and Communication Technology. Springer, Boston, MA.
  https://doi.org/10.1007/978-0-387-34892-6_1