Refinement Types for Secure Implementations
Refinement Types for Secure Implementations
复制标题
DOI：
10.1145/1890028.1890031
复制
发表时间：
2011-01-01
影响因子：
1.3
通讯作者：
Maffeis, Sergio
中科院分区：
文献类型：
--
作者：
Bengtson, Jesper;Bhargavan, Karthikeyan;Maffeis, Sergio
我们提出了一个类型检查器的设计和实现，用于验证密码协议和访问控制机制的源代码的安全属性。底层类型理论是一种带有精化类型的微积分，用于表达一阶逻辑中的前置和后置条件。我们推导出正式的密码原语，并在类型论中表示活跃的对手。良好类型的程序享有基于断言的安全属性，相对于一个现实的威胁模型，包括关键妥协。该实现相当于通用函数语言F-#的增强型类型检查器;类型检查生成传递给SMT求解器的验证条件。我们描述了一系列检查的例子。这是第一个通过对加密协议的源代码进行类型检查来验证其身份验证属性的工具。
We present the design and implementation of a typechecker for verifying security properties of the source code of cryptographic protocols and access control mechanisms. The underlying type theory is a lambda-calculus equipped with refinement types for expressing pre- and post-conditions within first-order logic. We derive formal cryptographic primitives and represent active adversaries within the type theory. Well-typed programs enjoy assertion-based security properties, with respect to a realistic threat model including key compromise. The implementation amounts to an enhanced typechecker for the general-purpose functional language F-#; typechecking generates verification conditions that are passed to an SMT solver. We describe a series of checked examples. This is the first tool to verify authentication properties of cryptographic protocols by typechecking their source code.