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 Verification Project.
Throughout this past year and five 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 fire.
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 efficient 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 Verification Project!
Introduction
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 Verification Project team.
The formal verification is to use logic to verify the credibility of the program to get the expected results without bugs.
Two ways to verify:
The first 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 verification 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 verification 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 verification, and including the symbolic execution without the theorem verification.
Please press the link to learn the results from the first phase.
https://steemit.com/formal/@starteos/starteos-uestc-blockchain-laboratory-reported-the-first-stage-formal-verification-research-result
Formal verification/Smart contract auditing from the omniscient perspective.
Press the link to learn the results from phase two.
https://steemit.com/blockchain/@starteos/the-world-s-first-eos-smart-contract-based-formal-verification-project-has-made-a-breakthrough
The First Globally EOS-Based Formal Verification Project has got the breakthrough.
This project has verified several contracts through their needs, and before the verification, it has finished the compiling work for the static chain library. The KLEE verification 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 verification 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 finish the logic verification 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 files which are compiled through LLVM, so we need to recompile all the DLL in eoiso through LLVM. Furthermore, finally, we import the new generated DLL to KLEE to obtain the verification results.
We have generated five static chain DLL to support the verification through our compiling, which includes libc++.a, libc.a, libnative.a and libeosio.a. The system has also systematically verified 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 flexible 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
1.High coverage
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 difficult 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 finds functional errors and many inconsistencies.
3.Extremely high efficiency
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 simplified the testing and error report.
The applications of KLEE in the project
1.The Code library compiling needed for contract verification 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 verification 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 verification, and the request for the analyst is not high, which largely improved the efficiency of contract verification.
Symbolic execution process diagram
Advantages of theorem verification
The actual cost of theorem verification is relatively high because it requires a large number of manual participation. So, this project starts with the symbolic execution-based verification 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 verification results (true, false, and unprovable). Last but not least, the system evaluates the smart contract code through verification results (true, false and unprovable)
Advantages of theorem verification based on symbolic execution
1.automation
The method offered by this project can identify, translate, and modeling for smart contracts automatically, and it makes the automation verification strategy easier by integrating the process of verification.
2.Consistency
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 verified line by line, forming a formal specification model consistent with the source code behavior. Operating environment consistency refers to the accurate modeling of source code semantic behavior in a formal verification system, which accurately reproduces the original behavior of the program.
3.Flexibility
This method enables verifiers with individual experiences to formalize modeling for specific problems without modifying the core mechanism within the original verification framework.
4.Expandable
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 modified and extended in a different language and different verification environment.
Project results output
1.Software completion
√ Interpreter: compiling (grammatic level) and converting for contract
√ Full-form verification engine: the EOS symbolic verification subsystem, create for EOS development language （C++11）and based on the KLEE mechanism.
√ WEB Integration
2.Files output
√Software development process files: requirements analysis specification, design abstract, design details (WEB), User manual, testing report.
√Project acceptance report.
√ Blockchain situation analysis.
√ Formal verification research report.
√ Formal verification results report.
√ The smart contract formal verification 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 verification platform.
Achievements exhibition
Project development plan
In the first 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 verification 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 verification 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 verification requirement Unify theorem design format and make more general and better verification strategies.
3.Reduce labor participation At present, there is still a lot of work that requires analysts to participate in for theorem verification, including formal modeling of pre-and post-set conditions, modeling of formal theorems to be proved, and the selection and invocation of automatic verification strategies.
4.Optimize algorithms and improve efficiency There are still lots of structures which can be optimized in the theorem verification framework, and the optimization can improve the verification efficiency.
Conclusion
At the end of the acceptance meeting, Mr. Li said: We should focus on and insist on one specific goal and dream to move on; only in this way can we achieve what we want. Just like the formal verification 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 Verification Project can optimize the current DApp developing mode, create more efficient 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 verification projects.
