arXiv 1801.018962018-01-05cs.PL

使用类型优化和综合恒定资源实现

Verifying and Synthesizing Constant-Resource Implementations with Types

Van Chan Ngo, Mario Dehesa-Azuara, Matthew Fredrikson, Jan Hoffmann

备注：: 30, IEEE S&P 2017

摘要：

我们提出了一种新的类型系统，用于验证程序正确实现恒定资源的行为。我们的类型系统扩展了最近的工作自动摊销资源分析（AARA），一组技术，自动推导出可证明的上限的资源消耗的程序。我们设计了新的技术，建立在潜在的方法，以实现组合性，精度和自动化。对于大多数实际应用程序来说，一个严格的全局要求，即程序总是保持恒定的资源使用，限制太多。对于只允许观察程序部分状态和行为的攻击者来说，要求程序的资源行为保持不变就足够了。为了说明这一点，我们的类型系统将信息流跟踪纳入其资源分析。这允许我们的系统在某些情况下验证需要违反恒定时间要求的程序，只要这样做不会将机密信息泄露给攻击者。我们正式通过定义一个新的概念，资源感知的不干扰，这种保证，并证明我们的系统强制执行it.Finally，我们展示了我们的类型推断算法可以用来合成一个恒定的时间实现，不能被验证为安全，有效地自动修复不安全的程序。我们还展示了如何计算资源使用的下限的第二种新的AARA系统，可以用来获得定量的信息量，通过其资源使用的程序泄漏的界限。我们在Resource Aware ML中实现了这些系统中的每一个，并表明它可以应用于验证许多应用程序中的恒定时间行为，包括加密和解密例程，数据库查询和其他资源感知功能。

英文摘要：

We propose a novel type system for verifying that programs correctly implement constant-resource behavior. Our type system extends recent work on automatic amortized resource analysis (AARA), a set of techniques that automatically derive provable upper bounds on the resource consumption of programs. We devise new techniques that build on the potential method to achieve compositionality, precision, and automation. A strict global requirement that a program always maintains constant resource usage is too restrictive for most practical applications. It is sufficient to require that the program's resource behavior remain constant with respect to an attacker who is only allowed to observe part of the program's state and behavior. To account for this, our type system incorporates information flow tracking into its resource analysis. This allows our system to certify programs that need to violate the constant-time requirement in certain cases, as long as doing so does not leak confidential information to attackers. We formalize this guarantee by defining a new notion of resource-aware noninterference, and prove that our system enforces it. Finally, we show how our type inference algorithm can be used to synthesize a constant-time implementation from one that cannot be verified as secure, effectively repairing insecure programs automatically. We also show how a second novel AARA system that computes lower bounds on resource usage can be used to derive quantitative bounds on the amount of information that a program leaks through its resource use. We implemented each of these systems in Resource Aware ML, and show that it can be applied to verify constant-time behavior in a number of applications including encryption and decryption routines, database queries, and other resource-aware functionality.

机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。

摘要：

英文摘要：

相关论文