Ontology and Beosin Launch First Customized Formal Verification Platform After Ethereum

The Ontology Team
Apr 11, 2019 · 4 min read
Image for post
Image for post
VaaS-ONT product page

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.

Image for post
Image for post

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.

Image for post
Image for post

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.

Image for post
Image for post

Select programming language.

Image for post
Image for post

3. Write smart contract

Image for post
Image for post

Now you can use the built-in contract template to quickly create and edit contracts.

4. Compile smart contract

Image for post
Image for post

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

Image for post
Image for post

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

  1. Static detection: The compiler has checked most of the basic detection items and is able to do more.
  2. 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.

Image for post
Image for post
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.

OntologyNetwork

A high performance, open-source blockchain specializing in digital identity and data.

The Ontology Team

Written by

Active project domain: https://ont.io/

OntologyNetwork

Ontology is a high performance, open source blockchain specializing in digital identity and data. ONTO: http://onto.app/downloadpage/TW Telegram: http://t.me/OntologyNetwork

The Ontology Team

Written by

Active project domain: https://ont.io/

OntologyNetwork

Ontology is a high performance, open source blockchain specializing in digital identity and data. ONTO: http://onto.app/downloadpage/TW Telegram: http://t.me/OntologyNetwork

Medium is an open platform where 170 million readers come to find insightful and dynamic thinking. Here, expert and undiscovered voices alike dive into the heart of any topic and bring new ideas to the surface. Learn more

Follow the writers, publications, and topics that matter to you, and you’ll see them on your homepage and in your inbox. Explore

If you have a story to tell, knowledge to share, or a perspective to offer — welcome home. It’s easy and free to post your thinking on any topic. Write on Medium

Get the Medium app

A button that says 'Download on the App Store', and if clicked it will lead you to the iOS App store
A button that says 'Get it on, Google Play', and if clicked it will lead you to the Google Play store