What is program verification

Formal verification (FV) is a series of methods and technologies allowing to get much more reliable guarantees of software (or hardware) correctness than traditional approaches based on testing.

The correctness in this case is a correspondence of the behavior to the specification which should be given in a strict and formal way. Traditionally the outcome (main artifact) of the FV process is called the proof and in the deductive branch of the technology it is actually the strict mathematical proof of the software properties which is in turn to be verified by the special software named proof assistants.

Industrial approach suggests the full FV stack consists of

• informal audit
• informal business level specification
• formal engineer level specification
• verification (proof) of the given code against the formal specification.

There are a lot of possible ways to perform software verification, all they differ in feasible strictness, potential completeness and deal both with production code or simplified models (used for protocols verification for example). The most methods used in FV are based on contemporary scientific research in mathematics and computer science. The underlying theory is still at the scientific edge and under permanent development and have deep influence both on computer science and mathematics itself (I am going to show that in further posts).

There exists well popular common sense that FV can guarantee absolute correctness if successfully completed. That is only partially true.

The more strict proposition is that deductive FV methods guarantee absolute correctness with respect to the given specification. The quality of the specification itself and it's completeness and consistency are independent problems, and often the specification, good or not-so-good, is suggested to be given out of the box, however the FV methods can be applied to assess the specification properties as well. In comparison with testing where only finite subset of cases can be considered, FV deals also with infinite number of cases literally proving the properties for all allowed values of variable parameters of the system. Another important feature of the deductive FV is that it is inheritable: the properties have not to be reverified when embedding the proven subsystem into a bigger one, all statements hold until one changes the code or specification.

The proof itself has not to be analyzed or manually read - the task to verify the proofs is on duty of special very sophisticated software. The consumers of FV results might assess only the specification: if it is good enough and proofs are verified by external proof assistants, the job is well done, and the verified software is assumed to be correct.

Methods we use in Pruvendo

(I am a cofounder of Pruvendo company which specifies on smart contract verification, so I put it here, though this blog is my personal, and I am not going to advertise anything here)

We basically work on the deductive branch of the formal verification technology. We use Coq proof assistant to state the properties and verify proofs. To cover the full stack of the verification process we divide it in the following steps.

On the first stage we make an informal audit of the contracts. This allows to realize the program architecture and dependencies, construct the call graph of contracts methods, find the potential security holes and prepare ourselves to the specification creation step. During this phase we actively communicate with developers and project managers to fully understand the system purpose and environment where it should be run at production phase. It happens that after this stage we offer the developers to make some workarounds to mitigate the revealed issues and to correct architectural limitations if any.

The second stage deeply connected with the first one and here we summarize the audit results to the informal specification - that is free but technical description of what system does, which high level properties it should have, and describe the main user scenarios of exploitation. One can think of scenarios as the user guide where we state how the user should act to get the estimated results or particular process flow. This high level document we also use to reconcile with developers to be assured that we are on the same wave.

After that our more technical work begins. To perform the verification process we need to represent both specification and code in a way which could be understood by the Coq proof assistant. And we developed our Coq embedded language we call Ursus to perform that task. Ursus toolkit allows to translate the original solidity code to the form which is very syntactically close but in the same time consists of correct Coq terms. Having both artifacts - specification and code in Ursus language we can perform further steps. To simplify the transition between informal specification and formal propositions in Coq we are developing intermediate language (without final name) which is strict enough but more human readable in comparison with Coq native language for predicates statements.

The lot of work as you see have to be done before we start proving the properties. Actually the process of deductive verification is still time consuming so we make yet another step before it. We run sophisticated randomized tests after the completion of Ursus translation. That is taking the propositions formulated on the previous steps inside Coq ecosystem we use special methods to run property-based checker which apply brute forcing algorithms to find the counter examples. After that when most of the issues are gone we use the deductive verification schemes to mathematically prove the correctness of the properties revealed. The good news here are that we do not need to reformulate the properties we used for randomized checking. So we just use two different techniques to verify the common set of contract's properties.

After the completion of all steps we may think that contract behavior is correct against the formulated specification which is in turn tightly connected with what developers and task managers see and estimate from the software under investigation.

All the phases we supply with comprehensive reports and verification code such that every consumer can check the proofs by herself and match the properties with her view.

(As I wrote before that is not advertising but this text allows me to explain something later without returning to the whole process)

Types of verification directions

Unit properties (functionality)

Direct scenarios (liveness?)

Inverse scenarios (security)

Functional (and declarative) and imperative programs

Do we really need our programs to be verified

What is next

some stuff happened