1. Hi区块链首页
  2. 资讯
  3. 技术指南

Galaxy数字之美:新型智能合约Q语言,如何实现100%无BUG?(一)

本文将为大家详细讲解我们设计“一种基于形式化验证的新型智能合约Q语言”的初衷,以及其实现原理与价值。

对于技术爱好者来说,数字本身并没什么稀奇,但组合在一起的编码,却能让一个个再简洁不过的数字碰出“火花”,让这个世界变得“绚丽多彩”。也正是这些数字的改变,让编程语言带来可编程经济,数字经济时代由此到来。

我们要推动数字经济发展,其中尤为关键的便是区块链基础设施隐私安全。为此我们前期一直致力于区块链隐私安全研究,目前我们在这方面已经取得了一些突破性研究进展,这也是VNT Chain的主网Galaxy核心技术成果。

VNT Chain社区一直秉承开源开放的理念,因此任何技术成果我们都希望与大家共享,共同构建社区商业生态。接下来,我们将把这些技术成果分别整成篇分享出来,带大家一同走进数字世界,探索Galaxy数字之美。

本文将为大家详细讲解我们设计“一种基于形式化验证的新型智能合约Q语言”的初衷,以及其实现原理与价值。

05d4d335b8c447d38f42821e84fc7d5c

cf13f8d4b9ab48d6b04e1c79671f12de

我们知道高级的编程语言,C语言、JAVA等都是面向函数和过程,即把代码组织成一个个函数,实现业务逻辑就实现一个过程。 但这种方法有很多BUG,这些BUG和安全漏洞基本上不可 避免。 而智能合约代码,对安全要求极高,一旦出现问题,造成的经济损失不可估量,自从以太坊正式上线以来,由于智能合约漏洞/缺陷所带来的经济损失便数以亿记。 另外对于安全有关的领域,比如航天、高铁、核电、航空,涉及人类安全,对安全漏洞更是几乎零容忍。

目前针对智能合约安全问题的应对方式主要有两种:合约代码的测试和审计。 这两种方式能够在一定程度上有效的规避大部分的安全问题,是保证合约安全的必要手段,但是同时也存在着一定的局限性。另外一些较为复杂的业务逻辑以及更高阶的性质,如经济学,博弈论范畴的问题,通过测试或者审计的方式更是难以有效验证。

因此我们设计了一种适用于形式化验证的新型智能合约Q语言,专门针对这种安全相关领域需求。 (当然我们也支持C语言这些高级语言,只不过这种是特定的,针对这种领域的应用。)

8f57bce5c3d144479abb9f08705d113e

那么要如何实现100%无BUG呢?

形式化证明是通过形式化逻辑的方式来表示合约代码,并加以严格地推理证明。 这个过程依赖于数学逻辑推理的严密性,可以保证 100% 覆盖到到代码的运行期行为,可以明确保证在一定范围内的绝对正确,能弥补以上两种传统方式的局限。 因此形式化证明在一些安全攸关的领域,如航天、高铁、核电、航空,已经逐步得到应用,并且取得了非常好的效果。 因而对于规模相对较小而设计复杂的智能合约而言,形式化程序验证无疑是保证其安全可靠的有效方法之一。

目前采用的形式化验证理论技术,是将智能合约语言编写的代码作为数学模型,将智能合约所需要满足的要求作为性质进行证明。 进一步来讲,就是使用数学语言来描述合约代码,并证明其具有一些好的性质,例如不存在整数溢出漏洞。

形式验证是一个系统性的过程,将使用数学推理来验证设计意图在实现中是否得以贯彻。 但常用智能合约编辑语言如JAVA,C语言等等均属于高效工程应用语言,在智能合约进行形式化验证过程中需要将其工程应用语言转化为可以形式化验证的数学逻辑语言,进行函数建模,运用比较繁琐,效率比较低。

为节省人力物力以及时间成本, 我们创新研发提供的一种适用于形式化验证的智能合约编译方法,同时包含工程语言和类型数学集合。 这种新型的Q语言,能够利用形式化证明结合语言编辑,可在运行前发现所有的BUG,能保证所写程序安 全无漏洞并且操作简单的编辑语言,实现智能合约形式化验证实时进行。

901e694a7c2b4c81ba9630e6c5711f2d

我们设计这种新型智能合约编译语言主要构成包括以下:

它的语言编译器按模块划分为:工程编译模块、语法模块、形式化证明模块。其中,工程编译模块为实体类的字段方法编译,通过WASM编译;语法模块包括语法解析(Parse)与构造语法树;形式化证明模块包括高阶逻辑语言与证明工具(Issbella)。

c1c95ecaf72b4625a5772c2dbd4a8d42

它的类型系统主要包含类型(实体类的字段方法)和数学集合。相对传统合约编译语言,它的合约语言使用多种虚函数表,可以实现多类型参数,可用高阶逻辑HOL 快速表达,在进行合约形式化验证时,仅需对所使用函数定理进行证明,无需函数建模,更加便捷高效。

类型作为其中一种集合实现交并补运算,并且可直接使用高阶逻辑描述,为其所在的数学集合提供实体类的字段方法。

而数 学集合是通过泛型与实例化来实现的,只有智能合约API入口点需要具有确定的类型,而之后的函数调用均被泛型实例化,编译时根据实际调用的参数类型派生出具有不同对应类型的函数。

由于篇幅有限我们先分享到这里,关于智能合约编译及形式化验证具体实现方式我们将在下篇为大家详细分享。

–END–

VNT Chain是一个开放的社区,我们会奖励每一个为VNT Chain做出贡献的开发者。目前2019维特链(VNT)全球开发大赛 正在火热进行中,想试一试用这种新型智能合约Q语言进行开发,你可以做出什么样好玩的区块链DApp吗?快来参加我们的开发大赛一展身手,赢百万大奖吧!

了解详情:维特链(VNT)全球开发大赛火热报名中,百万奖金等你来拿

声明:登载此文出于传递更多信息之目的,观点仅代表作者本人,绝不代表Hi区块链赞同其观点或证实其描述。
提示:投资有风险,入市须谨慎。本资讯不作为投资理财建议。