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 |
Former Researcher in Prog. Lang. and Distr. Systems, CEO at Origin Labs, CTO at OCamlPro |
4aca372ed9695ab42cc8ba7fd7f56d11c2401611c2d513bbc28beb5c7f4363a1 |
|
Sergey EGOROV |
Software manager/director with ~20 years of experience, Cofounder of Pruvendo |
67dd20b9a760ae538a7f24ebfbaaf09a7075b4617a7ad09c19503c2551f57d81 |
|
Thomas SIBUT-PINOTE |
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 |
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 |
Entrepreneur. Mathematician, Coq-programmer with 10+ years of experience. Co-founder of Pruvendo and consensusresearch.org. |
cec27f6cfdadadc5da135875d5988019bd8a760fe6e16fe1f49459cf6d18f9e7 |
|
Sergey |
Programmer 30+ years of experience |
2c0ec55a109eb466d9db5ee7c3adb075e77627ade83ae17cea847671ab8f0a85 |
|
Nickolay |
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
- 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.
- On the basis of the semi-formalized specification, a business-level specification is created so that:
- It is written in a natural language
- It contains a set of common-sense logical statements
- It is accompanied by diagrams and flowcharts
- It includes role-action matrices (optional)
- It includes a table of possible attacks and malfunctions prioritized by severity
- The business-level specification shall be reviewed and approved in due course by smart contract developers and architects.
Phase 2
- 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:
- First-Order Logic
- Temporal logic of different kinds
- Separation Logic
- TLA+ family languages
- Reachability Logic
- Event-B
- …
If need be, the source code can be translated to an embedded domain-specific language (eDSL).
- Using the formal specification, the functional verification is performed in one of the following ways:
- Semi-mechanical deductive reasoning (Coq, Agda, etc)
- Automated theorem provers (Vampire, etc)
- SAT/SMT solvers (Z3, AltErgo)
- Symbolic/Explicit Model-Checkers
- After review against the source code, the outcome is the code verified by a trusted proof checker so that:
- It proves the specification
- It is verifiable by an external trusted proof checker (e.g. Coq, Agda, Isabelle, Idris, K, whyML, Z3, AltErgo)
- The list of externally required specifications is kept separately for the sake of quick checkups
- The internal specifications and proofs are provided and fully pass the build chain
- All axioms (not proved assumptions) are kept in a separate file
Phase 3
- On the basis of the source code, the formal specification and functional proofs, the following artifacts are created:
- Scenario specifications
- Proofs of functional correctness
- The following verification is performed:
- Scenario-level verification
- Gas consumption verification
- Safety verification
- Liveness verification
- 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:
- TVM bytecode is translated to an eDSL allowing for formal verification if needed
- Mapping between high-level state and TVM-level stated must be described
- The eDSL code is run
- The resulting state is translated to a form comparable with the initial state
- 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:
- https://forum.everscale.network/t/free-ton-web-design-jury-selection-contest-1-0/4511
- https://forum.everscale.network/t/contest-global-community-subgov-jury-selection/6914
- https://blog.freeton.org/en/analytics-support-jury-selection-contest-results/
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
to