[ldv-project] Klever tutorial

[Evgeny Novikov]

Hi Lukas,

It would be great if you will try our framework yourself and encourage others who have some interest in analysis and verification of the Linux kernel. We expect an always valuable feedback!

Until we developed at least the basic documentation it was impossible to use Klever without much help from developers. And this obstacle forced most potential users to give up their attempts to get anything meaningful after all. Hopefully we substantially improved Klever deployment scripts and instructions (in particular, thanks to notes from you, Michal and some other users) so that I believe now it is pretty easy to install Klever. Besides, we considerably changed the user interface and underlying internals to make them more reliable, fast and convenient for a common workflow and added a basic support for verification of several new versions of the Linux kernel. At last, now you can see a tutorial that describes a basic use case, i.e. searching for bugs.

Most likely, you and other users will meet some unexpected issues while some points may be unclear. So, we will have to fix the tutorial and maybe something in the code. After that one will be able to detect bugs like we do (http://linuxtesting.org/results/ldv). And most likely you will understand better why different tasks mentioned at https://docs.google.com/document/d/11e7cDzRqx0nO1UBcM75l6MS28zRBJUicXdNiReEpDKI/edit do matter. Different users will need different improvements and fixes in Klever components and specifications. But that will be another story.

-- 
Best regards,
Evgeny Novikov

28.04.2020, 09:28, "lukas.bulwahn at bmw.de" <lukas.bulwahn at bmw.de>:
> Hi Evgeny,
>
>>  We are glad to announce that we are very close to release Klever 3.0 and there
>>  is the first version of the Klever tutorial:
>>  https://docs.google.com/document/d/1GBYmVZgjk0e8R-
>>  KV4WkZeQ1YDqYhavjvoDTlDe_hbCQ/edit#
>>  Everybody is welcome for reviewing, for discussing and for using Klever.
>
> I certainly appreciate the effort on your side, and I hope we are able to give you something in return for your efforts (e.g., attention among the kernel community, the support needed around LDV and more).
>
> I might try out Klever 3.0 on a latest supported Linux kernel on the weekend and report my experience. If it successful, I suggest that we use this written tutorial to reach out to others interested in static analysis tooling around the Linux kernel. I can organize that and do that once I know the basic documentation is there to get everyone fairly well started.
>
> Lukas