| 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: <ce9ef5e41c17953010bd31d19e7d2840cd533066.camel@redhat.com>
Date: Fri, 11 Apr 2025 13:17:30 +0200
From: Gabriele Monaco <gmonaco@...hat.com>
To: Nam Cao <namcao@...utronix.de>, Steven Rostedt <rostedt@...dmis.org>,
linux-trace-kernel@...r.kernel.org, linux-kernel@...r.kernel.org
Cc: john.ogness@...utronix.de
Subject: Re: [PATCH v2 13/22] rv: Add support for LTL monitors
On Fri, 2025-04-11 at 09:37 +0200, Nam Cao wrote:
> 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.
>
> For these cases, linear temporal logic is more suitable as the
> specification language.
>
> Add support for linear temporal logic runtime verification monitor.
>
> For all the details, see the documentations added by this commit.
>
> Signed-off-by: Nam Cao <namcao@...utronix.de>
> ---
> Documentation/trace/rv/index.rst | 1 +
> .../trace/rv/linear_temporal_logic.rst | 97 +++
> Documentation/trace/rv/monitor_synthesis.rst | 141 ++++-
> include/linux/rv.h | 56 +-
> include/rv/ltl_monitor.h | 184 ++++++
> kernel/fork.c | 5 +-
> kernel/trace/rv/Kconfig | 7 +
> kernel/trace/rv/rv_trace.h | 47 ++
> tools/verification/rvgen/.gitignore | 3 +
> tools/verification/rvgen/Makefile | 2 +
> tools/verification/rvgen/__main__.py | 3 +-
> tools/verification/rvgen/rvgen/ltl2ba.py | 552
> ++++++++++++++++++
> tools/verification/rvgen/rvgen/ltl2k.py | 242 ++++++++
> .../verification/rvgen/templates/ltl2k/main.c | 102 ++++
> .../rvgen/templates/ltl2k/trace.h | 14 +
> 15 files changed, 1431 insertions(+), 25 deletions(-)
> create mode 100644 Documentation/trace/rv/linear_temporal_logic.rst
> create mode 100644 include/rv/ltl_monitor.h
> create mode 100644 tools/verification/rvgen/.gitignore
> create mode 100644 tools/verification/rvgen/rvgen/ltl2ba.py
> create mode 100644 tools/verification/rvgen/rvgen/ltl2k.py
> create mode 100644 tools/verification/rvgen/templates/ltl2k/main.c
> create mode 100644 tools/verification/rvgen/templates/ltl2k/trace.h
>
> diff --git a/Documentation/trace/rv/index.rst
> b/Documentation/trace/rv/index.rst
> index 8e411b76ec82..2a27f6bc9429 100644
> --- a/Documentation/trace/rv/index.rst
> +++ b/Documentation/trace/rv/index.rst
> ...
>
> diff --git a/include/linux/rv.h b/include/linux/rv.h
> index c7c18c06911b..c8320fa3a94b 100644
> --- a/include/linux/rv.h
> +++ b/include/linux/rv.h
> @@ -10,6 +10,10 @@
> #define MAX_DA_NAME_LEN 32
>
> #ifdef CONFIG_RV
> +#include <linux/bitops.h>
> +#include <linux/types.h>
> +#include <linux/array_size.h>
> +
> /*
> * Deterministic automaton per-object variables.
> */
> @@ -18,6 +22,52 @@ struct da_monitor {
> unsigned int curr_state;
> };
>
> +/*
> + * In the future, if the number of atomic propositions or the size
> of Buchi automaton is larger, we
> + * can switch to dynamic allocation. For now, the code is simpler
> this way.
> + */
> +#define RV_MAX_LTL_ATOM 32
> +#define RV_MAX_BA_STATES 32
> +
> +/**
> + * struct ltl_monitor - A linear temporal logic runtime verification
> monitor
> + * @states: States in the Buchi automaton. As Buchi automaton is
> a
> + * non-deterministic state machine, the monitor can be
> in multiple states
> + * simultaneously. This is a bitmask of all possible
> states.
> + * If this is zero, that means either:
> + * - The monitor has not started yet (e.g. because
> not all atomic propositions are
> + * known).
> + * - there is no possible state to be in. In other
> words, a violation of the
> + * LTL property is detected.
> + * @atoms: The values of atomic propositions.
> + * @unknown_atoms: Atomic propositions which are still unknown.
> + */
> +struct ltl_monitor {
> +#ifdef CONFIG_RV_LTL_MONITOR
> + DECLARE_BITMAP(states, RV_MAX_BA_STATES);
> + DECLARE_BITMAP(atoms, RV_MAX_LTL_ATOM);
> + DECLARE_BITMAP(unknown_atoms, RV_MAX_LTL_ATOM);
> +#endif
> +};
Mmh, we have a lot of those ifdefs in quite inappropriate places, but I
think we can do better than this.
What about something like:
#ifdef CONFIG_RV_LTL_MONITOR
struct ltl_monitor {
DECLARE_BITMAP(states, RV_MAX_BA_STATES);
DECLARE_BITMAP(atoms, RV_MAX_LTL_ATOM);
DECLARE_BITMAP(unknown_atoms, RV_MAX_LTL_ATOM);
};
static inline bool rv_ltl_valid_state(struct ltl_monitor *mon)
{
...
}
static inline bool rv_ltl_all_atoms_known(struct ltl_monitor *mon)
{
...
}
#else
/*
* Leave the struct empty not to use up space
* In a later patch we could do the same for DAs..
*/
struct ltl_monitor { };
#endif
> +
> +static inline bool rv_ltl_valid_state(struct ltl_monitor *mon)
> +{
> + for (int i = 0; i < ARRAY_SIZE(mon->states); ++i) {
> + if (mon->states[i])
> + return true;
> + }
> + return false;
> +}
> +
> +static inline bool rv_ltl_all_atoms_known(struct ltl_monitor *mon)
> +{
> + for (int i = 0; i < ARRAY_SIZE(mon->unknown_atoms); ++i) {
> + if (mon->unknown_atoms[i])
> + return false;
> + }
> + return true;
> +}
> +
> /*
> * Per-task RV monitors count. Nowadays fixed in
> RV_PER_TASK_MONITORS.
> * If we find justification for more monitors, we can think about
> @@ -27,11 +77,9 @@ struct da_monitor {
> #define RV_PER_TASK_MONITORS 1
> #define RV_PER_TASK_MONITOR_INIT (RV_PER_TASK_MONITORS)
>
> -/*
> - * Futher monitor types are expected, so make this a union.
> - */
> union rv_task_monitor {
> - struct da_monitor da_mon;
> + struct da_monitor da_mon;
> + struct ltl_monitor ltl_mon;
> };
>
> #ifdef CONFIG_RV_REACTORS
> diff --git a/include/rv/ltl_monitor.h b/include/rv/ltl_monitor.h
> new file mode 100644
> index 000000000000..78f5a1197665
> --- /dev/null
> +++ b/include/rv/ltl_monitor.h
You hate macros don't you? :)
Anyway I really like your approach, very neat.
> @@ -0,0 +1,184 @@
> +/* SPDX-License-Identifier: GPL-2.0 */
> +/**
> + * This file must be combined with the $(MODEL_NAME).h file
> generated by
> + * tools/verification/rvgen.
> + */
> +
> +#include <linux/args.h>
> +#include <linux/rv.h>
> +#include <linux/stringify.h>
> +#include <linux/seq_buf.h>
> +#include <rv/instrumentation.h>
> +#include <trace/events/task.h>
> +#include <trace/events/sched.h>
> +
> +#ifndef MONITOR_NAME
> +#error "MONITOR_NAME macro is not defined. Did you include
> $(MODEL_NAME).h generated by rvgen?"
> +#endif
> +
> +#ifdef CONFIG_RV_REACTORS
> +#define RV_MONITOR_NAME CONCATENATE(rv_, MONITOR_NAME)
> +static struct rv_monitor RV_MONITOR_NAME;
> +
> +static void rv_cond_react(struct task_struct *task)
> +{
> + if (!rv_reacting_on() || !RV_MONITOR_NAME.react)
> + return;
> + RV_MONITOR_NAME.react("rv: "__stringify(MONITOR_NAME)":
> %s[%d]: violation detected\n",
> + task->comm, task->pid);
> +}
> +#else
> +static void rv_cond_react(struct task_struct *task)
> +{
> +}
> +#endif
> +
> +static int ltl_monitor_slot = RV_PER_TASK_MONITOR_INIT;
> +
> +static void ltl_atoms_fetch(struct task_struct *task, struct
> ltl_monitor *mon);
> +static void ltl_atoms_init(struct task_struct *task, struct
> ltl_monitor *mon, bool task_creation);
> +
> +static struct ltl_monitor *ltl_get_monitor(struct task_struct *task)
> +{
> + return &task->rv[ltl_monitor_slot].ltl_mon;
> +}
This means ltl monitors only support per-task, right?
It shouldn't take much effort putting an ifdef chain here and defining e.g.
PER_CPU in the header file to choose a different get_monitor.
Or directly an ltl_monitor_implicit.h
I think this patch is ready without it, just trying to brainstorm how we could
potentially extend this.
I need more time to play with these, but it looks promising.
Thanks,
Gabriele
Powered by blists - more mailing lists