Sun. Jan 2nd, 2022
    Free TON

    In April, the Formal Methods Sub-Governance was created to make Free TON more secure and robust. For more details — what is formal verification and how it is used in Free TON — we turned to one of the initiators of the Sub-Governance creation, Sergey Egorov (he is also a co-founder and one of the leaders of Pruvendo).

    • Please tell us about your background and how it all started.

    I have worked for quite a long time as the Head of QA in companies such as Oracle, and I am well aware of the field of quality control. Then I got tired of everything, and I started doing business together with my partner Andrey Lyashin (one of the authors of the NOT a TON binary system concept — ed.). We started with high-tech consulting and we went from one extreme to the other, but in the end, we returned to the “native harbor”. I became a Head of Software Development at a traditional outsourcing company, but I wanted something different.

    And about eight years ago, Andrey learned about formal verification. There was a complete feeling that there is a future behind it, a business, something big and interesting, but we did not understand what exactly. We tried different options, came from different sides, and eventually came up with the idea that it might be interesting for a smart contract. Indeed, at some stage, we were introduced to the guys from Free TON, who hold the same opinion.

    • How long ago did you come up with the idea to create a formal verification Sub-Governance system in Free TON?

    A few months ago, when we started launching the first contest, we faced the fact that, unfortunately, many people in the Main Governance did not have the competencies to objectively assess what was happening. And just then the idea arose to unite experts in this field in a separate SubGovernance, so that the group could purposefully engage in attracting new teams, developing the level of expertise, sharing experience, etc.

    • What is formal verification?

    There is a quality assurance complex — i.e. it is not only advanced testing but also a wide range of measures, ranging from the correct architecture embedded in the software product, and ending with intensive post-product monitoring. Such software testing aims to make the product reasonably reliable. And in 99% of cases, for practical use, this will be enough for you.

    If you take any product made by any decent company, then most likely it will work, although from time to time you will run into some small problems — something froze, did not work so well… It will sadden you, but not much. You will not suffer any losses because of this, because of which you would stop using the product. Therefore, this level of quality is sufficient.

    But there are areas where a different level of quality is needed — ultra-reliable. There are not very many of them. These are, first of all, medicine (it is clear that if some surgical device behaves incorrectly, everything can end sadly), all kinds of transport (aerospace), military applications and finance.

    Unlike the areas I mentioned first, finance is a relatively simple and low-entry area. If you develop medical equipment, you need to get certificates, licenses, etc., and finance is a simpler active part. Especially now there is such a smart direction as FinTech — a family of various interesting services developed and released by small suppliers. But the issue of reliability remains quite acute for services of this kind.

    The blockchain is open to the whole world, unlike, for example, banks, which sit behind seven firewalls with developed information security departments, etc. Here, the company is open to all winds, so it is easy to become victims of hackers: funds can freeze because of an illiterately smart contract and many different troubles can happen.

    Therefore, it is an area such as FinTech that makes special claims for the quality determination that, in principle, cannot be achieved by advanced testing. And here the methods of formal verification come to the rescue.

    Remember the Pythagorean theorem? You drew a right triangle, measured the leg, the hypotenuse, and the sum of the squares of the legs coincided with the square of the hypotenuse. Oh, you thought, it turned out interesting, or maybe there is some kind of law? Draw a second, third, and fifteenth triangle, and each time you make sure that the sum of the squares of the legs is equal to the square of the hypotenuse.

    So you can say that this can always be the case? Most likely yes, and this is roughly testing. You ran 15 tests and showed that this rule is true. If we prove the Pythagorean theorem, then we say that everything, the question is closed — it will always be so. This is what the formal method is.

    • That’s where the magic lies. Because how to apply this to software is completely unclear.

    It may seem quite difficult for an unenlightened person to understand how formal methods can be related to software, because mathematics is mathematics, and, for example, blockchain is completely different.

    A program is essentially a description of a system that must have certain properties. Let’s say you have, for example, a TIP-3 token system, and you need to make sure that the balance of tokens is maintained during any operation — this is a certain system property. If this program description satisfies such rules, you can prove that some properties will be executed or not.

    In a certain sense, the magic here, of course, is present. This is not ordinary programming, and not quite ordinary testing, and not quite ordinary mathematics. This is what lies at the intersection of these disciplines.

    • The document on the creation of the Formal Methods Sub-Governance at the first stage indicates interesting activities related to conversations with developers. You figure out what the system they are developing looks like, then somehow build a model and try to find vulnerabilities in it. Right?

    In fact, yes. In fact, the main problem today is getting a formal specification. Not the only one, but probably the main one. At a simple level, we say that we prove the program will work correctly. And what is “correct”? “Correct” means that it will conform to some specification, but this specification, in turn, may be erroneous and not correspond to the desired business logic.

    If the specification states that the account balance may be negative, then I’m sorry… Therefore, validating the formal specification is very broad and we take it seriously. And this is one of the areas that we are trying to actively develop now. This stops many developers from using such methods in their work to a large extent — there are no normal, simple, intuitive tools, specification assignments, and its control.

    We plan to do these things actively in the near future. And now, in order to create a normal specification, we definitely need to get the maximum information from the developers about what they really wanted. This is often not obvious.

    • Can we say that for each specific product you need to develop your own model?

    No, you don’t need to completely create your own model. It is necessary to develop a specification, and the method is the same for all — a method of translating a software product into some code in such a pseudo-language in which formal verification is carried out, and we can say that yes, every contract has its own model.

    There are several languages for formal verification, but we specifically like to program in Coq.

    But it is clear there are a very large number of repeatable moments and technologies. We do not come every time as in a new world, each time it is easier and better. But yes, in a certain way, we have to build a certain set of statements, an ecosystem around each specific contract.

    • The formal verification system first of all guarantees the absence of errors in the system’s design and precisely in the program’s logic. But does it provide a guarantee against errors if the vulnerability exists in the software tools themselves?

    In normal operation, we assume the node works correctly. But in the mid-term plans, we still plan to carry out formal verification of both the compiler and the node, the virtual machine and the entire technical stack.

    To what extent and when these works will be carried out is still a big question. But we would like to do it, because it will greatly increase the trust from the community. People will understand that this thing really works as it should, and their funds will not fly away because of some stupid mistake.

    • What will be the primary focus of work in the Formal Methods Sub-Governance?

    At the moment, work has been done with multisig, DePool, necessary smart contracts. SMV as a voting system, TIP-3 and a new electorate required to launch a new node are what is needed in the first place. I also think that some work will be done on DeFi, because the DeFi exchange is something that is extremely necessary to attract funds to the ecosystem. What will happen next is still under discussion.

    • The Formal Methods Sub-Governance also includes employees from Origin Labs, they also specialize in formal verification, have you encountered them before in other projects?

    We have heard about them, although we have not encountered them in some projects before. They are quite skilled, although they use a slightly different system of using formal methods. We will be happy to work together and exchange experiences.