SCIF: A Language for Compositional Smart Contract Security

保护智能合约仍然是一个根本性的挑战。本质上，它是关于构建与不受信任代码安全组合的软件，这是一个远远超出区块链的挑战。我们介绍了SCIF，一种用于构建组合安全智能合约的语言。SCIF基于安全信息流的基本组成原理，但扩展了这个核心机制，包括防止重入攻击、混淆副本攻击和不当错误处理，即使存在不遵循SCIF规则的恶意合约。SCIF通过其动态信任管理机制支持具有部分信任的互动主体的丰富生态系统。SCIF已经实现为Solidity的编译器。我们描述了SCIF语言，包括其静态检查规则和运行时。最后，我们实现了几个具有复杂安全性推理的应用程序，展示了SCIF如何支持构建复杂的安全智能合约，并为程序员提供有关潜在安全漏洞的准确诊断。

SCIF试图解决智能合约安全性的根本挑战，即如何构建与不受信任代码组合的安全软件，这是一个新问题。

SCIF是一种基于安全信息流的语言，通过动态信任管理机制支持互相信任的参与者。它不仅仅可以防止信息泄露，还可以防止重入攻击、混淆代理攻击和错误处理不当等问题。

论文详细介绍了SCIF语言的静态检查规则、运行时机制，并且实现了编译器到Solidity的转换。同时，论文还给出了一些复杂的安全性推理应用程序，证明了SCIF可以支持构建复杂的智能合约，并且能够准确诊断潜在的安全漏洞。

在智能合约安全性方面，最近的相关研究包括：(1) Mythril、Oyente、Securify等工具的开发；(2) 基于程序分析的智能合约安全性检测方法；(3) 基于形式化验证的智能合约安全性检测方法。