ProvenTools

ProvenTools is a complete software development toolchain designed to edit and prove computer programs written in Smart, Prove & Run’s modeling language. Smart is a text-based, strongly-typed functional language designed to be easily understood by software engineers proficient with C or Java.

Developing Proven Software with ProvenTools

Working with ProvenTools, software engineers follow a traditional software development process:

  • Starting from an informal specification of the behavior of the targeted software component, create the corresponding model written in Smart. This informal specification can be either a set of documents describing the expected behavior of the targeted software component or an existing codebase;
  • Identify the security properties that the targeted software component must fulfill and insert them in the Smart model;
  • Formally prove that the Smart model satisfies the security properties at all times using the interactive prover;
  • Generate working C or Java code from this model.

ProvenTools supports agile software development methodologies at every step of this process:

  • When a Smart model is modified to support a new functional or non-functional requirement, ProvenTools automatically detects if this modification invalidates the proofs;
  • Code generation is fully automated so any modifications to the Smart model are immediately reflected in the working code.

Creating and Editing Smart Models

ProvenTools provides software engineers working on Smart models with all the assistance they can expect from a modern IDE:

  • Code navigation;
  • Syntax highlighting;
  • Code completion;
  • Code transformations.

ProvenTools is based on Eclipse, ensuring that software engineers are immediately familiar with the tool.

Proving Smart Models

ProvenTools includes an interactive, intelligent prover, which automates simple proofs and assists users during more complex ones. ProvenTools’ prover has been designed to be as transparent as possible by explaining exactly how a proof is achieved and by providing a detailed context when a property cannot be proven. This is in stark opposition to traditional “black-box” provers that in many cases do not give detailed explanations about the results they provide. This property is especially important when a product has to be certified as an auditor needs to be able to verify the claims of the prover.

Generating Working Products from Smart Models

Smart is a modeling language that enables software engineers to fully define the behavior of their applications, down to the smallest details. However, embedded devices are only able to run applications written in C or Java, not in Smart. Therefore, ProvenTools includes a generator to transform programs modeled in Smart into their equivalents in other languages, while retaining the proof guarantees. In its standard configuration, ProvenTools can generate Java code as well as several kinds of C code. Since ProvenTools is based on a modular architecture, it can be extended to support another language.

The code generator has been built with the very specific requirements of embedded devices in mind. For example, it can generate code without memory allocations, which may be a requirement for embedded kernels.

Once generated, the C or Java source code can be compiled using traditional tools such as GCC or javac.

ProvenTools is available under flexible license terms. Please contact moc.n1513276716urnev1513276716orp@s1513276716elas1513276716 for more details.

Print Print