随着区块链的快速发展,智能合约作为区块链的核心技术受到广泛关注。但频繁发生的智能合约漏洞事件,在造成巨大经济损失的同时,也使智能合约陷入信任危机。如何确保合约的安全性成为亟待研究的问题。智能合约从需求分析到代码实现的过程中,需要经过严格的数学推理验证,使用模型检测方法可以确保合约需求的安全性;为检测以太坊上的智能合约源代码是否在执行时是安全、可靠的,也可以借助模型检测方法,反向进行安全漏洞的检测。因此,本文采用模型检测方法,基于合约需求和合约源代码两个角度,重点研究区块链智能合约安全的正向和逆向模型检测方法。主要工作内容如下:1)为检测合约需求中出现的漏洞问题,提出区块链智能合约安全的正向模型检测方法。建立正向分析框架,以此为基础结合角色访问控制（Role-based access control,RBAC）案例进行详细分析。通过剖析合约案例需求,抽象出合约的逻辑角色及操作算子,得出合约角色及系统间的信息交互,并对其进行形式化描述;引入模型检测技术构建Organization、Thirdparty、Schoolperson和System模型,利用时序逻辑公式表述合约案例的可靠性、功能属性、时效性和唯一性,使用UPPAAL工具对所刻画的性质进行验证。验证结果表明利用正向检测方法可以检测出合约需求所满足的安全性质,能够避免合约代码编写漏洞的出现。2)以太坊上的智能合约大部分仅存在合约源代码,正向检测方法无法实现分析及建模,因此,提出智能合约安全的逆向模型检测方法。建立逆向分析框架,有效改进检测方法与流程,更加适用于智能合约的普遍情况,并结合投票合约案例进行了详细分析。通过对以太坊智能合约源代码的功能分析和逻辑分析,提取合约逻辑流程;若发现合约案例中存在如整数溢出和二次委托等漏洞,对其进行漏洞修复,形式化描述性质、对象和事件;使用时间自动机构建Voter、Chairperson、Proposal和Sys模型,通过对可靠性、完整性、功能属性、时效性、唯一性等性质的检测,验证所提方法能够有效检测出投票合约系统的安全漏洞。