1. Devel
  2. Topics

ELISA Webinar #2: Linux Driver Verification & KLEVER, Evgeny Novikov, ISPRAS #poll

Lukas Bulwahn
 

Linux Driver Verification & KLEVER: Applying formal methods on the Linux kernel for various years
Presenter: Evgeny Novikov, ISPRAS

Date to be voted.
Time: 22:00 JST; 21:00 CST; 16:00 MSK; 15:00 CEST; 06:00 PDT   

 

Agenda:

Formal methods help to ensure the highest level of software quality that can contribute to the activities for safety and security-related projects. But as a rule they are successfully applied just for small, specially prepared programs (a dozen KLOC at most). The Linux kernel represents a huge, rapidly developed, legacy software. Researchers and developers constantly try to leverage formal methods to various parts of the Linux kernel. I would like to introduce you software verification framework Klever [1] that we have been developing more than 10 years at the Linux Verification Center [2] within the Linux Driver Verification (LDV) [3] program.
 
Klever allows automated checking of Linux kernel loadable modules and subsystems against a variety of safety and security requirements using software verification tools implementing such methods of thorough static analysis as Bounded Model Checking [4] and Counterexample-Guided Abstraction Refinement [5]. Klever can complement traditional software quality assurance tools for code review, testing and static analysis. In contrast to various kinds of testing the framework treats all execution paths and checks for requirements according to provided specifications. Unlike static analysis tools, it proves formal correctness of programs checked against particular requirements under certain assumptions. Altogether this enables revealing tricky faults in software including crucial ones. Concerning verification of the Linux kernel, this framework already demonstrated an ability to detect faults [6], many of which can be hardly found out by other techniques.
 
Potentially, Klever is able to detect much more if one invests in developing specifications, conducting verification, analysis of verification results and reporting bugs. We consider possible directions for further development of Klever that can contribute verification of the Linux kernel in some way in this document:
 
https://docs.google.com/document/d/11e7cDzRqx0nO1UBcM75l6MS28zRBJUicXdNiReEpDKI/edit
 
Everything related with verification of the Linux kernel in Klever is open source [7].
 
[1] https://forge.ispras.ru/projects/klever
[2] http://linuxtesting.org/
[3] http://linuxtesting.org/ldv
[4] https://link.springer.com/article/10.1023/A:1011276507260
[5] https://link.springer.com/chapter/10.1007/10722167_15
[6] https://git.kernel.org/pub/scm/linux/kernel/git/stable/linux.git/log/?qt=grep&q=Found+by+Linux+Driver+Verification
[7] https://github.com/ldv-klever/klever

Evgeny, please let us know in a separate email which dates fit you.

Results

See Who Responded

Lukas Bulwahn
 

If you have not voted yet for a suitable date for the second webinar, here is your last chance. Voting ends in 24 hours from now.

Lukas Bulwahn
 

Dear all,

 

 

Voting has ended. There was a tie between 2019-05-27 and 2019-05-30. I rechecked my calendar and decided to make 2019-05-27 possible on my side and hence with that change in votes, 2019-05-27 took the lead.

 

I will clarify if Evgeny can work with a Skype for Business session, and then ask Tobias Jordan if he can set up the Skype session as last time, which worked acceptably fine as far as I know.

 

As I discussed with Evgeny off-list, Evgeny will make his slides publicly available and he would like to also publish the recording of his presentation.

Hence, for the next webinar, we would like to change the policy for the recording:

 

The presentation will be provided publicly on the ELISA webpage (and we could consider uploading it to youtube or some other portal to increase outreach dependent on decision of the outreach committee.) Hence, all voices for questions will be captured and made public.

 

We will not publish the list of listeners. If you do not want to be part of the recording, you can ask questions on the chat and the moderator would ask them on your behalf (without naming you).

 

I hope this policy is acceptable to everyone. If not, please inform me and we can think about any changes that would address your concern.

 

 

Best regards,

 

Lukas

1 - 3 of 3