[ldv-project] Most important missed features and crucial bugs of Klever

Tue Jan 22 12:33:27 MSK 2019

Dear Evgeny,

This list of activities is looking very promising and going in the right direction.

(To be very honest: my personal interest in LDV/Klever has been eaten up by the pushbacks and difficulties we encountered last year. Despite all the support you provided and advances you built in Klever last year, it was just not yet ready for showing the results that I was hoping for. I personally will continue to investigate in syzkaller, but my assessment of Klever’s potential is still positive, and the quantative data I collected shows that LDV is still a promising tool in the Linux kernel development.

May I share this document with other potential stakeholders, the ELISA collaboration project and other interested parties through my expert network and with Linux Foundation?

Best regards,

Lukas

From: Evgeny Novikov <novikov at ispras.ru>
Date: Tuesday 2019-01-22 at 08:57
To: LDV list <ldv-project at ispras.ru>, "ldv-project at linuxtesting.org" <ldv-project at linuxtesting.org>, Alexander Petrenko <petrenko at ispras.ru>, "Bulwahn Lukas, JC-22" <Lukas.Bulwahn at bmw.de>, "mSzczepankiewicz at exida.com" <mSzczepankiewicz at exida.com>
Subject: Re: [ldv-project] Most important missed features and crucial bugs of Klever

Dear colleagues,

At last we completed internal discussions of further development of Klever in favor of verification of the Linux kernel. Here is the result:

https://docs.google.com/document/d/11e7cDzRqx0nO1UBcM75l6MS28zRBJUicXdNiReEpDKI/edit?usp=sharing

We would be glad to receive any feedback in addition to the one you provided thus far.

--
Evgeny Novikov
Linux Verification Center, ISP RAS
http://linuxtesting.org

25.11.2018, 21:04, "Evgeny Novikov" <novikov at ispras.ru>:
Until the mentioned date we did not receive feature/bug lists from anybody. I guess that this is because the task is not trivial at all. Without really deep understanding one can not reason about Klever pros and cons well enough. There are no straightforward analogues of Klever in industry, so, nobody can say easily, that X has such features while Klever does not have them.

From the other side people, who are aware much about Klever internals, can rank missed features and crucial bugs in quite an incorrect way. For instance, I dislike inefficient weaving very much but for many users better support of new versions and non-standard configurations of the Linux kernel is necessary much more.

Let's try another approach. The core development team will suggest an initial list of important features and bugs. They will be higher-level than ones in our issue tracker<https://forge.ispras.ru/projects/klever/issues?set_filter=1>. Then everybody will be able to suggest any improvements to be discussed. I hope that we will complete the former in 2-3 weeks, and we will finish discussion until the end of this year or the early beginning of the following year.

--
Evgeny Novikov
Linux Verification Center, ISP RAS
http://linuxtesting.org<http://linuxtesting.org/>

14.11.2018, 19:31, "Evgeny Novikov" <novikov at ispras.ru<mailto:novikov at ispras.ru>>:
Dear developers, users and experts!

We would like to collect your opinions about most important features that are missed in Klever as well as crucial bugs that Klever has at the moment. This survey will help us to evaluate better possible directions of future development.

Please, enumerate features and bugs that you treat most vital. We will assume that items that you will put earlier in a list have a larger priority for you. Examples are "Klever does not support verification of loadable kernel modules of recent versions of the Linux kernel", "Klever lacks documentation on development of requirement specifications", "Klever needs more user-friendly interface".

We will summarize your feedback on November 23, but we are looking forward for your opinion at any time.

Best regards,
Evgeny Novikov

--
Evgeny Novikov
Linux Verification Center, ISP RAS
http://linuxtesting.org<http://linuxtesting.org/>

-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://linuxtesting.org/pipermail/ldv-project/attachments/20190122/95e2b40e/attachment.html>