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

点击翻译按钮获取中文摘要

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.