Blockchains facilitate secure resource transactions through smart contracts, yet these digital agreements are prone to vulnerabilities, particularly when interacting with external contracts, leading to substantial monetary losses. Traditional verification techniques fall short in providing comprehensive security assurances, especially against re-entrancy attacks, due to the unavailable implementations of external contracts. This paper introduces an incremental approach: gradual verification. We combine static and dynamic verification techniques to enhance security, guarantee soundness and flexibility, and optimize resource usage in smart contract interactions. By implementing a prototype for gradually verifying Algorand smart contracts via the pyTEAL language, we demonstrate the effectiveness of our approach, contributing to the safe and efficient execution of smart contracts.

翻译：区块链通过智能合约促进安全的资源交易，然而这些数字协议容易存在漏洞，尤其是在与外部合约交互时，可能导致重大的经济损失。由于外部合约的实现不可获取，传统验证技术在提供全面的安全保障方面存在不足，特别是针对重入攻击。本文提出一种渐进式方法：渐进式验证。我们结合静态与动态验证技术来增强安全性，保证可靠性与灵活性，并优化智能合约交互中的资源使用。通过基于pyTEAL语言为Algorand智能合约实现渐进式验证的原型系统，我们证明了该方法的有效性，为智能合约的安全高效执行做出了贡献。