Formal Verification semi-automated toolkit support for FunC and Tact

NikSoin commented 4 months ago

Summary

We propose to expand the capabilities of the Pruvendo Formal Verification Automated Toolkit to include FunC and Tact languages. Our team has successfully developed and implemented a powerful Formal Verification (FV) toolkit initially designed to be used on TVM but for Solidity language. And now we aim to bridge the existing gap for TON developers by extending support for the online automated translator, as now it supports only direct and reverse translation of Solidity and partly Rust languages to Ursus meta language (Coq embedded DSL, suitable for formal verification).

Context

Experience: Previously Pruvendo team had successfully performed several projects with TVM, during collaboration with TonLabs (later - EverX) and then Everscale blockchain:

Created formal specification for TVM Assembler. While it’s not a smart contract, but rather part of the node, its intention is to convert a stream of primitives with parameters into a cell that can be loaded into a TVM machine.
Implemented TVM Solidity syntax highlighting for VS Code.
Successfully attempted to create a framework for the formal verification at the TVM level. The Coq-based TVM engine model was created as well as support for all the TVM-primitives involved, and it was partially proved.

Significant formal verification projects, in most cases formal verification revealed bugs, left after several audits passed:

Multisignature contract
Depool - Enabling small token holders to participate in network governance
Dune - acquisition of Dune blockchain by FreeTON
Elector - contract that periodically elect a set of validators that check the correctness of transactions using the PoS paradigm
Vesting contract - distributes the predefined amount of EVERs to the recipient splitting the amount into a set of monthly uniform tranches
DEX - An order-book based DEX with the original algorithm and implementation

Explicit product map, approach and examples of Solidity/Rust->Ursus translation: https://pruvendo.notion.site/Pruvendo-formal-verification-toolkit-69639d99a52b4b60b8f2f67d4cf00e06

References

https://ursus-tools.dev/translator/

Estimate suggested reward

Milestones:

Translation support: add support to existing to convert FunC and Tact code into the Ursus meta language (Coq eDSL), ensuring seamless integration with our existing Formal Verification toolkit. This step will also include testing and optimizations. Funding: Total $60K for 2 months. Detailed plan:

Stage I. $15k, 2 weeks Description of the input language grammar (FunC, Tact) in the form of Coq inductive types and similar ANTLR representation Obtaining the AST of the program in the input language using a compiler or similar means
Stage II. $15k, 2 weeks Translation of the AST of the input language into the internal representation obtained at the stage I Development (upgrading) of an internal representation of the output language (Ursus) suitable for conversion from the internal representation of the input language Converting the internal representation of the input language into the internal representation of the output language
Stage III. $15k, 2 weeks Development of Coq notations to maximize the visible similarity of the text representation of the input language Translation of the internal representation of the output language (Ursus) into a text representation in the output language, correct enough for the compilability in Coq
Stage IV. $15k, 2 weeks Development of test programs in the input language, which are a valid set for translation and testing of the translator

Documentation and training: provide comprehensive documentation and training resources (tutorials and seminars) for TON developers to effectively use semi-automated Formal Verification toolkit, emphasizing best practices and integration guidelines. Funding: $4K for 2 weeks

Funding Asked: $64K in total Frame 46

anton-trunov commented 4 months ago

This is a very ambitious project which, if implemented, would bring to the TON ecosystem state-of-the-art tooling to ensure contract security and correctness with the level of guarantees way beyond traditional testing, because it uses formal mathematical proofs at its core, see, for instance, the analogous tools and techniques for the Ethereum blockchain: https://ethereum.org/en/developers/docs/smart-contracts/formal-verification.

The question to Pruvendo from my side would be "How do you compare your approach to the existing Ethereum formal verification tools, like Certora prover or others"?

delovoyhomie commented 3 months ago

This issue has been automatically closed due to 14 days of inactivity and lack of the additional information requested. Please feel free to reopen it if you wish to provide further details or require assistance.

andruiman commented 3 months ago

This is a very ambitious project which, if implemented, would bring to the TON ecosystem state-of-the-art tooling to ensure contract security and correctness with the level of guarantees way beyond traditional testing, because it uses formal mathematical proofs at its core, see, for instance, the analogous tools and techniques for the Ethereum blockchain: https://ethereum.org/en/developers/docs/smart-contracts/formal-verification.

The question to Pruvendo from my side would be "How do you compare your approach to the existing Ethereum formal verification tools, like Certora prover or others"?

Hi Anton! Thank you for your question and sorry for the late reply. Currently I have subscribed to the topic and will reply instantly.

Regarding the question. Pruvendo verification pipeline is based on high level language properties, so we can support in theory any language and VM with shorter efforts. The underlying language Ursus can be seen as meta-language which can mimic the correspondent behaviour both in terms or original language semantics and VM specification. Another important difference we have is using the fully deductive way of verification conducted in Coq proof assistant. That brings the possibility to prove much more complicated properties, using high level logic and powerful type system of Coq itself. However we have a lot of automation written and tested on a number of functions from real contracts.

So, summarizing:

high level language support
rapid new VM support at level of standard functions
deductive verification in Coq proof assistant
a number of automations implemented to support simple of patternized proofs

anton-trunov commented 3 months ago

Thanks a lot for the clarification @andruiman!

Please feel free to reopen it if you wish to provide further details or require assistance.

Looks like this issue could be reopened since additional info has been provided

NikSoin commented 2 months ago

In addition, I'd add a more explicit technical description of Pruvendo approach: Pruvendo_workflow (7).pdf

We also propose subscription-based support for each new version/element of the abstract syntax tree of FunC. We will ensure timely support within one month of each commit.

ton-society / grants-and-bounties