The world’s first EOS Smart Contract based Formal Verification Project has made a breakthrough
On May 28th, 2019, the “Joint Laboratory for Research and Application of Blockchain Technology” jointly built by Starteos and University of Electronic Science and Technology of China (UESTC) reported the results of the second phase of the project, this impressive world’s first EOS Smart Contract based Formal Verification Project has made a breakthrough.
The laboratory was established on April 18th, 2018, which is dedicated to cultivating talents for the blockchain industry and promoting the rapid development of blockchain technology.
At present, the second phase of the project has completed the full formal verification engine, WebAssembly, paper publication, patent point selection based on the development language for EOS (C++11) and other work that can realize the translator machine for contract lexicography, grammar analysis, and transformation.
What are more rigorous testing and security auditing? What to do with the bugs that have been concerning the developers? You will find out the answer after reading this phase of the report!
Participants in the opening presentation of the project results report are:
Ang Li — Founder and CEO of Starteos ;
Nan Sang — Professor at UESTC ;
Weizhong Qian — Associate Professor at UESTC ;
Zheng Yang — Doctor at UESTC;
Vahid Toosi — CEO of EOS Sw/eden
Eric Björk — CTO of EOS Sw/eden
Michael Yeates — CEO&CTO of EOS DAC
Gangqiang Liu — CEO of Alchemy
Zi Cen — Founder and CEO of Hello EOS
Associate Prof. Weizhong Qian of UESTC explains the progress of the project
Yifang Zeng, a member of the Joint Laboratory Project, demonstrates the project results
Xi Yang, a member of the joint laboratory project, introduces the project concept
Dr. Zheng Yang, the core member of the laboratory, interprets the core technologies of the project
Monica is translating project content for Michael and Eric
Both of them listen to the report carefully and said they are looking forward to the completion of the project
Dr. Zheng Yang answers questions
Ang Li, Vahid and Prof. Nan Sang are discussing the completion of the project
Concept Explanation
The project adopts a formal verification method to carry out security verification on the smart contract. The smart contract verified is proved to have no loopholes in programming logic, providing a reliable verification method for smart contract.
The formalization method adopts some rigorous mathematical theory to model, describe, deduce and prove the target object accurately and precisely.
The formal verification verifies the reliability of program with logic and proves it could get anticipated results without bugs.
At present, the Joint Laboratory for Research and Application of Blockchain Industry jointly-established by Starteos and UESTC is the world’s first team works on Formal Verification Project based on EOS Smart Contract.
In other words, the purpose of Starteos carrying out this project is not only to serve its own products but to serve the whole EOS ecosystem even the whole blockchain industry.
Operation Model
There exist four kinds of roles in the project system: User、Analyst、Evaluator、Administrator, each role corresponds to different functional scope:
User — Who needs to validate the contract
Users are required to log in and enter the home page, where they can upload the EOS smart contract, and enter the contract name and contract description respectively in the input box of contract name and contract description.
Analyst — Evaluate contact and feedback validation results
After the analyst undertakes the contract, he/she can view the contract details and analysis page. In this page, he/she can see the sugar code formed by the contract requirements and contract source code translation.
In the pre-conditions and post-conditions text boxes, the analyst can fill in the pre-conditions and post-conditions as required.
At the same time, the analyst could describe the pre- and post-conditions in the description box for the evaluators' reference.
At last, the analyst fills in the report, enter the validation type, relevant requirements, validation result and comments of each requirement.
Each uploaded contract requires at least two analysts to review.
Evaluator
Arbitration of contracts in dispute to ensure consistency of verification results
The evaluator mainly looks at contracts where two analysts submit an analysis and the system determines that the analysis results are inconsistent.
The evaluator can view the requirements uploaded by the users of the requirements and the translated formal model of the source code of the contract, as well as the analysis report, description and pre- and post-condition of the contract by two analysts.
For the contract to be evaluated, the assessor can perform two operations: “accept” or “reject”.
Administrator — Manage permissions, system, and users
Four different roles connect to each other to achieve the one-stop service of “contract submission — verification — report”.
Project Advantages
Traditional security testing is divided into two types: static testing and dynamic testing.
Due to the high degree of manual participation in traditional security testing, limitations of test cases and other factors, it is difficult to conduct an in-depth analysis of the code, fully verify the reliability, and even more difficult to ensure the correctness of the code logic.
Compare with traditional security testing, Joint Lab project of Research and Application for Blockchain Industry has the following advantages:
Uniqueness: it is the only formal verification platform that adopts higher-order theorem proof technology for EOS based on the C++ source code level.
Full formalization: the testing platform has conducted formal modeling on target hardware and software, in order to fully ensure the correctness and reliability of the platform itself.
Highly automatic: compared with the traditional theorem proving method, the experimental platform has higher automation ability in modeling and verification
High Reusability: the current experimental platform adopts modular design, which can be compatible with the formal protocol of multiple languages, and can be extended to customized modules for support.
The implementation of the compilation、transformation and interpretation of the original contract provides a toolchain prototype system for the formal verification of EOS contracts.
Next phase goal
In the next phase of development, the joint lab will focus on the following work modules:
— The symbol execution technology is introduced to make up for and overcome the technical defects and difficulties in the current theorem proving technology so as to improve the efficiency of the tool towards the commercial practical goal.
— Further improvement of the translator machine
— System performances optimization
Albert Camus, a famous French writer, once said: “Passion and pain make heroes. This is the price that worldly passions must pay.”
The passion for EOS has made Starteos think about things that can drive the industry since its inception, such as today’s introduction of the first formal validation project based on EOS smart contracts.
The frustration caused by the bottleneck in the R&D process has worn down numerous technicians, and also set a high threshold for other teams who want to get involved in this field.
Each step of moving forward, Starteos has been through careful planning and affectionate expectation.
For the first formal verification project based EOS Smart Contracts, we considered more than just the theory.
With the continuous progress of research and development, we will consider its practicability and application, and strive to build a formal verification project that can meet the huge market demand and cover the whole EOS ecology, or even the whole blockchain industry.
Hope is the fire that pushes human civilization to keep moving forward, and time will make it like spread wildfire.
The third phase of formal verification project has been carried out, let’s looking forward to more exciting things.
