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:

• More than half of our teams hold a PhD in Computer Sciences in the field of formal method and program verification;

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

• OCamlPro helped Samsung obtain EAL6+ Certificates from ANSSI, using the Coq proof assistant (read more);

• OCamlPro was 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;

Use-Case:

In 2021, we audited several sets of smart contracts in Solidity, winning the first price several times in contests organized by the EverScale Network. We also developed a decompiler between Michelson and Liquidity, two smart contract languages for the Tezos blockchain, 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;

Use-Case:

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

Common Criteria⚓

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 able to provide the certification work for companies needing EAL6+ certificates.

Use-Case:

In 2022, we codeveloped the certification proofs with Samsung of several of their smart card systems, using the Coq proof assistant to verify the SPM, Boot Loader and Authentication. The proofs have been audited by the CEA Leti cesti, and certificates have been delivered by ANSSI.