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

使用sketchins实现可证明正确的高性能密码grastislav bodik本研究利用广泛使用的廉价并行硬件（如多媒体扩展、图形协处理器和即将推出的多核处理器）来显著提高密码性能。目标是(i)使安全性用于当前性能不允许的地方（例如对笔记本电脑和移动电话上的文件进行加密），以及（ii）简化在设计安全系统时所做的复杂的性能-安全性权衡。技术上的新奇之处在于用草图来实现密码。使用草图编程是高性能应用程序的一种半自动方法。草图是一种基于搜索的方法，它既简化了编程，又保证了最终实现的完全正确性。使用草图，程序员可以编写干净且可移植的参考代码，然后通过简单地勾画出所需实现的轮廓来获得高质量的实现。然后编译器会填补缺失的细节。通过搜索保证实现参考代码的草图的“完成”来填充细节。

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.