Klever

Ilja Zakharov has finished works on Google Summer of Code 2016 project "Environment model specifications for more bugs to reveal" for The Linux Foundation.

During the project Ilja has ported all environment model specifications and tests to a new process calculus based environment model generator and implemented new environment model specifications to improve precision of environment models generated during static verification of Linux kernel modules. Moreover, a lot of work has been done to fix bugs in the environment model generator and to implement new features in it. For instance, Ilja has implemented a feature to generate simplified models for huge drivers to get a chance to a verification tool to finish analysis within a reasonable time.

As a result of this work, overall verification false positive rate has been decreased to 75% and a number of missing target bugs has been decreased to 40% from 60% (number of missed confirmed bugs that should be able to detect with our verification system).

Ilja's commits to the environment model generator and specifications sets (commits.ods) have already been reviewed and merged into the master branch of the upstream repository.

Patches to fix errors found with the environment model generator and new specification sets submitted by Ilja's mentor Alexey Khoroshilov:

1. https://patchwork.kernel.org/patch/8999941/
2. https://patchwork.kernel.org/patch/9094121/
3. https://patchwork.kernel.org/patch/9130115/
4. https://patchwork.kernel.org/patch/9154199/
5. https://patchwork.kernel.org/patch/9206223/
6. https://patchwork.kernel.org/patch/9221835/
7. https://patchwork.kernel.org/patch/9232893/
8. https://patchwork.kernel.org/patch/9262359/
9. https://patchwork.kernel.org/patch/9276095/
10. https://patchwork.kernel.org/patch/9276093/