新型智能合约Q语言,如何实现100%无BUG?(一)

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

新型智能合约Q语言,如何实现100%无BUG?(一)

新型智能合约Q语言,如何实现100%无BUG?(一)

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

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

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

新型智能合约Q语言,如何实现100%无BUG?(一)

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

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

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

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

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

新型智能合约Q语言,如何实现100%无BUG?(一)

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

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

新型智能合约Q语言,如何实现100%无BUG?(一)

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

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

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

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

来源:VNT Chain



版权声明:

新型智能合约Q语言,如何实现100%无BUG?(一)新型智能合约Q语言,如何实现100%无BUG?(一)新型智能合约Q语言,如何实现100%无BUG?(一)

作者保留权利。文章为作者独立观点,不代表巴比特立场。



发文时比特币价格

¥66780.74


本文来源于互联网:新型智能合约Q语言,如何实现100%无BUG?(一)

Click to rate this post!
[Total: 0 Average: 0]

人已赞赏
名家说每日优选行情分析

行情分析:比特币短线反弹不可持续,注意锁定利润切忌贪婪

2019-7-18 14:44:19

名家说每日优选

Bitfury Group首席技术官:区块链加速电子商务,降低信任成本

2019-7-18 14:52:22

0 条回复 A文章作者 M管理员
    暂无讨论,说说你的看法吧
个人中心
购物车
优惠劵
今日签到
有新私信 私信列表
有新消息 消息中心
搜索