双十一喧嚣未散，王校长 ig 刚夺冠…
作为中奖绝缘体的小编自以为没那福分成为锦鲤…
于是乎，默默地逛起论坛，顺手把喜欢的文章翻译整理出来供各位看官把玩…
希望各位看得愉快，各有收获…
智能合约形式化验证主要是基于形式化验证来确认目标合约是否安全并且满足 SN[T]ARKs 的某些规范，相应的功能类似于传统互联网中的 “https”。
1.1 背景
现状是智能合约的形式化验证是在每个计算机上执行的，如果某人已经对合约进行形式化验证，那么当前用户是无法在不执行形式化验证程序的前提下验证合约。而对智能合约来说，它是无法判定其他合约是否经过形式化验证的。
LayerX Inc. R& D 团队（ R & D: Research and Development) 针对上述问题提出了链上的解决方案，并且计算成本要低得多。
该解决方案带来的主要有2个好处：
1）智能合约可以自行判断即将调用的其他合约是否经过形式化验证并满足某些规范要求。
2）移动应用程序等轻量级客户端可以查看某个合约是否符合某些规格。
换句话说，该协议在区块链中相当于 “https” ，虽然这不能杜绝黑客攻击，但会给予某种程度的安全保证。
1.2 协议摘要
在协议中，验证者合约(verifier contract ) 验证 SN[T]ARKS 证明，即证明给定的 EVM 字节码满足某些规范。SN[T]ARKS 证明 即 SNARKS 证明及 STARKS 证明，从 zk-SNARKs 到 zk-STARKs 是空间换时间的取舍，虽然都不完美，但在持续进化中。用户合约或是其他合约可以通过询问相应的验证者合约来获取目标合约是否经过形式化验证或满足某些规范。
1.3 案例
以下是 1.1 中所描述的相应示例：
（1） 无代币的加密抵押系统
在稳定币或衍生物的一些金融协议中，不仅包括以太币，还包括其他的基于 ERC20 协议的代币所涉及的加密资产被用作抵押品，即便这些协议能够处理代币价格下跌的情况，但是如果抵押资产所依据的合约有漏洞，比如著名的整数溢出或是重放攻击，可能会造成“黑天鹅”事件，以及整个系统都将被破坏。
如果基于这些协议的系统合约禁止使用未经形式化验证的代币作为抵押品，在一定程度上将减少 “黑天鹅” 事件的发生。
（2）安全钱包应用或 dapp 浏览器
钱包应用或 dapp 浏览器基于验证者合约来避免使用不安全的智能合约。这不仅限于检查溢出漏洞 (overflow)。
Layer2 协议，如 plasma 以及状态通道在未来会发布相应的标准。L4 以及 Celer 团队证致力于状态通道的相关协议研发，这些标准将被编写为适用于形式化验证的正式规范。
基于这些协议，钱包应用或是 dapp 浏览器可以警告用户所使用的合约是否符合这些标准。
好了 ，以上都是一些虚的客套话，接下来小编给大家上正菜。
emmmm……祖国的花骨朵表示只想学习，不想吃，端走！
2.方法
2.1 SNARKs 形式化验证
鉴于证明体量足够小并且适合区块链，本文使用 SNARK 作为非交互式证明系统。
SNARKs 的证明体量只有 288 字节，其中 128 字节用于安全性证明。
STARKs 较 SNARKs 的优势在于需要可信设置以及证明成本，但加密证明的容量也会大得多 。
下面讨论 SNARKs:
copyright @ LayerX Inc. R&D 团队
验证者智能合约需要在设置阶段预先部署。
图示中的前端 (Frontend）部分，形式验证程序在 RAM 中被执行，RAM 是一个通用计算模型，该节点生成 SNARKs 的电路。
而在后端(Backend) 中，生成的电路和 RAM 用于 SNARKs。
设置(Setup)阶段主要是作为生成证明密钥和验证密钥的预处理阶段。
只有当证明人通过形式化验证的字节码时，从证明人传递给验证者的证明才会被接受
并且通过验证者合约返回 true ，并通知 dapp 浏览器或被其他合约调用。
基于 SNARKs 的验证过程公式化如下 ：
Pprove(w = bytecode, x = hash(bytecode)) {return proof}
Pverify(proofkey, hash(bytecode)) = True/False
x 是传递给链上计算的主要输入，w 是辅助输入
bytecode 是需要验证的合约字节码
proof_key:形式化验证结果的证明密钥
鉴于智能合约字节码的体量过于庞大，以致于无法放于链上，因此将它作为辅助输入（也可以称为私有输入），只把它的哈希值作为主要输入（即公有输入）。
以下是 P_prove 的伪代码片段：
为了将程序转换成布尔电路，因此引入了 TinyRAM 等计算模型，并基于这些计算模型实现形式验证器。
私有输入变量包含证明，以及除了对字节码进行哈希处理之外，如何对其应用推理规则的对象。
当 P_verify 返回值为 true , 验证后的合约在部署者合约中注册或是发出事件以将结果通知给链下客户端。
2.3 设置
上述的协议中，验证者合约需要在合约的可信任列表中事先注册或是基于该协议的移动应用程序。
这些协议皆是基于 verifier 合约的正确性，即
1）形式化验证的算法
2）需验证的形式化格式
3）表示形式化验证算法的电路
4）SN[T]ARKs 验证程序
3 挑战&解决方案
3.1 面临的主要挑战
实现这一目标的主要困难在于将形式化验证程序转换为电路。大多数形式验证方法采用 Z3 作为 SMT 求解器或是使用 Coq ，Isabelle 等交互式定理证明器。
具体来说，主要存在两个挑战：
（1）实现方面的困难
已有的几个库，如 Z0Krates ,xJsnark ,以及 Pequin 来帮助将程序编译为 SNARKs 电路。但是该领域专属语言(DSL) 无法与 JAVA,PYTHON ,C++等匹敌，因此实现形式验证器非常困难，没有足够的文档支撑，并且其中的大部分都不是为了生产用途。
（2）电路复杂性
SNARK 的验证时间和证明体量是恒定的，但随着程序复杂性的增加，约束的数目也会随之增加。即生成密钥的时间和成本。
因此形式化验证的计算成本是巨大的，如 DIZK 等库则用于降低电路的复杂性，节约计算成本。
gnosis 团队预估基于 AWS 和 DIZK ，他们的去中心化交易所的成本为 1200 美元。因此优化工作不仅应在后端进行，前端也应该进行优化。
3.2 解决方案
(1)通用计算
LayerX 团队计划基于 LLVM 实现形式化验证并将其编译到 RAM 以转换成电路。TinyRAM 能够生成复杂度较小的电路，
但因为基于 LLVM 后端实现 TinyRAM 过于困难，因此转而使用与 TinyRAM 较为类似的后端，其中一个是 RISC-V,它的指令集较为简单并且数量有限。于是 LayerX 团队将其作为生成电路的计算机器。
但是因为 RISC-V 的指令集较 TinyRAM 更为庞大，因此在生成电路的效率方面有所不及，并且在计算形式化验证算法方面面临着更大的困难。
(2)计算量更少的形式化验证算法
其中一个非常有前景的方法是移除证明搜索部分，因为证明搜索需要大量的计算，以便专注于 给定证明的验证。
形式化证明软件在人类的帮助下半自动地找到证明，推理相应的代码规则。因为由链下形式验证器生成的证明可以作为私有输入进行传递，并且所有的程序都专注于对验证证明，所以协议中转换成电路的程序不一定要找到证明。
另一种方法是针对某些漏洞的启发式方法。
比如 Securify 在表达其 DSL 的目标字节码语义中使用模式检测，通俗来说，违反智能合约的属性设置其实也违反了更简单的属性设置，而这更容易进行审查。与 KEVM 以及交互式定理证明器相比，该算法更容易转换为电路。但如果没有 Z3 等自动定理证明器，证明“无溢出”将是非常困难的。
4.展望未来
针对形式验证器的电路复杂性研究至关重要，以及包括 STARK 在内的零知识证明系统研究。
LayerX 未来的长期目标包括：
1）通过通用性计算进行 SN[T]ARKs 证明的基础性开发工作。
2）更加友好的 SN[T]ARKs 形式化验证开发。
