Klever: Newshttps://forge.ispras.ru/https://forge.ispras.ru/favicon.ico?16490126692022-08-26T15:59:33ZOpen-Source Projects
Redmine Klever 3.7https://forge.ispras.ru/news/7682022-08-26T15:59:33ZEvgeny Novikovnovikov@ispras.ru
<p>Klever <a class="version" href="https://forge.ispras.ru/versions/505">3.7</a> was primarily devoted to improving a quality of verification results for Linux kernel drivers. After all about 43% of original false alarms issued when checking memory safety have gone.</p>
<p>Following fixes and improvements in Klever <a class="version" href="https://forge.ispras.ru/versions/505">3.7</a> deserve an attention:</p>
<ul>
<li>Adding new environment models for the Linux kernel:
<ul>
<li>Modeling the <em>list</em> API.</li>
<li>Modeling the <em>kref</em> API.</li>
<li>Adding model for the <em>input_ff_create_memless()</em> function.</li>
<li>Adding models for <em>check_add_overflow()</em>, <em>check_sub_overflow()</em> and <em>check_mul_overflow()</em> macros that fixes the <em>struct_size()</em> model for new versions of the Linux kernel.</li>
<li>Modeling <em>v4l2_device</em>(un)register()_ functions.</li>
<li>Modeling the <em>i2c_match_id()</em> function.</li>
<li>Adding model for the <em>dev_err_probe()</em> function.</li>
<li>Adding models for the dynamic debug printing API.</li>
</ul>
</li>
<li>Fixing existing environment models for the Linux kernel:
<ul>
<li>Modeling failures for <em>calloc()</em> and <em>zalloc()</em>.</li>
<li>Fixing the off-by-one error when choosing a device from <em>MODULE_DEVICE_TABLE</em>.</li>
<li>Passing the same resource to probe and remove for HID drivers.</li>
<li>Allocating memory for <em>inode</em> for <em>file_operations</em> callbacks.</li>
<li>Allocating memory for <em>tty_struct</em> for <em>tty_operations</em> callbacks.</li>
<li>Avoiding using implicit resources in environment model specifications.</li>
</ul>
</li>
<li>Adding a new section to the user documentation: <a href="https://klever.readthedocs.io/en/latest/verifying_new_program.html" class="external">Verifying New Program</a>.</li>
<li>Fixing tests for environment model specifications and Environment Model Generator.</li>
<li>Updating CIF which main file was rewritten in C++ and that started to print keyword <em>static</em> for local variables.</li>
<li>Updating CPAchecker that supports packed/aligned attributes and issues violation witnesses more efficiently.</li>
<li>Updating Python dependencies.</li>
</ul>
<p>We would like to thank very much everybody who made this great job possible!</p> Klever 3.6https://forge.ispras.ru/news/7652022-06-26T06:50:50ZEvgeny Novikovnovikov@ispras.ru
<p>Klever <a class="version" href="https://forge.ispras.ru/versions/500">3.6</a> was released pretty soon after Klever <a class="version" href="https://forge.ispras.ru/versions/454">3.5</a> since we updated Clade and CIF in the backward incompatible manner. This means that the new version of Klever requires all build bases to be regenerated with the new version of Clade and CIF installed together with Klever. You can download build bases for Linux 5.5.19, 5.10.120 and 5.17.13 as well as sample build bases prepared ahead of time. Corresponding files are available either directly from the "Files" tab or from the <a href="https://klever.readthedocs.io/en/v3.6/tutorial.html#preparing-build-bases" class="external">Klever tutorial</a>.</p>
<p>Other changes in Klever <a class="version" href="https://forge.ispras.ru/versions/500">3.6</a> are new models for <em>struct_size()</em> and underlying __<em>ab_c_size()</em> for the Linux kernel.</p> Klever 3.5https://forge.ispras.ru/news/7642022-05-27T12:36:32ZEvgeny Novikovnovikov@ispras.ru
<p>We released Klever <a class="version" href="https://forge.ispras.ru/versions/454">3.5</a> that has following noticeable changes:</p>
<ul>
<li>Improving support for verification of Linux 5.10 and Linux 5.17 (new specifications set "5.17" was added). </li>
<li>Environment models generated at verification of Linux loadable kernel modules do not contain infinite loops anymore. This accelerated analysis and did not result in any degradation in the quality of verification results.</li>
<li>Using <a href="https://wiki.ubuntu.com/FocalFossa/ReleaseNotes" class="external">Ubuntu 20.04</a>, <a href="https://wiki.debian.org/DebianBullseye" class="external">Debian 11</a> and <a href="https://doc.opensuse.org/release-notes/x86_64/openSUSE/Leap/15.3/" class="external">openSUSE 15.3</a> as preferable Linux distributions for deployment of Klever.</li>
<li>Switching to Python 3.10. You should carefully read this <a href="https://forge.ispras.ru/issues/10937#note-7" class="external">comment</a> if you are going to update existing local instances of Klever.</li>
<li>Supporting regular expressions for assessing unsafes (you can see <a class="issue tracker-4 status-5 priority-5 priority-high3 closed behind-schedule" title="Feature: Add pattern search to error traces comparison functions (Closed)" href="https://forge.ispras.ru/issues/11513">#11513</a> for more details).</li>
<li>Updating <a href="https://klever.readthedocs.io/en/v3.5/tutorial.html" class="external">Klever Tutorial</a>, in particular using verification of loadable kernel modules of Linux 5.5 as an example.</li>
<li>Updating add-ons and verification back-ends (various bug fixes and optimizations).</li>
<li>More advanced authorization of new users. Now the administrator should activate new users while somebody should grant them access to some jobs.</li>
</ul>
<p>Many thanks to everybody involved!</p> Klever contributor Ilya Shchepetkov started a new positionhttps://forge.ispras.ru/news/7622022-03-24T16:03:56ZEvgeny Novikovnovikov@ispras.ru
<p>Ilya Shchepetkov gave us a lot of brilliant ideas, considerably improved Klever deployment facilities, developed <a href="https://github.com/17451k/clade" class="external">Clade</a> and contributed to <a href="https://forge.ispras.ru/projects/cif" class="external">CIF</a> (Klever actively uses both these tools at various stages of its operation). We would like to thank him from the bottom of our hearts and wish him new great achievements as a Senior Research Developer at <a href="https://www.kaspersky.com/" class="external">Kaspersky</a>.</p> Klever 3.4https://forge.ispras.ru/news/7612022-02-24T15:07:45ZEvgeny Novikovnovikov@ispras.ru
<p>Klever <a class="version" href="https://forge.ispras.ru/versions/431">3.4</a> includes the following prominent features:</p>
<ul>
<li>Several improvements contributing development and generation of environment models:
<ul>
<li>Ability to specify savepoints for the main process.</li>
<li>Ability to select scenarios for particular savepoints manually.</li>
<li>Ability to configure the number of iterations for invocation of callbacks.</li>
<li>Providing users with a graphical representation of environment models directly in the Klever web UI.</li>
</ul>
</li>
<li>Models for <em>kmem_cache</em> functions for the Linux kernel.</li>
<li>Updating add-ons and verification back-ends (various bug fixes and optimizations).</li>
<li>New sections in the user documentation: <a href="https://klever.readthedocs.io/en/latest/dev_decomposition_conf.html" class="external">Configuring Program Decomposition</a> and <a href="https://klever.readthedocs.io/en/latest/dev_verifier_profiles.html" class="external">Development of Verifier Profiles</a>.</li>
<li>Besides, you can find the <a href="https://cif.readthedocs.io/en/latest/index.html" class="external">CIF’s user documentation</a> that may be helpful at development of advanced specifications and models.</li>
<li>Many fixes and minor improvements that make the specification development and verification workflow more easy, correct and reliable.</li>
</ul>
<p>We highly appreciate efforts of developers and the feedback from users who made this release possible!</p> Klever top contributor Ilja Zakharov started a new jobhttps://forge.ispras.ru/news/7582021-12-07T13:51:38ZEvgeny Novikovnovikov@ispras.ru
<p><a class="user active" href="https://forge.ispras.ru/users/388">Ilja Zakharov</a> was one of the greatest contributors to the Klever project. He was the primary developer of such components as Environment Model Generator, Program Fragment Generator, Schedulers and Controller. Besides, he created a lot of environment model specifications for different kinds of target programs and made considerable <a href="https://scholar.google.ru/citations?user=nvAuJScAAAAJ&hl=en" class="external">scientific researches</a>. We appreciate his work very much.</p>
<p>Recently Ilja Zakharov became a Verification Engineer at the <a href="https://runtimeverification.com" class="external">Runtime Verification</a> company. There he will be engaged in application of formal methods for smart contracts and tools used for their verification. We wish him good luck and hope that the gained experience will help him at the new position.</p> Klever 3.3https://forge.ispras.ru/news/7562021-10-20T17:05:21ZEvgeny Novikovnovikov@ispras.ru
<p>The most noticeable work in Klever <a class="version" href="https://forge.ispras.ru/versions/398">3.3</a> is a new section <a href="https://klever.readthedocs.io/en/latest/dev_env_model_specs.html" class="external">Development of Environment Model Specifications</a> in the user documentation. Besides, there are following considerable improvements:</p>
<ul>
<li>Fixing allocation of memory for arguments of callbacks of several vital Linux device driver types.</li>
<li>Enhancing environment model specifications for file systems.</li>
<li>Simplifying development of environment model specifications and fixing some bugs at their processing</li>
<li>Numerous enhancements of the Klever web UI that simplify several common use cases.</li>
<li>Updating dependencies and addons that make them more functional and robust.</li>
<li>Development of unit tests for deployment of Klever within the OpenStack cloud</li>
<li>Supporting deployment at openSUSE.</li>
<li>New section <a href="https://klever.readthedocs.io/en/latest/dev_common_api_models.html" class="external">Development of Common API Models</a> in the user documentation.</li>
</ul>
<p>We would like to thank those developers and users who actively contributed to Klever <a class="version" href="https://forge.ispras.ru/versions/398">3.3</a>!</p> Klever 3.2https://forge.ispras.ru/news/7552021-08-05T14:51:22ZEvgeny Novikovnovikov@ispras.ru
<p>The major improvement of Klever <a class="version" href="https://forge.ispras.ru/versions/374">3.2</a> is a new environment model generator that supports automated splitting of complex environment models into sets of smaller ones. This is extremely helpful at verification of large programs and program fragments when verification tools often can not provide definite answers within specified time limits.</p>
Other important changes are as follows:
<ul>
<li>Substantially fixed and enhanced representation of violation witnesses (error traces) and code coverage reports as well as navigation through them.</li>
<li>New environment models for the Linux kernel (the bitmap API and several functions working with strings).</li>
<li>New validation set on the base of faults found by Klever and fixed in the Linux kernel.</li>
<li>Supporting more reliable and efficient deployment of Klever within the OpenStack cloud.</li>
<li>New section <a href="https://klever.readthedocs.io/en/latest/tutorial.html#analysis-of-code-coverage-reports" class="external">Analysis of Code Coverage Reports</a> in the Klever tutorial.</li>
</ul>
<p>In addition, Klever <a class="version" href="https://forge.ispras.ru/versions/374">3.2</a> includes numerous minor improvements and bug fixes.</p>
<p>This release would not be possible without intensive work of developers and testers. Also, we always look forward and welcome a feedback from users.</p> Klever 3.1https://forge.ispras.ru/news/7532021-03-31T09:34:25ZEvgeny Novikovnovikov@ispras.ru
<p>Klever <a class="version" href="https://forge.ispras.ru/versions/362">3.1</a> was released!</p>
The new release has the following major changes:
<ul>
<li>Improved support for the ARM/ARM64 architecture.</li>
<li>New parts within the user documentation:
<ul>
<li><a href="https://klever.readthedocs.io/en/latest/cli.html" class="external">Klever CLI</a>.</li>
<li><a href="https://klever.readthedocs.io/en/latest/dev_req_specs.html" class="external">Development of Requirement Specifications</a>.</li>
</ul>
</li>
<li>Fixing existing models and specifications and development of the new ones:
<ul>
<li>Support deregistration of <em>pm_ops</em> callbacks.</li>
<li>Fixing models for <em>vmalloc()/vfree()</em> and friends.</li>
<li>Developing the model for <em>current</em>.</li>
</ul>
</li>
<li>Adding the ability to weave in models (<a class="issue tracker-4 status-5 priority-6 priority-high2 closed" title="Feature: Allow to weave in models with their aspects (Closed)" href="https://forge.ispras.ru/issues/10742">#10742</a>).</li>
<li>Allowing excluding common models (<a class="issue tracker-4 status-5 priority-6 priority-high2 closed" title="Feature: Allow excluding common models in job.json (Closed)" href="https://forge.ispras.ru/issues/10716">#10716</a>).</li>
<li>Suggesting working source trees automatically (most likely you will not need to specify them manually for new build bases).</li>
<li>Showing Klever version in Bridge.</li>
<li>Updating vital Klever addons and dependencies:
<ul>
<li><a href="https://github.com/17451k/clade/releases/tag/v3.4" class="external">Clade 3.4</a> (old build bases are not supported anymore).</li>
<li><a href="https://forge.ispras.ru/projects/cif/repository/110/revisions/746d8be0" class="external">CIF 746d8be</a>.</li>
<li><a href="https://forge.ispras.ru/projects/astraver/repository/framac/revisions/18d3be82" class="external">Frama-C 18d3be8</a> (switching from 18.0 to 20.0).</li>
<li><a href="https://github.com/sosy-lab/cpachecker/commit/4715b56" class="external">CPAchecker klever_fixes:36955</a>.</li>
<li><a href="https://github.com/sosy-lab/cpachecker/commit/3491764" class="external">CPALockator CPALockator-combat-mode:36901</a>.</li>
</ul>
</li>
<li>Support for the <a href="https://sky.ispras.ru" class="external">new OpenStack cloud at ISP RAS</a>.</li>
</ul>
<p>Many thanks to all contributors of Klever <a class="version" href="https://forge.ispras.ru/versions/362">3.1</a>!</p> Klever 3.0https://forge.ispras.ru/news/7512021-01-11T12:03:02ZEvgeny Novikovnovikov@ispras.ru
<p>Let’s start the new year 2021 with new Klever <a class="version" href="https://forge.ispras.ru/versions/264">3.0</a>!</p>
Among a lot of improvements and bug fixes, most significant changes in Klever <a class="version" href="https://forge.ispras.ru/versions/264">3.0</a> are as follows:
<ul>
<li>Support for verification of kernel loadable modules of Linux 5.5.</li>
<li>Support for verification of Linux kernel loadable modules on the ARM architecture.</li>
<li>Fixing and developing specifications for verification of Linux kernel loadable modules:
<ul>
<li>Fixing specifications for checking usage of clocks in drivers.</li>
<li>Support for checking usage of the RCU API.</li>
<li>Developing detailed specifications for USB serial drivers.</li>
<li>Improving environment models for runtime power management callbacks.</li>
<li>Using device identifiers from the driver tables.</li>
<li>Developing models for <em>devm</em> memory allocating functions.</li>
<li>Fixing <em>framebuffer_alloc/release</em> models.</li>
<li>Adding models for <em>request/release_firmware()</em>, <em>v4l2_i2c_subdev_init()</em> and <em>i2c_smbus_read_block_data()</em>.</li>
</ul>
</li>
<li>More user-friendly configuration for target program fragments and requirement specifications.</li>
<li>Development of preset tags for assessing most common false alarms.</li>
<li>Support for new internal data formats for enhancing and optimizing representation and assessment of verification results.</li>
<li>Support for cross-references for original program source files and models.</li>
<li>Update of all variants of the <a href="https://cpachecker.sosy-lab.org/" class="external">CPAchecker</a> verification back-end.</li>
<li>Switching to a special version of Frama-C developed within project <a class="project" href="https://forge.ispras.ru/projects/astraver">Deductive Verification Tools for Linux Kernel</a> from outdated and unmaintained CIL. Both tools are used for merging source files and optimizations like removing unused functions.</li>
<li>Using <em>systemd</em> scripts instead of <em>init.d</em> ones for Klever services.</li>
<li>Development of <a href="https://klever.readthedocs.io/en/latest/tutorial.html" class="external">Tutorial</a>.</li>
</ul>
<p>Klever <a class="version" href="https://forge.ispras.ru/versions/264">3.0</a> is not backward compatible with former versions of Klever, so, you need to remove existing instances if so and deploy Klever from scratch.</p>
<p>As usual many thanks are to everyone who participated in this release of Klever!</p>