C Instrumentation Framework: CIF 1.2

Added by Evgeny Novikov about 1 month ago

The major enhancement for CIF 1.2 is that the main CIF source file was rewritten in C++. The new version is more abstract and it is easier to maintain and develop it further. Using C++ allows to avoid a lot of potential memory errors that we encountered and fixed earlier. Besides, the execution time was reduced by using another way of launching subprocesses. The latter made redundant escaping double quotes in command-line options passed to CIF.

We would like to thank Ilya Shchepetkov for this awesome job!

C Instrumentation Framework: CIF 1.1

Added by Evgeny Novikov about 1 month ago

CIF 1.1 was released!

There are following important changes and fixes:

  • Supporting additional special directive for source code queries:
    • $storage_class that allows to get storage classes for functions and variables.
    • $var_init_list_json that allows to print global variable initializers in JSON.
  • Fixing Aspectator to keep storage classes for variables.
  • Improving and fixing Aspectator’s C back-end:
    • Fixing initialization of anonymous unions.
    • Fixing conversion for strings containing hexadecimal escape sequences.
    • Increasing recursion limit from 10 to 100 to handle deeply nested expressions.
  • Simplifying the main CIF source file and avoiding errors of its compilation with GCC 12.
  • Adding new test cases and making the test framework more robust.

This release was done at the beginning of June.

Klever: Klever 3.6

Added by Evgeny Novikov about 2 months ago

Klever 3.6 was released pretty soon after Klever 3.5 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 Klever tutorial.

Other changes in Klever 3.6 are new models for struct_size() and underlying __ab_c_size() for the Linux kernel.

Klever: Klever 3.5

Added by Evgeny Novikov 3 months ago

We released Klever 3.5 that has following noticeable changes:

  • Improving support for verification of Linux 5.10 and Linux 5.17 (new specifications set "5.17" was added).
  • 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.
  • Using Ubuntu 20.04, Debian 11 and openSUSE 15.3 as preferable Linux distributions for deployment of Klever.
  • Switching to Python 3.10. You should carefully read this comment if you are going to update existing local instances of Klever.
  • Supporting regular expressions for assessing unsafes (you can see #11513 for more details).
  • Updating Klever Tutorial, in particular using verification of loadable kernel modules of Linux 5.5 as an example.
  • Updating add-ons and verification back-ends (various bug fixes and optimizations).
  • More advanced authorization of new users. Now the administrator should activate new users while somebody should grant them access to some jobs.

Many thanks to everybody involved!

Local Support Project: Redmine 5.0.0

Added by Alexey Demakov 4 months ago

Уважаемые коллеги!

Redmine обновился до версии 5.0.0.

Просьба сообщать об обнаруженных проблемах.

Klever: Klever 3.4

Added by Evgeny Novikov 6 months ago

Klever 3.4 includes the following prominent features:

  • Several improvements contributing development and generation of environment models:
    • Ability to specify savepoints for the main process.
    • Ability to select scenarios for particular savepoints manually.
    • Ability to configure the number of iterations for invocation of callbacks.
    • Providing users with a graphical representation of environment models directly in the Klever web UI.
  • Models for kmem_cache functions for the Linux kernel.
  • Updating add-ons and verification back-ends (various bug fixes and optimizations).
  • New sections in the user documentation: Configuring Program Decomposition and Development of Verifier Profiles.
  • Besides, you can find the CIF’s user documentation that may be helpful at development of advanced specifications and models.
  • Many fixes and minor improvements that make the specification development and verification workflow more easy, correct and reliable.

We highly appreciate efforts of developers and the feedback from users who made this release possible!

Local Support Project: Redmine 4.2.3

Added by Alexey Demakov 7 months ago

Уважаемые коллеги!

Redmine обновился до версии 4.2.3.

Просьба сообщать об обнаруженных проблемах.

Klever: Klever top contributor Ilja Zakharov started a new job

Added by Evgeny Novikov 8 months ago

Ilja Zakharov 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 scientific researches. We appreciate his work very much.

Recently Ilja Zakharov became a Verification Engineer at the Runtime Verification 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.


Also available in: Atom