Klever Components Overview¶

Klever consists of the following components (at the moment they are not clearly reflected in the repository):

• Bridge
• Native Scheduler
• Cluster Scheduler
• VerifierCloud Scheduler
• Core
• Controller

Bridge¶

Bridge connects users and all other Klever components together by providing a web interface to a database. By using this interface users can prepare verification jobs of various classes (see below) and start their decision. Besides users can evaluate verification results by associating expert marks with corresponding reports (see below).

Native and Cluster Schedulers¶

Schedulers distribute verification jobs and verification tasks (see below) to be decided on workers in accordance with available/required resources, priorities and so on.

Both Native Scheduler and Cluster Scheduler have Job Worker and Task Worker as subcomponents. In case of Native Scheduler all instances of both workers are executed on the same computer as Native Scheduler. In case of Cluster Scheduler instances of workers can be executed on any computer of the cluster that has appropriate resources.

Job Worker decides a verification job with help of Core.

Task Worker decides a verification task with help of a specified static verifier.

Both Core and static verifiers are launched under BenchExec (at the moment for Core it is used RunExec that is a part of BenchExec) that counters and limits consumed resources and performs some common pre- and post-processing of input parameters and output results.

VerifierCloud Scheduler¶

VerifierCloud Scheduler decides verification tasks by means of VerifierCloud. It can not decide verification jobs.

Core¶

Core decides a verification job. During decision several verification tasks can be prepared. Besides Core and its subcomponents generate reports including:

• unknown reports describing reasons of failures
• unsafe reports describing potential bugs in software found by static verifiers
• safe reports meaning that static verifiers can prove correctness of software against checked properties under corresponding conditions
• other auxiliary reports to provide information when Core and its subcomponents start/finish execution, what resources they consumed and so on

Core uses appropriate subcomponents to decide verification jobs of corresponding classes. In case of Verification of Linux kernel modules they are:

• Linux Kernel Build Command Extractor (LKBCE) fetches Linux kernel source code and then configures and builds the Linux kernel intercepting appropriate build commands, e.g. CC and LD commands
• Linux Kernel Verification Object Generator (LKVOG) produces one or more verification objects that are trees of groups of source files with corresponding CC commands
• Abstract Verification Task Generator (AVTG) weaves each generated verification object with rule specifications in the static verifier independent manner
• Verification Task Generator (VTG) generates one or more verification tasks for a specified static verifier on the basis of each generated abstract verification task and performs post-processing of verification task decisions

LKVOG has the following strategies to generate verification objects (at the moment they are not represented as corresponding subcomponents):

• Separate Linux Kernel Module (SLKM) - each verification object corresponds to a single Linux kernel module and consists of a single group of corresponding module source files with CC commands

AVTG invokes plug-ins in the order and with special parameters specified by corresponding rule specifications. Each plug-in usually takes some specification(s) as input and can produces aspects or/and some data as output. Following plug-ins are available:

• Source Analyser (SA) queries verification object source files to get some useful knowledge, e.g. information on function calls and definitions, macro substitutions, type and variable declarations (at the moment this knowledge is used just by EMG)
• Environment Model Generator (EMG) generates environment models in form of aspects
• Argument Signature Extractor (ASE) queries verification object source files to get argument signatures represented as strings allowing distinguish various objects like mutexes and spin locks
• Template Renderer (TR) renders specified templates on the basis of specified contexts, e.g. argument signatures
• Rule Specification Generator (RGG) extends verification objects with rule model source files and add aspects binding them with verification object source files
• Weaver weaves all produced aspects into verification object source files

VTG has the following strategies to generate verification tasks:

• All Bug Kind Merge (ABKM) considers all bug kinds specified in rule model source files as one and thus produces one verification task per each abstract verification task

Controller¶

Controller performs various checks of available services and resources and notify concerned parties about this.