linux-kernel - Re: [PATCH v7 13/22] rv: Add support for LTL monitors

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

Hash Suite: Windows password security audit tool. GUI, reports in PDF.

[<prev] [next>] [<thread-prev] [day] [month] [year] [list]

Message-ID: <20250509152321.zsiacCwk@linutronix.de>
Date: Fri, 9 May 2025 17:23:21 +0200
From: Nam Cao <namcao@...utronix.de>
To: Gabriele Monaco <gmonaco@...hat.com>
Cc: john.ogness@...utronix.de, Steven Rostedt <rostedt@...dmis.org>,
	linux-trace-kernel@...r.kernel.org, linux-kernel@...r.kernel.org
Subject: Re: [PATCH v7 13/22] rv: Add support for LTL monitors

On Fri, May 09, 2025 at 04:50:29PM +0200, Gabriele Monaco wrote:
> On Fri, 2025-05-09 at 10:12 +0200, Nam Cao wrote:
> > +    def negate(self):
> > +        # ![]F == <>(!F)
> > +        return EventuallyOp(self.left,
> > self.right.negate()).normalize()
> 
> Shouldn't this be:
>   +        return EventuallyOp(self.child.negate()).normalize()

Yes, remnant of the old version :(

> > +def p_unop(p):
> > +    '''
> > +    unop : ALWAYS ltl
> > +         | EVENTUALLY ltl
> > +         | NOT ltl
> > +    '''
> > +    if p[1] == "always":
> > +        op = AlwaysOp(p[2])
> > +    if p[1] == "eventually":
> > +        op = EventuallyOp(p[2])
> > +    if p[1] == "not":
> > +        op = NotOp(p[2])
> 
> Pylint is complaining about this one, wouldn't it be better changing it to an
> if/elif chain and addding:
> 
>     else:
>         raise ValueError("Invalid unary operator: %s" % p[1])

lex should have failed due to unknown token before getting here. But yes,
this would be a good change.

> > +def parse_ltl(s: str) -> ASTNode:
> > +    spec = parser.parse(s)
> > +
> > +    subexpr = dict()
> > +
> > +    for assign in spec:
> > +        if assign[0] == "RULE":
> > +            rule = assign[1]
> > +        else:
> > +            subexpr[assign[0]] = assign[1]
> 
> rule may be undefined here (but I guess python will just say variable rule is
> undefined and it would be quite clear the ltl didn't start with a rule.

We could make the error verbose.

> I'm still getting a few more errors but my model may be to blame, still need to
> play a bit.

Feel free to send me the model. Maybe it is a bug in the script. But I
would be happy to help debugging your model as well.

Thanks for the feedback,
Nam