Free TON

Formal Methods Sub-Governance Proposal

ForMet SG proposal

Summary

We hereby propose the creation of a Formal Methods Subgovernance (ForMet SG) for Free TON.

Mission and Vision

The mission is to facilitate the improvement of the software used on the FreeTON network by using formal verification methods.

The vision is to make FreeTON more secure and robust, and thus to enhance the FreeTON ecosystem and expand the FreeTON community.

Rationale

The world of blockchain and crypto-currencies is a wonderful world for hackers looking for easy targets : smart contracts are small pieces of code managing huge amounts of crypto-currencies, and their automated behavior and immutability make them easy targets. The short history of blockchains is already full of stories of millions of USD stolen or lost in many smart contracts, starting from the DAO and ERC20 awful stories. Most of these contracts had been tested by developers (using frameworks like Truffle, etc.) and many of them were audited by “security experts”. Despite these efforts, there were still bugs to be exploited in them. This is due to the limited nature of such verification techniques.

On the other hand, formal methods provide much more bullet-proof verification techniques: they show that a smart contract code satisfies a formal specification, not for a few tested cases, but for all possible executions. This is a very strong property to get, that gives much more trust in the smart contracts than just testing or auditing. Yet, formal methods are limited by the expertise and skills required to deploy them on real life smart contracts.

The goal of this new sub-governance is to build a team of strong experts from various companies and to apply their expertise in formal methods to secure the Free TON ecosystem and its most important smart contracts.

Scope of Activities

The proposed sub governance shall perform the following activities:

  • Organization and running of formal verification contests
  • Distribution of funds to contest winners
  • Developing and improving the Free TON community guidelines on formal verification
  • Facilitating the development and application of open source tooling for formal verification purposes
  • Encouraging the creation of further formal verification teams

Formal verification is intended to be applied to the following software:

  • Smart contracts (especially those essential to the Free TON infrastructure)
  • TON compiler and other essential software
  • Other software related to the Free TON blockchain with critically important behaviour

Subgovernance Organization and Management

Membership

Initial Members

Name

Telegram

Background

Public Key

Fabrice LE FESSANT

Telegram

Former Researcher in Prog. Lang. and Distr. Systems, CEO at Origin Labs, CTO at OCamlPro

4aca372ed9695ab42cc8ba7fd7f56d11c2401611c2d513bbc28beb5c7f4363a1

Sergey EGOROV

Telegram

Software manager/director with ~20 years of experience, Cofounder of Pruvendo

67dd20b9a760ae538a7f24ebfbaaf09a7075b4617a7ad09c19503c2551f57d81

Thomas SIBUT-PINOTE

Telegram

PhD. in Formal Proof (https://www.theses.fr/2017SACLX086) using Coq. Engineer at OCamlPro/Origin Labs. Initial author of the Tezos Michelson formal proof framework in Coq and F*.

50384ec36bee19914526f436a0adf57d0c35389934b5aaca15db5b5e89f42aa0

Evgeniy SHISHKIN

Telegram

Researcher in the field of Formal Methods in Software. Pursuing PhD in Institute of Systems Programming (ISP RAS). Senior Researcher at InfoTeCS R&D (software security/reliability group). See my homepage.

6ff61c1a7bb09795f7b5d5514dd710efb72e9557654d362ef208fde545ba7a33

Andrey
LYASHIN

Telegram

Entrepreneur. Mathematician, Coq-programmer with 10+ years of experience. Co-founder of Pruvendo and consensusresearch.org.

cec27f6cfdadadc5da135875d5988019bd8a760fe6e16fe1f49459cf6d18f9e7

Sergey
TYURIN

Telegram

Programmer 30+ years of experience

2c0ec55a109eb466d9db5ee7c3adb075e77627ade83ae17cea847671ab8f0a85

Nickolay
VASILEV

Telegram

Formal Verification Engineer, 8+ years of experience in Coq

b722871cc121019663e982eaf24958b2ca9ffad4472d8d0a98110d5eb5082004

The initial members shall oversee the efforts related to building the SG. They will also act as jurors until the SG jury is assembled.

Member Admission

Membership is open to everyone with proven experience in the field of formal verification, provided that a simple majority of the SG members approves the prospective member.

Membership Termination / Dismissal

Membership in the SG can be terminated at any time by notifying all members of the SG in the Telegram group.

A member can be dismissed from the SG if ⅔ of SG members cast their votes for this.

Communication

The communication on the matters related to the activities of the SG shall happen through the following channels:

  • Website on gov.freeton.org (publication of contest proposals, information on membership etc).
  • Forum on gov.freeton.org
  • Telegram group (open membership)
  • Regular (weekly/biweekly) call

Formal Verification Workflow

We hereby propose a workflow for formal verification. It comprises four phases, and each of them can be the subject of a separate contest. It’s illustrated at the next page and discussed further later.

Phase 1

  1. On the basis of information obtained from smart contract developers and architects (interviews, specifications, and source code), a semi-formalized specification in a controlled natural language is created.
  2. On the basis of the semi-formalized specification, a business-level specification is created so that:
  1. It is written in a natural language
  2. It contains a set of common-sense logical statements
  3. It is accompanied by diagrams and flowcharts
  4. It includes role-action matrices (optional)
  5. It includes a table of possible attacks and malfunctions prioritized by severity
  1. The business-level specification shall be reviewed and approved in due course by smart contract developers and architects.

Phase 2

  1. On the basis of smart contract source code, a formal specification should be provided  in a language that allows smart verification to be formally described. This language can be either the own language of the verification tool (proof assistant, Prolog etc.) being used or be a specific formal logic language such as:
  1. First-Order Logic
  2. Temporal logic of different kinds
  3. Separation Logic
  4. TLA+ family languages
  5. Reachability Logic
  6. Event-B

If need be, the source code can be translated to an embedded domain-specific language (eDSL).

  1. Using the formal specification, the functional verification is performed in one of the following ways:
  1. Semi-mechanical deductive reasoning (Coq, Agda, etc)
  2. Automated theorem provers (Vampire, etc)
  3. SAT/SMT solvers (Z3, AltErgo)
  4. Symbolic/Explicit Model-Checkers
  1. After review against the source code, the outcome is the code verified by a trusted proof checker so that:
  1. It proves the specification
  2. It is verifiable by an external trusted proof checker (e.g. Coq, Agda, Isabelle, Idris, K, whyML, Z3, AltErgo)
  3. The list of externally required specifications is kept separately for the sake of quick checkups
  4. The internal specifications and proofs are provided and fully pass the build chain
  5. All axioms (not proved assumptions) are kept in a separate file

Phase 3

  1. On the basis of the source code, the formal specification and functional proofs, the following artifacts are created:
  1. Scenario specifications
  2. Proofs of functional correctness
  1. The following verification is performed:
  1. Scenario-level verification
  2. Gas consumption verification
  3. Safety verification
  4. Liveness verification
  5. Verification of other requirements from Phase 1

Phase 4 (optional)

The goal of Phase 4 is to verify that the TVM code generated for the particular contract works identically to the source code verified at the former stages. Thus, the compiler will be verified but for the particular contract only. The kind of verification can be achieved, for example, by the following workflow:

  1. TVM bytecode is translated to an eDSL allowing for formal verification if needed
  2. Mapping between high-level state and TVM-level stated must be described
  3. The eDSL code is run
  4. The resulting state is translated to a form comparable with the initial state
  5. The states are compared, and the TVM bytecode is proved identical to the source code

Formal Verification Contest Organization

The SG shall follow the established Free TON practices when organizing contests.

The Jury

Contests are managed by the elected Jury. At the inception stage of the SG, the Initial Members shall organize the Jury Selection Contest; before the Jury is elected, the Initial Members shall act as jurors.

Selection Criteria

The Jury is elected from members with proven expertise in formal verification. Further requirements shall be described separately in the proposal for the Jury selection contest.

Some samples of Jury selection contest proposals for reference:

Functions of the Jury

The Jury shall perform the following functions:

  • Ensuring the smooth operation of the SG
  • Developing and reviewing contest proposals (CPs)
  • Accepting and reviewing contest proposals
  • Assessing contest submissions from participants
  • Choosing contest winners
  • Distributing funds between contest winners

Term of office of the Jury

Jurors are elected indefinitely; if a juror leaves the Jury, a new by-election contest shall be held.

Remuneration to the Jury

The matter is covered in the following section. Further details shall be included in specific contest proposals.

Budget and Remuneration

The global budget 

The global budget of the ForMet SubGov for 2021 can be summarized as follows:

Contest

1st place total award

Details

Smart Contract Verification Contests

6.6 million TON

6 sets of smart contracts need to be verified (TIP-3, Elector, SMV, PBTG, Multisig v2, DePool 2)

Open Source Tooling Contest

1 million TON

Tooling to improve the quality of smart contracts in the ecosystem

TVM Verification Contests

500 kTON

2 contests: TVM formal definition and program logic for TVM bytecode

Bug Bounty Contest

500 kTON

Incentives for bug finders

TVM Audit Contest

300 kTON

Audit of the TVM Execution Engine in Rust prior to later formal verification

Specification contest

500 kTON

Contests for those parts of the system that are not planned to be formally verified in the near-term but still useful for the audit and other activities such as blockchain model, node model, consensus etc.

Bug Bounty

This is for the first place only, all the other distribution (second, third and other winning places) will be covered by the separate document as a function of the 1st place award and jury expected efforts. Normally jury bounty is 5% of the overall budget but for phases 2, 3 and 4 of Smart Contract Verification Contests it’s planned to raise it up to 20% as it requires extremely serious efforts.

Phase-by-phase breakdown (for Smart Contract Verification Contests)

It’s planned to keep the same 1st place awards as for the previous contests so:

Phase 1 : 50 kTON

Phase 2 : 350 kTON

Phase 3 : 350 kTON

Phase 4 (optional) : 350 kTON

9 Likes

total budget for this SG?

please include something like this, to get that easily processed

Request
We request main gov to send X :gem: to 0:123...123

Hi! Thanks for the proposal. I would like to clarify the following points.

If need be, the source code can be translated to an embedded domain-specific language (eDSL).

This translation step is critical from semantic preservance viewpoint: it must be kind of sound, otherwise you risk introducing or loosing some behaviors. How are you going to ensure the soundness of this translation? Are the translation rules going to be published and/or peer-reviewed before taken as the verification target? Or is it a part of a contest submission and jurors are to establish soundness on their own?

Summary table needed:

How many TONs? When? For what (KPI).

Thanks.

Hi all,

Thank you for your comments, we tried to integrate all of them. Unfortunately, the new version of the proposal is too big to fit into the forum message so just providing a link: ForMet SG proposal v3 - Google Docs

With Best Regards,
Sergey.

2 Likes