linux-kernel - Re: Follow-up on Linux-kernel code accessibility

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] [thread-next>] [day] [month] [year] [list]

Message-ID: <89258fb3-4e2b-4461-9794-662b0e92349d@paulmck-laptop>
Date: Fri, 19 Dec 2025 16:31:52 -0800
From: "Paul E. McKenney" <paulmck@...nel.org>
To: Julia Lawall <julia.lawall@...ia.fr>
Cc: Gabriele Paoloni <gpaoloni@...hat.com>,
	Steven Rostedt <rostedt@...dmis.org>,
	Kate Stewart <kstewart@...uxfoundation.org>,
	Chuck Wolber <chuckwolber@...il.com>,
	Dmitry Vyukov <dvyukov@...gle.com>,
	Mark Rutland <mark.rutland@....com>,
	Thomas Gleixner <tglx@...utronix.de>,
	Lorenzo Stoakes <lorenzo.stoakes@...cle.com>,
	Shuah Khan <skhan@...uxfoundation.org>,
	linux-kernel@...r.kernel.org
Subject: Re: Follow-up on Linux-kernel code accessibility

On Fri, Dec 19, 2025 at 07:51:47AM +0100, Julia Lawall wrote:
> Maybe we're not looking for an instant understanding methodology.  Rather
> a machine checkable way to document the invariants that exist in the head
> of the developer, and for some bounded amount of time in the head of the
> person who has tried to reconstruct them.

I like that goal.  Much easier to evaluate the results than for
improving learning, for one thing.

> There are different levels of specifications that one can write.  In Japan
> Imentioned how for the enable-disable ftrace function, I enumerated all of
> the permutations of the if tests, resulting in hundreds of lines of
> specifications, but after two failed attempts, the third attempt yielded
> both valid specifications and some insight into what the function was
> doing.  This insight could potentially be used to make some higher level
> specifications that would be even more concise than the current
> English-language ones.  Maybe the low-level ones could be made
> automatically in many cases, or regenerated automatically from some hints.
> But the low-level ones may be needed to make the bridge between the code
> and the high-level specification.

If it was easy, we would already be doing it?  ;-)

							Thanx, Paul