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

University Of California-Berkeley, Berkeley CA

Investigators

Abstract

NSF 0524815 Implementing Provably Correct High-Performance Ciphers with Sketching Rastislav Bodik This 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.