Free TON

DePool Contract Verification (Phase 2) [26 October 2020 — 26 November 2020]

Thank you! Fixed)) Now it’s correct!

Hello! Please tell me where on the website https://gov.freeton.org I can find this contest?

Hi! You can see it here https://easy-vote.rsquad.io

Unfortunately, it is not there either. There is only “DePool Contract Verification (Phase 1)”. Please give a link to the active contest for Phase 2.

1 Like

Look here https://gov.freeton.org/proposal?proposalAddress=0:9ed644435eebf731844e99cea186430159b08d43aea4d79f27e4a7871fbde698

You have fixed it on the forum instead of PDF and now we have wrong contest dates.

DePool smartcontract addresses one of the most important problems within FreeTON blockchain ecosystem: lowering the bar for those who would like to participate in validation process, let ordinary users make profit on it and increase decentralization of the platform.
It is obvious that errors in such mechanism can lead to tremendous money loss, and, therefore, an extra effort must be made to ensure its functional correctness. Free TON Foundation together with InfoTeCS have started the process of DePool formal verification. The verification team led by Evgeniy Shishkin have created the formal specification you can now examine.
Unfortunately, due to complexity of the smartcontract, this effort requires much more time than the time period stated in the Contest. We view our participation as a starting point in collaboration on formal verification of DePool and other important contracts.
You can ask questions regarding the document and other related things on Forum or using our Contacts:
Evgeny Shishkin - evgeny.shishkin@infotecs.ru
Sergey Tyurin - @Custler (Telegram)
Pavel Rozanov -@pasha_rozanov (Telegram)
Free TON Foundation is a tool for engaging new users and developers into Free TON community. Please check the link for details:
Free TON Foundation

Submission #5 :

11 Likes

Hi everybody,

Pruvendo team is about to submit Depool Phase-2 formal verification report. While the first phase was about text, the second one is mostly about code. In a few minutes we’share with a report that has an explanation what was done as well as a link to a few GitHub repositories that contain code and proofs for the Phase-2. It’s not a finalized work, we’ll continue with Phase-3 to finish formal verification of the DePool contract.

If you have any questions feel free to contact @SergeyEgorovSPb or @andruiman at Telegram or just drop a message at this forum.

With Best Regards,
Pruvendo Team.

5 Likes

Hi everyone!

My name is Evgeniy Shishkin, I am a scientific researcher from the
field of software formal verification [1], participated in
writing the FreeTON Foundation/Infotecs DePool formal specification report.

I would like to express some thoughts regarding what is being done in
the direction of DePool formal verification, as well as other TON
smart-contracts.

First thing to notice, is that currently there are 2 teams doing this
work: FreeTON Foundation/InfoTecs, and Provendo.

One might think that there are two competing companies, and the one
that made the best job has to gain rewards.

In my view, this point is totally wrong. And here is why:

  1. Both companies do the work on formal verification, but do it in
    completely different directions.

    Provendo do deductive formal verification in the Interactive Proof
    Assistant tool (Coq). Very precise and trustworthy, this approach
    has its practical limitations regarding the kind of properties that
    can be verified in a feasible amount of time. For example, most of
    SAFETY properties from our submission will be very hard to prove
    using deductive approach due to complexity of the logical apparatus
    needed (LTL temporal logic proofs are very hard to build). On the
    other hand, Hoare-style proofs has to be made this way.

    FreeTON Foundation/InfoTecs has very different approach, and it is
    called symbolic model-checking. The whole system gets simplified
    into something that can be efficiently automatically proved correct
    but with the given upper bound on many options, like: transactions
    count, number of users, number of stakes etc. More scalable and
    flexible, this approach has its own limitations, but permits to
    check some critical business-level scenarios.

    Both approaches can and should benefit each other, because they
    address kind of different attack vectors. This point is heavily
    underappreciated.

  2. Both companies do the work in the direction of improving the
    quality of FreeTON smart-contract ecosystem.

    Everyone in this community will benefit from having more than “one”
    pair of eyes looking at the code and verification scripts.

    I feel like the community should encourage partnerships, not
    competition-like cannibalism, at least in the field of system
    security/reliability

And please keep in mind the Sad Story of Ethereum TheDAO
smart-contract that got hacked right after being published, leading to
50m$ money loss.

My take on this: FreeTON community have to build some kind of
‘continuous’-verification paradigm that will encourage smart contract
safety in the long run, not limited with the strict rules of a specific
contest.

Thanks!

4 Likes

First let me welcome Infotecs team to join Free TON formal verification efforts. It is much appreciated. I hope to see you as part of the FV Sub Governance that we plan to introduce very soon.
Totally agree on your point of cooperation, but disagree with way to achieve it. Competition is a major market force including in the field of scientific research. If, say, we would have a grants system there would still be a competition simply because the resources are not unlimited. Fortunately we don’t have a grants system, because unlike scientific community we want to foster entrepreneurship. You don’t need to go very far: Covid 19 vaccine story proves competition and private entrepreneurship bets academia hands down (in 5 days to be precise).
The cooperative framework that you are talking about and which is in our case is called “sub-governance” still should run competitions for its members internally. I understand sometimes it is hard to decide which approach should win, that is why in case of formal verification it is organized in a form of staged contests. The contests can be frequent but the funds should be distributed disproportionally and with good level of competition to achieve best results.
I did not quite get your point about DAO contract and how that apply to us as Free TON has stated from the very beginning its dedication to contract formal verification.

2 Likes

It would be great if Evgeny and Sergey can present here analysis of competitors work. It will be not only help for jurors, but start of cooperations for benefit of community

2 Likes

Dear colleagues!

The contest has finished. I wouldn’t say the results are somewhat
surprising for me. After all, the document we developed is only the
beginning of the formal verification effort, yet it is done very
thoroughly.

Thanks for those jurors who accepted our work and for those who,
despite being forced to reject the work, still highlighted its quality
and depth in comments.

All key decisions regarding this contest are probably already made,
and this message has no impact on the future. Anyway, I would like to
concisely describe what we are aiming to build in the end should this
work get the support of this community.

We aim to build the DePool checkable formal model using techniques
developed inside InfoTeCS R&D center for verifying Solidity
smart-contracts.

After we build the model, we are going to automatically verify that
all high-level properties of DePool (stated in Section 4 of The Specification)
hold for any possible alternations of DePool
transactions. To make this feasible, we have to put restrictions on
search “depth”, as well as other params, like number of users, user
balances etc. And this is despite the fact that the search will be
made by a cluster of 20 high-profile servers during the two weeks
interval. In the end, we get proofs of the correctness or we get
failure scenarios that we put into the final report.

Please note, that our ambition is somewhat different comparing to
approaches of other teams, namely to check the correctness of some
predefined business scenarios. The total amount of business
scenarios for systems like DePool is astronomically huge, and because
of that, it is very unlikely to verify all of them using this
approach. You have to weight all related risks here.

I would like to notice the high technical level of other participants
solutions. The deductive verification approach (mechanical reasoning in Coq)
is theoretically appealing and sound, yet its completeness in the broad sense
is not obvious at all.

Thanks everyone and Good luck!

5 Likes