CT-ISG: Implementing Provably Correct High-Performance Ciphers with Sketching

CT-ISG：通过草图实现可证明正确的高性能密码

• 批准号: 0524815
• 负责人: Rastislav Bodik
• 金额: $ 45万
• 依托单位: University of California-Berkeley
• 依托单位国家: 美国
• 项目类别: Standard Grant
• 财政年份: 2005
• 资助国家: 美国
• 起止时间: 2005-10-01 至 2008-09-30
• 项目状态: 已结题
• 来源: https://www.nsf.gov/awardsearch/showAward?AWD_ID=0524815&HistoricalAwards=false
• 关键词: CT; ISG; Implementing; Provably; Correct

NSF 0524815Implementing Provably Correct High-Performance Ciphers with SketchingRastislav BodikThis research exploits widespread inexpensive parallel hardware ---such as multimedia extensions, graphics co-processors, and upcoming multi-core processors --- for dramatic improvements in cipher performance. The goal is to (i) make security used where performance currently prohibits it (such as encrypting files on laptops and cell phones) and (ii) simplify the complex performance-security tradeoffs made in designing secure systems.The technical novelty is to implement ciphers with sketching. Programming with sketches is a semi-automatic approach for high-performance applications. Sketching is a search-based approach that both simplifies programming and guarantees full correctness of the resulting implementation. With sketching, programmers write clean and portable reference code, and then obtain a high-quality implementation by simply sketching an outline of the desired implementation. The compiler then fills in the missing detail. The detail is filled in by searching for such "completions'' of the sketch that are guaranteed to implement the reference code.

NSF 0524815用草图实现可证明正确的高性能密码Rastislav Bodik这项研究利用了广泛使用的廉价并行硬件-如多媒体扩展、图形协处理器和即将推出的多核处理器-来显著提高密码性能。其目标是（i）使安全性用于目前性能不允许的地方（例如加密笔记本电脑和手机上的文件），（ii）简化设计安全系统时复杂的性能-安全性权衡。使用草图编程是一种用于高性能应用程序的半自动方法。 草图是一种基于搜索的方法，既简化了编程，又保证了最终实现的完全正确性。有了草图，程序员可以编写干净和可移植的参考代码，然后通过简单地绘制所需实现的轮廓来获得高质量的实现。 然后，编译器填充缺少的详细信息。通过搜索保证实现参考代码的草图的“完成”来填充细节。