232 lines
8.4 KiB
ReStructuredText
232 lines
8.4 KiB
ReStructuredText
|
====================
|
||
|
|
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 a 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 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 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 bellow::
|
||
|
|
|
||
|
|
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 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.
|
||
|
|
|
||
|
|
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**:
|
||
|
|
|
||
|
|
- 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**
|
||
|
|
|
||
|
|
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**
|
||
|
|
|
||
|
|
- Writing "0" prevents reactions for happening
|
||
|
|
- Writing "1" enable reactions
|
||
|
|
- Reading returns the current status of the reaction
|
||
|
|
|
||
|
|
**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
|
||
|
|
|
||
|
|
**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
|