DEX Phase 1 Formal Verification Proposal

Contest Proposal: DEX Smart Contract System Phase 1 Formal Verification

Short Description

The contestants shall perform the Phase 1 formal verification of the central DEX smart contracts (Price, Stock, TradingPair, FlexClient, RootTokenContract, TONTokenWallet), hereinafter referred to as “smart contracts”, including the preformal audit of the same contracts. All debot contracts are excluded from the present contest.

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.

As a supplementary step to the development of the above-mentioned specifications, it is hereby proposed that the contestants also undertake a preformal audit of the smart contracts. The rationale of the preformal audit is to reduce the workload at the stage of formal verification proper (since such audit can help identify and remove bugs that would otherwise surface only in the course of the formal verification, necessitating major rework) and to speed up the release of the smart contracts to Free TON, pending complete formal verification.

Caveat: Given the risks associated with possibly overlooked vulnerabilities, the release of smart contracts for which the full formal verification has not been completed should be undertaken exclusively in case of a strong business need.

Location

The all three versions of smart contract to be preformally audited are located here:

Prerequisites

Before entering the preformal audit 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
  • The smart contract’s developers must set up a Telegram group for discussions as well as a slot for one-hour voice calls at least once a week
  • All the smart contracts being audited must be covered by unit and integration tests
  • For the unit tests, the coverage must be measured (by any kind of coverage tool) and provide an evidence to the numbers not lower than:
    • Public function (all the functions but private) coverage - 100%
    • Private function coverage - 95%, all the functions having more than 5 lines of code must be covered
    • Line coverage - at least 80%
    • All the tests must pass
  • For the rest of the tests, all the tests must pass

The contestants shall use all information obtainable from the smart contract system developers (including, but not limited to, specifications, interviews with developers, and (prototype) source code).

Contest Terms

The contestant shall submit a document in the PDF format that will include the following:

  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. Preformal Audit Report

Preformal Audit must be conducted for three implementations of Flex - the winner of the corresponding contest and two immediate runners-up. The links to the implementations are provided in the corresponding section of the present document.

This section, supplementing the above-mentioned specifications, shall include the results of the preformal audit of the smart contracts undertaken by the contestant, complete with a list of identified bugs and/or vulnerabilities discovered in the course of such audit. In particular, this section shall contain the following information:

  1. A high-level description of the contestant’s approach to preformal audit

  2. A description of the toolkit(s) the contestant intends to use for preformal audit purposes (if any), including their motivation to do so

  3. A list of the checkpoints the contestant will make before commencing preformal audit both for functional and application level where application level checklist must include:

  4. Correctness checklist (correct state always moves to correct)

  5. Liveliness checklist (no stall in any conditions)

  6. Safety checklist (any foreseeable attacks are checked)

  7. A list of potential holes the contestant plans to leave opened accomplished with the solutions intended to reduce the risk of malfunction

  8. Results of the applying checklists and well as the tools (if any)

  9. Result summary

  10. 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

23 April 2021 - 28 May 2021

Proposed Prices

The total contest budget is 300 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 - 150 kTON
  • Place 2 - 90 kTON
  • Place 3 - 45 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 audit is useful in terms of decreasing the bug risk for the contract being audited
  • All the requirements mentioned above are considered as mandatory otherwise some points have to be taken from the corresponding application
  • The usage of industry-adopted 3rd party tools should bring additional points in case the motivation of their usage has been clearly demonstrated
  • Any team that managed to find a non-minor bug must be placed higher than a team that failed to do it
  • Any bugs related to the kind of the exceptions as well those related to the logging or retrieving the state are considered as minor and should not be taken into account for the ranking

Jury Rewards

The total budget for jury rewards is 5% of the above-mentioned contest reward budget (15 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.

2 Likes

I would recommend waiting until the second stage of the DeX contest is finished in the DeFi group.
There is no sense to check current contracts, IMHO.

3 Likes

I also think that current contracts are subject to change.

And I think a verification of only selected DEXes is very strange practice. I think we should not separate prize places from other prize places. Why 3 places? Why not 2 or 4? There was 5 places in DEX, so it should be 5 places to verify.
On the other hand, we can make less prize places in next DEX stage, so less prize places will be verified from DEX Stage 2. But we shouldn’t separate winners from winners. That’s ridiculous.

1 Like

Guys, unfortunately, Eva ate the apple and we are out the paradise. And being out the paradise the developers are never ready, they always have some tasks in backlog, so we never can start our verification. But community wants us to start. So, in our experience, it’s a good idea to start with “almost finished” contracts being ready to slightly change our models and proofs in the middle of the verification. It’s a normal practice.

1 Like

It’s a TopGov requirement to analyze three winners. For me I’d analyze the top winner only and hope that in future we’ll switch to that practice if we manage to convince all the stakeholders. But for now there are three, and I’m quite unhappy with.

1 Like

We are about to run Phase 1 consest just for Flex. The full conditions are below:

Contest Proposal: Flex Smart Contract System Phase 1 Formal Verification

Short Description

The contestants shall perform the Phase 1 formal verification of the central DEX smart contracts for the implementation known as Flex (Price, Stock, TradingPair, FlexClient, RootTokenContract, TONTokenWallet), hereinafter referred to as “smart contracts’’, including the preformal audit of the same contracts. 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.

As a supplementary step to the development of the above-mentioned specifications, it is hereby proposed that the contestants also undertake a preformal audit of the smart contracts. The rationale of the preformal audit is to reduce the workload at the stage of formal verification proper (since such audit can help identify and remove bugs that would otherwise surface only in the course of the formal verification, necessitating major rework) and to speed up the release of the smart contracts to Free TON, pending complete formal verification.

Caveat: Given the risks associated with possibly overlooked vulnerabilities, the release of smart contracts for which the full formal verification has not been completed should be undertaken exclusively in case of a strong business need.

Location

The Flex version of smart contract implementation to be worked with is located here:

  • https://github.com/tonlabs/flex
    The versions available in the branch main/master by the midnight (UTC) of the contest starting date should be taken into account.

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

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. Preformal Audit Report

Preformal Audit must be conducted for the Flex implementation of Dex - one of the contest winners. The corresponding contests for other winners will start when the corresponding projects are ready for Phase 1. The links to the implementations are provided in the corresponding section of the present document.

This section, supplementing the above-mentioned specifications, shall include the results of the preformal audit of the smart contracts undertaken by the contestant, complete with a list of identified bugs and/or vulnerabilities discovered in the course of such audit. In particular, this section shall contain the following information:

  1. A high-level description of the contestant’s approach to preformal audit

  2. A description of the toolkit(s) the contestant intends to use for preformal audit purposes (if any), including their motivation to do so

  3. A list of the checkpoints the contestant will make before commencing preformal audit both for functional and application level where application level checklist must include:

  4. Correctness checklist (correct state always moves to correct)

  5. Liveliness checklist (no stall in any conditions)

  6. Safety checklist (any foreseeable attacks are checked)

  7. A list of potential holes the contestant plans to leave opened accomplished with the solutions intended to reduce the risk of malfunction

  8. Results of the applying checklists and well as the tools (if any)

  9. Result summary

  10. 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

24 May 2021 - 14 Jun 2021

Proposed Prices

The total contest budget is 150 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 - 75 kTON
  • Place 2 - 45 kTON
  • Place 3 - 22.5 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 audit is useful in terms of decreasing the bug risk for the contract being audited
  • All the requirements mentioned above are considered as mandatory otherwise some points have to be taken from the corresponding application
  • The usage of industry-adopted 3rd party tools should bring additional points in case the motivation of their usage has been clearly demonstrated
  • Any team that managed to find a non-minor bug must be placed higher than a team that failed to do it
  • Any bugs related to the kind of the exceptions as well those related to the logging or retrieving the state are considered as minor and should not be taken into account for the ranking

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.

It’s a TopGov requirement to analyze three winners.

But for now there are three, and I’m quite unhappy with.

We are about to run Phase 1 consest just for Flex

In my imagination it looks like this:

- TONLabs Guy: Hey! You should verify DEX project by TON Labs
- FM SG: But it’s not a winning submission!
- TONLabs Guy: OK, verify 3 top subs, so there will be Flex by TON Labs.
- FM SG: But there is too much code to check…
- TONLabs Guy: No problems, just verify only DEX by TON Labs

Are you Free TON Sub-Governance or TON Labs Sub-Governance at all?

P.S. Of course, I’m strongly against this “contest”. It’s an obvious fraud and abusing of community resources. You should verify https://swap.tonswap.com that took 1st place or all 5 prize places or not run this at all.

4 Likes

Agree, my message was misleading. We still plan to go with the three but splitting the contest into two as nobody but Flex is ready and we don’t want to slow down.

Number three still looks like a right balance between amount or paticipants and required workload.

1 Like

Contest Proposal: Flex Smart Contract System Phase 1 Formal Verification

Short Description

The contestants shall perform the Phase 1 formal verification of the central DEX smart contracts for the implementation known as Flex (Price, Stock, TradingPair, FlexClient, RootTokenContract, TONTokenWallet), hereinafter referred to as “smart contracts’’, including the preformal audit of the same contracts. 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.

As a supplementary step to the development of the above-mentioned specifications, it is hereby proposed that the contestants also undertake a preformal audit of the smart contracts. The rationale of the preformal audit is to reduce the workload at the stage of formal verification proper (since such audit can help identify and remove bugs that would otherwise surface only in the course of the formal verification, necessitating major rework) and to speed up the release of the smart contracts to Free TON, pending complete formal verification.

Caveat: Given the risks associated with possibly overlooked vulnerabilities, the release of smart contracts for which the full formal verification has not been completed should be undertaken exclusively in case of a strong business need.

Location

The Flex version of smart contract implementation to be worked with is located here:

  • https://github.com/tonlabs/flex
    The versions available in the branch main/master by the midnight (UTC) of the contest starting date should be taken into account.

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

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. Preformal Audit Report

Preformal Audit must be conducted for the Flex implementation of Dex - one of the contest winners. The corresponding contests for other winners will start when the corresponding projects are ready for Phase 1. The links to the implementations are provided in the corresponding section of the present document.

This section, supplementing the above-mentioned specifications, shall include the results of the preformal audit of the smart contracts undertaken by the contestant, complete with a list of identified bugs and/or vulnerabilities discovered in the course of such audit. In particular, this section shall contain the following information:

  1. A high-level description of the contestant’s approach to preformal audit

  2. A description of the toolkit(s) the contestant intends to use for preformal audit purposes (if any), including their motivation to do so

  3. A list of the checkpoints the contestant will make before commencing preformal audit both for functional and application level where application level checklist must include:

  4. Correctness checklist (correct state always moves to correct)

  5. Liveliness checklist (no stall in any conditions)

  6. Safety checklist (any foreseeable attacks are checked)

  7. A list of potential holes the contestant plans to leave opened accomplished with the solutions intended to reduce the risk of malfunction

  8. Results of the applying checklists and well as the tools (if any)

  9. Result summary

  10. 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

27 May 2021 - 24 Jun 2021

Proposed Prices

The total contest budget is 150 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 - 75 kTON
  • Place 2 - 45 kTON
  • Place 3 - 22.5 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 audit is useful in terms of decreasing the bug risk for the contract being audited
  • All the requirements mentioned above are considered as mandatory otherwise some points have to be taken from the corresponding application
  • The usage of industry-adopted 3rd party tools should bring additional points in case the motivation of their usage has been clearly demonstrated
  • Any team that managed to find a non-minor bug must be placed higher than a team that failed to do it
  • Any bugs related to the kind of the exceptions as well those related to the logging or retrieving the state are considered as minor and should not be taken into account for the ranking

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.

Hi!

Infotecs/FF team is going to submit their specification very soon.

Stay tuned!

Hi everybody,

Pruvendo is sending its specification in a few minutes.

Contest redeploy proposal

  1. It’s suggested to redeploy Free TON Community extending the list of jurors by the following persons:
Denis EFREMOV Telegram Works as a developer at Oracle (Ksplice team). Previously worked as a formal verification engineer at ISPRAS (Frama-C/Event-B) and also has some experience with Solidity (mainly hackatons). 1c9c683858e623bb469787f5b3adcfc4aaa030d0cf5f8517cb67ad4a226621ad 0:a6002af20f1c23e6916f9696a6d91d34989ab450e722cb649090e938afbca174 Oracle
Ilya SHCHEPETKOV Telegram Researcher at ISP RAS, and I have participated in multiple formal verification projects since 2014. These include working with security and access control models for various operation systems: e.g. creating formal specifications and proving their correctness using the Event-B formal method and the Rodin platform. Also I took part in developing formal specification of a security framework for smart contracts using Isabelle/HOL theorem prover 67cab400f89fa8a49eb766a18f8fc15c1bcdfd6c4ca443667ca195e4dd0edce0 0:1460408fdeaf8a4dd6ee63513bab31202ac09fdafef825a0c98adb2080ea7c35 ISP RAS
  1. All the dates, submissions and other conditions must remain unchanged
1 Like

Another update:

Contest redeploy proposal

  1. It’s suggested to redeploy Free TON Community extending the list of jurors by the following persons:
Denis EFREMOV Telegram Works as a developer at Oracle (Ksplice team). Previously worked as a formal verification engineer at ISPRAS (Frama-C/Event-B) and also has some experience with Solidity (mainly hackatons). 1c9c683858e623bb469787f5b3adcfc4aaa030d0cf5f8517cb67ad4a226621ad 0:a6002af20f1c23e6916f9696a6d91d34989ab450e722cb649090e938afbca174 Oracle
Ilya SHCHEPETKOV Telegram Researcher at ISP RAS, and I have participated in multiple formal verification projects since 2014. These include working with security and access control models for various operation systems: e.g. creating formal specifications and proving their correctness using the Event-B formal method and the Rodin platform. Also I took part in developing formal specification of a security framework for smart contracts using Isabelle/HOL theorem prover 67cab400f89fa8a49eb766a18f8fc15c1bcdfd6c4ca443667ca195e4dd0edce0 0:1460408fdeaf8a4dd6ee63513bab31202ac09fdafef825a0c98adb2080ea7c35 ISP RAS
Anton TRUNOV Telegram Mathematically inclined embedded systems hacker who switched to formal methods

and interactive theorem proving more than half a decade ago. Want to live in a world

of provably correct distributed software systems.|38a67d804e03af93dcb3aab62b7cbe5acc4be5d8048558f3175973ce9d76e52a|0:8d08cafbb04b5690e93ce25ab8e0bb63bece459c1c05405682aaf62ee714d8e4|Ziliqa|
|||||||

  1. All the dates, submissions and other conditions must remain unchanged

Contest Proposal: Radiance-DEX Smart Contract Informal Audit

Short Description

The contestants shall provide the informal audit 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.

Motivation

Ideally speaking, all smart contracts issued by the Free TON ecosystem must pass the formal verification process. However, as the formal verification is an extremely time-consuming process, in some cases the business cannot wait for such a long time. Additionally, each bug found during the formal verification requires a major rework of the whole underlying stuff already completed.

To address both above-mentioned issues, we suggest to undertake the informal audit before proceeding to formal verification. Being capable to find most bugs, the completion of this kind of activity allows us to:

  • Release a smart contract with a high (but not the highest) level of reliability (this should be undertaken exclusively in a case of a strong business need)
  • Dramatically decrease the likelihood of finding a bug during the formal verification (taking into account that each bug found at the formal verification stage brings major overhead for the proving system)

Prerequisites

Before entering the informal audit process, each smart contract must comply with the following rules:

  • The smart contract must be compilable with the latest version of tondev tool
  • All smart contracts must be submitted with detailed documentation
  • The smart contract’s developers must set up a Telegram group for discussions as well as a slot for one-hour voice meetings at least once a week
  • All the smart contracts being audited must be covered by unit and integration tests
  • All the tests must pass

Location

All the source codes must be provided by the authors via Telegram: Join Group Chat Telegram group. The code to be audited has a hash 7d65f0d3b85e504ac33f01395b6ba0ffef9d5fe5 (branch main, link - Update README.md · radianceteam/dex2@7d65f0d · GitHub)

Contest Terms

Contestants shall submit a document in PDF format that covers:

● All the errors found

● All the warnings found

● All the “bad code” (long functions, violation of abstraction levels, poor readability etc.)

Foundings

Errors and warnings should be submitted to the developers as early as possible, during the

contest, so that the code can be fixed immediately.

The document should also contain a high-level description of the code, and any information

showing that the contest had a good understanding of the infrastructure and of the code.

Contest Dates

23 July 2021 - 06 Aug 2021

Proposed Prices

The total contest budget is 75 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 - 37.5 kTON
  • Place 2 - 22.5 kTON
  • Place 3 - 11.25 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 audit is useful in terms of decreasing the bug risk for the contract being audited
  • All the requirements mentioned above are considered as mandatory otherwise some points have to be taken from the corresponding application
  • The usage of industry-adopted 3rd party tools should bring additional points in case the motivation of their usage has been clearly demonstrated
  • Any team that managed to find a non-minor bug must be placed higher than a team that failed to do it
  • Any bugs related to the kind of the exceptions as well those related to the logging or retrieving the state are considered as minor and should not be taken into account for the ranking

Jury Rewards

The total budget for jury rewards is 5% of the above-mentioned contest reward budget, or

3.75 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.

OCamlPro is going to submit its audit of the code.
Telegram contact: @fabrice_dune

Pruvendo is about to submit its audit.
For any questions please contact me at @SergeyEgorovSPb

Contest Proposal: Flex Smart Contract System Phase 2 Formal Verification

Short Description

The contestants shall perform the Phase 2 formal verification of the central DEX smart contracts for the implementation known as Flex (Price, Flex, TradingPair, FlexClient, RootTokenContract, TONTokenWallet), hereinafter referred to as “smart contracts’. All the debot contracts are excluded from the present contest. Other winning implementations of DEX are subject to similar contests when the corresponding implementations pass Phase 0 and Phase 1 contests.

Motivation

Phase 2 (that can be roughly named as functional level verification) is a critical part of the overall verification process that validates the smart contracts at the functional level. The completion of the part is a prerequisite for Phase 3 that means the full verification at the high-level language level that is enough for correctness and reliability confidence for the most real-life applications.

Flex is one of the most important implementations of decentralized stock exchange that, in turn, one of the most critical parts of the overall Free TON infrastructure, the cost of any error is very high there and it’s clearly a sweet cake for all the malicious users, so, it’s definitely worth promoting to the Phase 2 without limiting the verification at lower informal levels.

Location

The Flex version of smart contract implementation to be worked with is located here:

  • https://github.com/tonlabs/flex
    The versions available in the branch main/master by the midnight (UTC) of the contest starting date should be taken into account.

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 contract must successfully pass Phase 1 level of verification
  • 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
  • Either accept (and respond to in a timely manner) a private Telegram chat created by each of participants

Contest Terms

The contestant shall submit a document in the PDF format describing all the activities overtaken as well as a link to GitHub where all code should be located. The materials provided must include:

  1. Concise description of a methodology used in the work.

  2. On the basis of functional specification conducted in Phase 1, a formal specification should be provided in a language that allows smart contract 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:

  3. First-Order Logic

  4. Temporal logic of different kinds

  5. Separation Logic

  6. TLA+ family languages

  7. Reachability Logic

  8. 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:

  2. Semi-mechanical deductive reasoning (Coq, Agda, etc)

  3. Automated theorem provers (Vampire, etc)

  4. SAT/SMT solvers (Z3, AltErgo)

  5. Symbolic/Explicit Model-Checkers

  6. After review against the source code, the outcome is the code verified by a trusted proof checker so that:

  7. It proves the specification

  8. It is verifiable by an external trusted proof checker (e.g. Coq, Agda, Isabelle, Idris, K, whyML, Z3, AltErgo)

  9. The list of externally required specifications is kept separately for the sake of quick checkups

  10. The internal specifications and proofs are provided and fully pass the build chain

  11. All axioms (not proved assumptions) are kept in a separate file

  12. List of defects found and submitted to the authors during the verification process. Defects should also be accompanied with their respective severity ranking.

  13. Short overview of the work results: what properties were proven, which properties are out of scope, how many defects were found, were they fixed or not, etc.

In addition to the materials mentioned above the following requirements must be met:

  1. The detailed instructions how to compile and run all the provided code must be written

  2. LICENSE file that describes the license for the published source code

  3. Upon the literal following the instructions the code must be compiled and run

  4. The PDF part of the document must be self-explaining, including all the links and briefs related to any activities outside of the present contest

  5. Contestant Information should be provided and include:

  6. The contact information (preferably a Telegram ID)

  7. A short overview of the contestant’s background

  8. Experience with blockchain, security, and formal verification

  9. The contestant is free to include any further information as they see fit.

Contest Dates

13 Sep 2021 - 13 Nov 2021

Proposed Prices

The total contest budget is 815 kTON, whereby 765 kTON are allocated to the contestant awards and 50 kTON are allocated to the jury reward.

The contestant awards are distributed as follows:

  • Place 1 - 350 kTON
  • Place 2 - 250 kTON
  • Place 3 - 165 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 contract is indeed verified at the functional level and corresponding risks are dramatically decreased
  • Non-functional level verification is out of the scope of the current contest and should be out of the consideration
  • Formal specification provided should follow Phase 1 specification of any of the awarded (top-3) participants
  • The following considerations should be taken into account during the judging:
    • How well the provided formal specifications are linked with business properties of a system. How traceable are they?
    • How adequate are assumptions being made in the statement definitions and/or within proofs.
    • The properties proved and their respective severity to the overall system reliability.
    • How reasonable/trustworthy is the used methodology appears.

Jury Rewards

The total budget for jury rewards is 50 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.

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 Flex version of smart contract implementation to be worked with is located here:

  • https://github.com/radianceteam/dex3
  • 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

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

13 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.

can’t open

image
also there is a typo

Thank you. Will fix the typo. The repository is restricted so to access it each participant is expected to explicitly request an access from the develpers. I’m going to add this requirement right now and to resubmit the proposal

1 Like