| lists.openwall.net | lists / announce owl-users owl-dev john-users john-dev passwdqc-users yescrypt popa3d-users / oss-security kernel-hardening musl sabotage tlsify passwords / crypt-dev xvendor / Bugtraq Full-Disclosure linux-kernel linux-netdev linux-ext4 linux-hardening linux-cve-announce PHC | |
|
Open Source and information security mailing list archives
| ||
|
Message-Id: <cover.1621414942.git.bristot@redhat.com>
Date: Wed, 19 May 2021 13:36:21 +0200
From: Daniel Bristot de Oliveira <bristot@...hat.com>
To: linux-kernel@...r.kernel.org, Steven Rostedt <rostedt@...dmis.org>
Cc: Tommaso Cucinotta <tommaso.cucinotta@...tannapisa.it>,
Kate Carcia <kcarcia@...hat.com>,
Daniel Bristot de Oliveira <bristot@...hat.com>,
Jonathan Corbet <corbet@....net>,
Ingo Molnar <mingo@...hat.com>,
Mauro Carvalho Chehab <mchehab@...nel.org>,
Thomas Gleixner <tglx@...utronix.de>,
Peter Zijlstra <peterz@...radead.org>,
Will Deacon <will@...nel.org>,
Catalin Marinas <catalin.marinas@....com>,
"Paul E. McKenney" <paulmck@...nel.org>,
Joel Fernandes <joel@...lfernandes.org>,
Mathieu Desnoyers <mathieu.desnoyers@...icios.com>,
Gabriele Paoloni <gabriele.paoloni@...el.com>,
Juri Lelli <juri.lelli@...hat.com>,
Clark Williams <williams@...hat.com>, linux-doc@...r.kernel.org
Subject: [RFC PATCH 00/16] The Runtime Verification (RV) interface
Over the last years, I've been exploring the possibility of
verifying the Linux kernel behavior using 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 usage of deterministic automaton for RV is a well-established
approach. In the specific case of the Linux kernel, you can check how
to model complex behavior of the Linux kernel with this paper:
DE OLIVEIRA, Daniel Bristot; CUCINOTTA, Tommaso; DE OLIVEIRA, Rômulo Silva.
*Efficient formal verification for the Linux kernel.* In: International
Conference on Software Engineering and Formal Methods. Springer, Cham, 2019.
p. 315-332.
And how efficient is this approach here:
DE OLIVEIRA, Daniel B.; DE OLIVEIRA, Rômulo S.; CUCINOTTA, Tommaso. *A thread
synchronization model for the PREEMPT_RT Linux kernel.* Journal of Systems
Architecture, 2020, 107: 101729.
tlrd: it is possible to model complex behaviors in a modular way, with
an acceptable overhead (even for production systems). See this
presentation at 2019's ELCE: https://www.youtube.com/watch?v=BfTuEHafNgg
Here I am proposing a more practical approach for the usage of deterministic
automata for runtime verification, and it includes:
- An interface for controlling the verification.
- A tool and set of headers that enables the automatic code
generation of the RV monitor (Monitor Synthesis).
Given that RV is a tracing consumer, the code is being placed inside the
tracing subsystem (Steven and I have been talking about it for a while).
In this RFC I am still not proposing any complex model. Instead, I am
presenting only simple monitors that help to illustrate the usage of
the automatic code generation and the RV interface. This is important to
enable other researchers and developers to start using/extending this method.
It is also worth mentioning that this work has been heavily motivated by
the usage of Linux on safety critical systems, mainly by the people
involved in the Elisa Project. Indeed, we will be talking about the
usage of RV in this field on today's presentation:
A Maintainable and Scalable Kernel Qualification Approach for Automotive
Gabriele Paoloni, Intel Corporation & Daniel Bristot de Oliveira, Red Hat
At the Elisa workshop.
The more academic concepts behind this approach have been discussed with
some researchers, including:
- Romulo Silva de Oliveira - Universidade Federal de Santa Catarina
(BR)
- Tommaso Cucinotta - Scuola Superiore Sant'Anna (IT)
- Srdan Krstic - ETH Zurich (CH)
- Dmitriy Traytel - University of Copenhagen (DK)
Thanks!
Daniel Bristot de Oliveira (16):
rv: Add Runtime Verification (RV) interface
rv: Add runtime reactors interface
rv/include: Add helper functions for deterministic automata
rv/include: Add deterministic automata monitor definition via C macros
rv/include: Add tracing helper functions
tools/rv: Add dot2c
tools/rv: Add dot2k
rv/monitors: Add the wip monitor skeleton created by dot2k
rv/monitors: wip instrumentation and Makefile/Kconfig entries
rv/monitors: Add the wwnr monitor skeleton created by dot2k
rv/monitors: wwnr instrumentation and Makefile/Kconfig entries
rv/reactors: Add the printk reactor
rv/reactors: Add the panic reactor
rv/docs: Add a basic documentation
rv/docs: Add deterministic automata monitor synthesis documentation
rv/docs: Add deterministic automata instrumentation documentation
Documentation/trace/index.rst | 1 +
.../trace/rv/da_monitor_instrumentation.rst | 230 ++++++
.../trace/rv/da_monitor_synthesis.rst | 286 +++++++
Documentation/trace/rv/index.rst | 9 +
.../trace/rv/runtime-verification.rst | 233 ++++++
include/linux/rv.h | 31 +
include/rv/automata.h | 52 ++
include/rv/da_monitor.h | 336 +++++++++
include/rv/trace_helpers.h | 69 ++
kernel/trace/Kconfig | 2 +
kernel/trace/Makefile | 2 +
kernel/trace/rv/Kconfig | 60 ++
kernel/trace/rv/Makefile | 8 +
kernel/trace/rv/monitors/wip/model.h | 38 +
kernel/trace/rv/monitors/wip/wip.c | 124 ++++
kernel/trace/rv/monitors/wip/wip.h | 64 ++
kernel/trace/rv/monitors/wwnr/model.h | 38 +
kernel/trace/rv/monitors/wwnr/wwnr.c | 122 +++
kernel/trace/rv/monitors/wwnr/wwnr.h | 70 ++
kernel/trace/rv/reactors/panic.c | 44 ++
kernel/trace/rv/reactors/printk.c | 43 ++
kernel/trace/rv/rv.c | 700 ++++++++++++++++++
kernel/trace/rv/rv.h | 50 ++
kernel/trace/rv/rv_reactors.c | 478 ++++++++++++
kernel/trace/trace.c | 4 +
kernel/trace/trace.h | 2 +
tools/tracing/rv/dot2/Makefile | 26 +
tools/tracing/rv/dot2/automata.py | 179 +++++
tools/tracing/rv/dot2/dot2c | 30 +
tools/tracing/rv/dot2/dot2c.py | 240 ++++++
tools/tracing/rv/dot2/dot2k | 49 ++
tools/tracing/rv/dot2/dot2k.py | 184 +++++
.../rv/dot2/dot2k_templates/main_global.c | 96 +++
.../rv/dot2/dot2k_templates/main_global.h | 64 ++
.../rv/dot2/dot2k_templates/main_per_cpu.c | 96 +++
.../rv/dot2/dot2k_templates/main_per_cpu.h | 64 ++
.../rv/dot2/dot2k_templates/main_per_task.c | 96 +++
.../rv/dot2/dot2k_templates/main_per_task.h | 70 ++
38 files changed, 4290 insertions(+)
create mode 100644 Documentation/trace/rv/da_monitor_instrumentation.rst
create mode 100644 Documentation/trace/rv/da_monitor_synthesis.rst
create mode 100644 Documentation/trace/rv/index.rst
create mode 100644 Documentation/trace/rv/runtime-verification.rst
create mode 100644 include/linux/rv.h
create mode 100644 include/rv/automata.h
create mode 100644 include/rv/da_monitor.h
create mode 100644 include/rv/trace_helpers.h
create mode 100644 kernel/trace/rv/Kconfig
create mode 100644 kernel/trace/rv/Makefile
create mode 100644 kernel/trace/rv/monitors/wip/model.h
create mode 100644 kernel/trace/rv/monitors/wip/wip.c
create mode 100644 kernel/trace/rv/monitors/wip/wip.h
create mode 100644 kernel/trace/rv/monitors/wwnr/model.h
create mode 100644 kernel/trace/rv/monitors/wwnr/wwnr.c
create mode 100644 kernel/trace/rv/monitors/wwnr/wwnr.h
create mode 100644 kernel/trace/rv/reactors/panic.c
create mode 100644 kernel/trace/rv/reactors/printk.c
create mode 100644 kernel/trace/rv/rv.c
create mode 100644 kernel/trace/rv/rv.h
create mode 100644 kernel/trace/rv/rv_reactors.c
create mode 100644 tools/tracing/rv/dot2/Makefile
create mode 100644 tools/tracing/rv/dot2/automata.py
create mode 100644 tools/tracing/rv/dot2/dot2c
create mode 100644 tools/tracing/rv/dot2/dot2c.py
create mode 100644 tools/tracing/rv/dot2/dot2k
create mode 100644 tools/tracing/rv/dot2/dot2k.py
create mode 100644 tools/tracing/rv/dot2/dot2k_templates/main_global.c
create mode 100644 tools/tracing/rv/dot2/dot2k_templates/main_global.h
create mode 100644 tools/tracing/rv/dot2/dot2k_templates/main_per_cpu.c
create mode 100644 tools/tracing/rv/dot2/dot2k_templates/main_per_cpu.h
create mode 100644 tools/tracing/rv/dot2/dot2k_templates/main_per_task.c
create mode 100644 tools/tracing/rv/dot2/dot2k_templates/main_per_task.h
--
2.26.2
Powered by blists - more mailing lists