DEX Phase 1 Formal Verification Proposal

Contest Proposal: Radiance-DEX Smart Contract System Phase 1 Formal Verification

Short Description

The contestants shall provide the Phase 1 of formal verification of the central Radiance-DEX smart contracts (DEXClient, DEXConnector, DEXPair, DEXRoot RootTokenContract, TONTokenWallet), hereinafter referred to as “smart contracts”, where the detailed description of the “informal audit” is described below. All debot contracts are excluded from the present contest. Other winning implementations of DEX are subject to similar contests when the corresponding implementations are ready.

Motivation

The contest shall yield a set of specifications necessary for the security audit and formal verification of the smart contracts. These shall include a function-level specification in a formalized version of English, a business-level specification, a description of user scenarios, and an evaluation of smart contract security and reliability threats (further details as to the specific content of said specifications are provided under Contest Terms). All these activities are critical as the preliminary steps for getting (at the latter phases) the formal specification and, eventually, the formal verification of the smart contract.

Location

The Radiance-DEX version of smart contract implementation to be worked with is located here:

  • https://github.com/radianceteam/dex3
  • Please note that the provided location is restricted so each participant is expected to explicitly send a request to the developers regarding the access using Telegram: Join Group Chat and any other means of communication. The developers, in their turn, are expected to grant the viewing permissions without delays
  • The versions available in the branch main/master by the midnight (UTC) of the contest starting date should be taken into account.
  • Throughout the contest the participants are encouraged to apply all the fixes committed not later than one week before the end of the contest

Prerequisites

Before entering the formal verification process, each smart contract must comply with the following rules (otherwise, the contest may be frozen by the request of any participant with the corresponding end date shifting until these requirements are met):

  • The smart contract must be compilable with the latest version of the Free TON development toolchain
  • All smart contracts must be submitted with detailed documentation. In particular, each public function (or all of its interfaces) of a smart-contract must be commented thoroughly: input arguments, expected output. The project must contain a detailed README file with deployment instructions, together with general business logic description.
  • All the smart contracts being audited must be covered by, al least, integration tests
  • No test coverage requirement are set for the moment

Also the contract developer is expected to:

  • Create or enter the Telegram group where all the issues can be rapidly discussed
  • Setup at least a weekly one-hour meeting with all the contest participants or have a private/public channel for these purposes
  • Grant an access to the repository to each participant in the timely manner

Contest Terms

The contestant shall submit a document in the PDF format that will include the following for each implementation of the smart contract mentioned in the “Location” section:

  1. General

  2. A general description of the smart contracts to be verified, accompanied by a chart

  3. A list of roles and responsibilities that can be identified for the smart contracts of the system

  4. A description of the semi-formalized variant of English that the contestant intends to use for smart contract specification

  5. A description of the preformal audit of the smart contracts

  6. Smart contract specification

(Note: there shall be a subsection for each of the smart contracts in the system; the structure of all such subsections is outlined below)

  1. A description of the smart contract state, including state components and their description.

  2. A function-level specification in the above-mentioned semi-formalized variant of English that shall describe, for each function:

  3. Access requirements

  4. Input parameters

  5. Output parameters

  6. Exceptions

  7. A business-level specification that shall:

  8. Be written in plain English

  9. Contain a set of common-sense logical statements

  10. Be accompanied by diagrams and flowcharts

  11. Include role-action matrices

  12. User Scenarios

This part shall contain the description of the user scenarios identified for the smart

contract system

  1. Security and Reliability Evaluation

This section shall contain a list of identified security and reliability threats. For each list item, the threat’s severity evaluation and the ways of mitigating it shall be described.

  1. Contestant Information

This section shall contain the information about the contestant. The contact information

(preferably a Telegram ID) and a short overview of the contestant’s background and

experience with blockchain, security, and formal verification are obligatory. Otherwise, the contestant is free to include any further information as they see fit.

Contest Dates

14 Sep 2021 - 01 Oct 2021

Proposed Prices

The total contest budget is 100 kTON, whereby 95% are allocated to the contestant awards and 5% are allocated to the jury reward.

The contestant awards are distributed as follows:

  • Place 1 - 50 kTON
  • Place 2 - 30 kTON
  • Place 3 - 15 kTON

The Jury

The Jury shall be formed from acknowledged experts in the fields of security, smart contract audit, and formal verification fields, whereby:

  • Jurors whose team(s) intend to provide submissions in this contest shall lose their right to vote in this contest
  • Each juror shall vote by rating each submission on a scale of 0 to 10 (0 equalling rejection of the proposal); a juror may abstain from voting if they do not see themselves sufficiently qualified to judge such proposal
  • A juror that has voted on a submission shall provide detailed feedback on it

Jury Guidelines

  • The main goal of the jury is to check how the provided specification is accurate and full.
  • The specification is intended to be understandable for an average IT professional but at the same time it must be evident it’s relatively easy to convert it to the formal one
  • All the requirements mentioned above are considered as mandatory otherwise some points have to be taken from the corresponding application.

Jury Rewards

The total budget for jury rewards is 5% of the above-mentioned contest reward budget (5 kTON).

This amount shall be distributed between jurors who have voted and provided feedback on submissions.

The proportion of the total budget assigned to a juror shall be defined according to the extent of this juror’s participation in the contest, i.e. the count of votes cast by this juror divided by the total votes cast count for this contest.

Procedural Limitations

  • Only one submission per contestant shall be accepted. Multiple submissions, including but not limited to updated versions of the initial submission, are not allowed.
  • Submissions shall be made within the time frame defined above in the Contest Dates section. Late submissions shall be rejected by the Jury.
  • All submissions shall contain the contestant’s contact information (preferably a Telegram ID) to ensure that the jury can match the submission to the specific contestant. If such contact information is missing, the submission shall be rejected.
  • If the submission contains links to external material (reports on further work by the contestant), this material shall have the contestant’s contact details (preferably a Telegram ID), to ensure that the jury can match the material to the specific contestant. If such contact information is missing, the submission shall be rejected.

Disclaimer

Anyone can participate, but Free TON cannot distribute tokens to US citizens or US entities.