The official launch of the First Global EOS-Based Formal Verification Project!
On the 23rd of September 2019, the Blockchain Technology Research and Application Joint Laboratory (a Starteos established company) and the University of Electronic Science and Technology of China (UESTC) have developed the acceptance and presentation of the results of the First Global EOS-Based Formal Veriﬁcation Project.
Throughout this past year and ﬁve months, the doctoral students and professors of UESTC have been working around the clock and have overcome the many technical issues throughout this process to make this ambitious goal a reality.
For the presentation, it began with Mr. Qian, an assistant professor from UESTC, introducing the general information of the project to us.
This is Qin Tang, a student from the university, presenting the operational process of the project.
This is Mr. Li, the CEO of Starteos, having intellectual discussions with the members of the laboratory.
Hope is just like the spark, which always promotes the continuous advancement of human civilization, and time enables the spark that becomes ﬁre.
In the future, the laboratory will continue to research and develop this project, which will optimize the DApp developing mode and offering a safer and more efﬁcient smart contract service.
What are the more precise ways of testing and verifying a security auditing? How do we solve the system bugs and problems that bother computer programmers? The answers will come out soon with the establishment of the First Global EOS-Based Formal Veriﬁcation Project!
Currently, the Blockchain Technology Research and Application Joint Laboratory established by Starteos and the University of Electronic Science and Technology of China is The Global EOS-Based Formal Veriﬁcation Project team.
The formal veriﬁcation is to use logic to verify the credibility of the program to get the expected results without bugs.
Two ways to verify:
The ﬁrst way to verify is theorem proving, full name is symbolic execution-based theorem proving; another one is symbolic execution, full name is symbolic execution-based dynamic constraint solving.
The goal of this project is to provide EOS smart contracts with the formal veriﬁcation toolchain, C++ grammar compiling, conversion, and interpretation proving.
Principals of project design
There four characters existing in the system: the user, analyst, evaluator, and administrator.
Users can log in to upload the EOS smart contract, and the analysts will be able to evaluate the contracts and review the veriﬁcation results; the evaluators arbitrate the contracts in dispute; And, the administrators manage the website platform’s permission.
Project operation process diagram
The work in phase three:
Compared with the second phase, the main focus during this was introducing KLEE to the system, which provides EOS smart contracts with a different form of veriﬁcation, and including the symbolic execution without the theorem veriﬁcation.
Please press the link to learn the results from the ﬁrst phase.
Formal veriﬁcation/Smart contract auditing from the omniscient perspective.
Press the link to learn the results from phase two.
The First Globally EOS-Based Formal Veriﬁcation Project has got the breakthrough.
This project has veriﬁed several contracts through their needs, and before the veriﬁcation, it has ﬁnished the compiling work for the static chain library. The KLEE veriﬁcation is seen to be the essential step of the entire project, which is compiling a static chain library to support an EOS smart contract.
To make sure the veriﬁcation transfers over quickly, the KLEE does not load any external libraries and the self-providers uclibc, which is just a tiny C library which is unable to ﬁnish the logic veriﬁcation to the EOS smart contract. So, in short, we are trying to import the DLL (Dynamic-link library) from eosio.cdt.
The second problem is that the DLL from eosio compiles through GCC, but KLEE is only compatible with .a and .so ﬁles which are compiled through LLVM, so we need to recompile all the DLL in eoiso through LLVM. Furthermore, ﬁnally, we import the new generated DLL to KLEE to obtain the veriﬁcation results.
We have generated ﬁve static chain DLL to support the veriﬁcation through our compiling, which includes libc++.a, libc.a, libnative.a and libeosio.a. The system has also systematically veriﬁed the hello contract, multi-index example contract, multi betting contract, NBA contract, and error check contract.
The advantage of symbolic execution is one of the most popular symbolic execution engines; KLEE provides a ﬂexible modular framework that enables others to construct various technology-based on symbolic execution. Currently, the main types of vulnerability detection supported includes: memory leak, array out of bounds, null pointer, the denominator is 0 in the division and the remainder. For the program testing aspect, KLEE has lots of outstanding features as a more mature tool in symbolic execution and error testing.
Advantages for KLEE
The test cases automatically generated by KLEE covered 84.5% of the total COREUTILS line and 90.5% of busybox (ignoring the library code). The average coverage path of these testing in each tool code is over 90% (Median: exceed 94%), and the coverage is 100% in 16 COREUTILS tools and 31 BUSYBOX tools.
2.Extremely high accuracy of the test
KLEE can detect many vulnerabilities which are difﬁcult found by human beings, and these detections are not limited to low-level programming errors. When it is used to cross-check the same purported BUSYBOX and GNU COREUTILS tools, it automatically ﬁnds functional errors and many inconsistencies.
3.Extremely high efﬁciency
KLEE’s 89-hour test path coverage on COREUTILS was 16.8%, which is higher than the project developers’ cumulative test suite coverage over 15 years. KLEE testing examples can be operated on the code’s original version, which largely simpliﬁed the testing and error report.
The applications of KLEE in the project
1.The Code library compiling needed for contract veriﬁcation The EOS related function library is compiled and linked by Clang and llvm to form a static library in llvm bitcode format.
2.Construct the contract veriﬁcation codes Symbolic operation on contract memory through inserting KLEE makes symbolic in the key points. The symbolic execution-only needs an analyst compared with theorem veriﬁcation, and the request for the analyst is not high, which largely improved the efﬁciency of contract veriﬁcation.
Symbolic execution process diagram
Advantages of theorem veriﬁcation
The actual cost of theorem veriﬁcation is relatively high because it requires a large number of manual participation. So, this project starts with the symbolic execution-based veriﬁcation mode to think about the questions.
Firstly, the smart contract code transformed into the equivalent formal model through the manually compiled translator and interpreter. Secondly, manually abstract modeling carried to verify the functions or design requirements and give the formal theorem to be proven. Thirdly, prove the theorem to be proved by theorem proving technique, and then the system will get the veriﬁcation results (true, false, and unprovable). Last but not least, the system evaluates the smart contract code through veriﬁcation results (true, false and unprovable)
Advantages of theorem veriﬁcation based on symbolic execution
The method offered by this project can identify, translate, and modeling for smart contracts automatically, and it makes the automation veriﬁcation strategy easier by integrating the process of veriﬁcation.
Through this project framework, it can ensure the consistency of the model and the environment for operation. The consistency of the model is that this method can convert and model the source code to be veriﬁed line by line, forming a formal speciﬁcation model consistent with the source code behavior. Operating environment consistency refers to the accurate modeling of source code semantic behavior in a formal veriﬁcation system, which accurately reproduces the original behavior of the program.
This method enables veriﬁers with individual experiences to formalize modeling for speciﬁc problems without modifying the core mechanism within the original veriﬁcation framework.
This method is designed based on the module component, consisting of several independent functional module components, and each module has a separate extension interface that can be modiﬁed and extended in a different language and different veriﬁcation environment.
Project results output
√ Interpreter: compiling (grammatic level) and converting for contract
√ Full-form veriﬁcation engine: the EOS symbolic veriﬁcation subsystem, create for EOS development language （C++11）and based on the KLEE mechanism.
√ WEB Integration
√Software development process ﬁles: requirements analysis speciﬁcation, design abstract, design details (WEB), User manual, testing report.
√Project acceptance report.
√ Blockchain situation analysis.
√ Formal veriﬁcation research report.
√ Formal veriﬁcation results report.
√ The smart contract formal veriﬁcation platform development white book.
3.The situation of intellectual property rights
√Authorized journal articles published at home and abroad.
√Utility Patent Application.
√Software copyright: EOS smart contract interpreter and formal veriﬁcation platform.
Project development plan
In the ﬁrst phase of project achievement presentation, Mr. Li, the founder of the project and the CEO of Starteos, said:
We should focus on the realistic and applied features of this formal veriﬁcation project, and we aim to create a big product that will not only serve for Starteos but also for the whole EOS society and the entire blockchain industry.
In the project acceptance meeting, Mr. Li stated that: There are no previous good cases and examples for the EOS-based smart contract formal veriﬁcation currently, but we have got some results through our hardworking and endeavor in this market.
However, we still need to reduce the manual intervention and to lower the threshold for use if we want to apply this into the market and large-scaly serve the developers. So, we will continue to put efforts in the following areas in the future after the acceptance for the project.
1.Optimize the C++ supporting level Gradually complete the fully-supported for eosio cpp, incomplete modules gradually adding support for standard libraries.
2.Standardize the veriﬁcation requirement Unify theorem design format and make more general and better veriﬁcation strategies.
3.Reduce labor participation At present, there is still a lot of work that requires analysts to participate in for theorem veriﬁcation, including formal modeling of pre-and post-set conditions, modeling of formal theorems to be proved, and the selection and invocation of automatic veriﬁcation strategies.
4.Optimize algorithms and improve efﬁciency There are still lots of structures which can be optimized in the theorem veriﬁcation framework, and the optimization can improve the veriﬁcation efﬁciency.
At the end of the acceptance meeting, Mr. Li said: We should focus on and insist on one speciﬁc goal and dream to move on; only in this way can we achieve what we want. Just like the formal veriﬁcation project, nobody can judge whether it is right or wrong as it has not been tested by the market.
However, we do trust the things we are doing is right, we are trying to create something to serve the whole blockchain market. So, we need to do it better, just like what I usually said, do the best or nothing. We do believe this First Globally EOS-Based Formal Veriﬁcation Project can optimize the current DApp developing mode, create more efﬁcient and safer smart contract services to help boost the ecology and market development.
We are looking forward to seeing more exciting news and products in the future, coming with the formal veriﬁcation projects.