linux-kernel - Re: [PATCH] docs: kbuild: add references on Kconfig semantics

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: <CAK7LNAT=7=kPQP3+Nf0gyRZGbXE19=wSu3NOanrzuM2gLHE1Rw@mail.gmail.com>
Date:   Wed, 6 Apr 2022 23:53:38 +0900
From:   Masahiro Yamada <masahiroy@...nel.org>
To:     Necip Fazil Yildiran <fazilyildiran@...il.com>
Cc:     Linux Kernel Mailing List <linux-kernel@...r.kernel.org>,
        "open list:DOCUMENTATION" <linux-doc@...r.kernel.org>,
        Linux Kbuild mailing list <linux-kbuild@...r.kernel.org>,
        paul@...zz.com
Subject: Re: [PATCH] docs: kbuild: add references on Kconfig semantics

On Tue, Apr 5, 2022 at 1:34 PM Necip Fazil Yildiran
<fazilyildiran@...il.com> wrote:
>
> Add references to 1) a research paper which provides a definition of
> Kconfig semantics, 2) the kismet tool, which checks for unmet direct
> dependency bugs in Kconfig specifications.
>
> Signed-off-by: Paul Gazzillo <paul@...zz.com>
> Signed-off-by: Necip Fazil Yildiran <fazilyildiran@...il.com>
> ---

Applied to linux-kbuild. Thanks.


>  Documentation/kbuild/kconfig-language.rst | 6 ++++++
>  1 file changed, 6 insertions(+)
>
> diff --git a/Documentation/kbuild/kconfig-language.rst b/Documentation/kbuild/kconfig-language.rst
> index 93a5b6e1fabd..a7173843a294 100644
> --- a/Documentation/kbuild/kconfig-language.rst
> +++ b/Documentation/kbuild/kconfig-language.rst
> @@ -693,6 +693,8 @@ in documenting basic Kconfig syntax a more precise definition of Kconfig
>  semantics is welcomed. One project deduced Kconfig semantics through
>  the use of the xconfig configurator [1]_. Work should be done to confirm if
>  the deduced semantics matches our intended Kconfig design goals.
> +Another project formalized a denotational semantics of a core subset of
> +the Kconfig language [10]_.
>
>  Having well defined semantics can be useful for tools for practical
>  evaluation of dependencies, for instance one such case was work to
> @@ -700,6 +702,8 @@ express in boolean abstraction of the inferred semantics of Kconfig to
>  translate Kconfig logic into boolean formulas and run a SAT solver on this to
>  find dead code / features (always inactive), 114 dead features were found in
>  Linux using this methodology [1]_ (Section 8: Threats to validity).
> +The kismet tool, based on the semantics in [10]_, finds abuses of reverse
> +dependencies and has led to dozens of committed fixes to Linux Kconfig files [11]_.
>
>  Confirming this could prove useful as Kconfig stands as one of the leading
>  industrial variability modeling languages [1]_ [2]_. Its study would help
> @@ -738,3 +742,5 @@ https://kernelnewbies.org/KernelProjects/kconfig-sat
>  .. [7] https://vamos.cs.fau.de
>  .. [8] https://undertaker.cs.fau.de
>  .. [9] https://www4.cs.fau.de/Publications/2011/tartler_11_eurosys.pdf
> +.. [10] https://paulgazzillo.com/papers/esecfse21.pdf
> +.. [11] https://github.com/paulgazz/kmax
> --
> 2.25.1
>


-- 
Best Regards
Masahiro Yamada