Home   >   Demonstrators   >   KINDSPEC

KINDSPEC

Demonstrator|vrain

Description
KindSpec automatically infers software contracts from C programs.
Member
Address
Camino de Vera S/N
Province
Valencia

DEMONSTRATOR INFORMATION

DESCRIPTION

KindSpec is a tool for automatic inference of software contracts from programs written in a meaningful fragment of the C language called KernelC. KernelC supports dynamic pointer-based data structures and stack manipulation. KindSpec takes as input a program and the user must specify which method (called modifier) he wants to infer the software contract for. Once specified, KindSpec automatically generates a contract using the observer methods (which have a return value) of the program itself. The inferred contract consists of logical axioms that express preconditions and postconditions that define the input/output behavior of the object method. By using the program's own methods as components of the assertions, they are easily understood by the developer. The inferred axioms can be used both for the documentation of the code and for the detection of shortcomings or errors in the system when the inferred assertions are not as expected. The tool can generate reports about the final software contract, statistics, and store the contract in a serialized object that can be used by other tools.

POSSIBILITIES

KindSpec's inference method relies on symbolic execution technique and abstract interpretation to prune the symbolic execution tree when we have infinite branches originating from loops and recursion. There are different configuration alternatives associated with this technology. We can set aliasing to be used in symbolic execution in order to capture properties of cyclic data structures. We can also select an abstract domain that allows more precise tree pruning than using a maximum depth. The use of abstractions allows to detect patterns in the loops that can give rise to axioms that represent a certain behaviour. Due to the abstraction, we will not be able to guarantee the correctness of some axioms, which are noted as candidates until they can be verified or discarded in the refinement process that can be executed after the inference. From the refinement section, the user can select the candidate axioms to be refined either through a falsification process (to discard them as incorrect) or through a verification process (so that they will become part of the contract). Associated with the verification process, a generalization and simplification of axioms is carried out, since it is possible that with the introduction of new axioms, more general axioms can be defined that subsume several axioms of the contract. In this case, the subsumed axioms are removed from the contract leaving only the general axiom. Thanks to this process we can obtain specifications that are more compact and easier to understand for the user.

TECHNOLOGICAL ENABLER

Artificial Intelligence and Computing
Data security and privacy technologies

Program verification, safety analysis, provable security. Protocol crypto-analysis. Automated analysis, modeling, verification, synthesis, learning, debugging and optimization of complex systems and models