Ontology and Beosin Launch First Customized Formal Verification Platform After Ethereum
→ Upvote and comment on Reddit, 8 people will be picked to each win 50 ONG!
In the field of blockchain technology, the security of smart contracts is of utmost importance. That is why Ontology and its strategic partner Beosin (LianAn Technology), a Chengdu-based tech company focused on blockchain security, have launched VaaS-ONT, the world’s first customized formal verification platform after Ethereum’s.
Last July, Beosin joined Ontology’s “Co-Builder Plan” and worked with Ontology to focus on smart contract development, security auditing, and formal verification, in a bid to strengthen the security of smart contracts and blockchain platforms, creating safe, secure, and reliable blockchain infrastructure. VaaS-ONT is the world’s second formal verification platform customized for public blockchain, and has been deeply integrated into SmartX, Ontology’s smart contract integrated development environment.
Beosin’s formal verification technology has been applied to the civil aviation and defense industry for many years, which allows VaaS-ONT to provide a “military-grade” formal verification service. Compared to the traditional method of manually auditing smart contracts, the VaaS-ONT formal verification tool is able to precisely locate vulnerable code, quickly find out the causes, and verify common security vulnerabilities, security properties, and functional correctness of smart contracts or blockchain applications, thus strengthening security significantly. At the same time, VaaS-ONT platform will customize smart contract applications according to the requirements of Ontology’s users and provide security design for the contracts.
VaaS-ONT formal verification tool
Operation Steps
1. Log in to SmartX
Go to https://smartx.ont.io/ in Chrome, click the logo below to log in with your GitHub account.
2. Create project
After you have logged in, click “Create Project” to create a project. Currently formal verification only supports smart contracts written in Python.
Select programming language.
3. Write smart contract
Now you can use the built-in contract template to quickly create and edit contracts.
4. Compile smart contract
After writing the contract, select compiler version 2.0 (currently formal verification only supports version 2.0), click “Compile” to compile a contract.
5. Formal verification for smart contract
Switch to the “Verify” tab after compiling, click “Formal verification” to start formal verification, and the result will be shown on the right.
About Formal Verification
Introduction
In computer science, specifically software engineering and hardware engineering, formal methods are a particular kind of mathematically-based technique for the specification, development, and verification of software and hardware systems. The use of formal methods for software and hardware design is motivated by the expectation that, as in other engineering disciplines, performing appropriate mathematical analysis can contribute to the reliability and robustness of a design.
In the field of smart contracts, formal verification uses mathematical and logical language to precisely define smart contracts, their operating environment, correctness, and security, and seek to verify the correctness and security of smart contracts through mathematical proof and logical reasoning. Compared to conventional test methods, formal methods are able to define the required correctness and security more precisely, and ensure higher coverage. In normal development processes, formal verification methods are combined with other methods to ensure blockchain security.
Main functions of formal verification tools
- Static detection: The compiler has checked most of the basic detection items and is able to do more.
- Dynamic detection: The most valuable part of formal verification tools. Dynamic detection items include Div-zero-occurred, Index-out-of-range, Assert-fail, Require-fail, Integer-overflow-occurred, Integer-underflow-occurred, and Data-injection-attack.
For more details, please refer to the Ontology Formal Verification Tool Detection Function List.
Are you a developer? Make sure you have joined our tech community on Discord. Also, take a look at the Developer Center on our website, there you can find developer tools, documentation, and more.
Find Ontology elsewhere
Ontology website / Ontology GitHub / ONTO website / OWallet (GitHub)
