Table des Contenus

Audit and Verification Services

Audit and Formal Verification Services⚓

OCamlPro has a long tradition of working at the edge between programming and formal verification. Formal verification is used to model programs using mathematical formulas, that can be proved to verify properties on these programs.

OCamlPro has great expertise in formal verification:

  • Several members of the team have a PhD in Computer Sciences in the field of program verification;

  • OCamlPro maintains Alt-Ergo, an automatic theorem prover used in program verification to prove the formulas extracted from the program formalisation;

  • OCamlPro is an active member of the FreeTON/EverScale Formal Verification Sub-Governance, in charge of auditing, specifying and verifying Solidity Smart Contracts;

Code Audit⚓

Auditing code is the first stage of formal verification.

It usually implies:

  • Writing a pre-formal specification of the code, describing the overall behavior of the program, and, for each component or function, their individual behaviour;

  • Careful reading of the code to check for semantic bugs and flaws in the architecture. Formal verification should not be done until such initial flaws have been fixed;

  • Using simple tooling to analyze the code, finding simple bugs, and checking compliance with best practices;

In the past, we have audited several sets of smart contracts in Solidity, winning the first price several times in EverScale contests. We also developed a decompiler between Michelson and Liquidity, two smart contract languages of Tezos, to ease auditing Michelson smart contracts.

Formal Verification⚓

Formal verification is to verify mathematically that a program code implements its formal specification. Formal verification is a complex task, and may take a lot of time, depending on the size of the program, and the availability of a formalization of the language and runtime in which the program is written.

Smart contracts are a good target for formal verification, as they are usually rather small in comparison with computer programs, and written in a simple language with a small set of well-defined operations.

We usually use two verification technologies:

  • The Coq proof assistant, that can be used to prove models, or to generate running code from proofs;

  • The Why3 Platform for deductive verification, that can be used to prove properties on code sources, using a wide range of automatic theorem provers;

In the past, we have written a formalization of the EverScale Smart Contract Virtual Machine that we are using to verify smart contracts written in Solidity on this blockchain.

Common Criteria Certification⚓

Common Criteria is a set of international standards to evaluate the security of computer systems and softwares. ANSSI, the French National Agency for Security of Software Systems, is well-known as one of the most demanding agencies to evaluate Common Criteria Certification.

At levels EAL6+, Common Criteria Certification requires formal verification of the security policy model.

We are currently involved in the EAL6 Certification of a smart card system, using the Coq proof assistant to verify the SPM, Boot Loader and Authentication.