PrettyCat: Adaptive guarantee-controlled software partitioning of security protocols

One single error can result in a total compromise of all security in today's large, monolithic software. Partitioning of software can help simplify code-review and verification, whereas isolated execution of software-components limits the impact of incorrect implementations. However, existing application partitioning techniques are too expensive, too imprecise, or involve unsafe manual steps. An automatic, yet safe, approach to dissect security protocols into component-based systems is not available. We present a method and toolset to automatically segregate security related software into an indefinite number of partitions, based on the security guarantees required by the deployed cryptographic building blocks. As partitioning imposes communication overhead, we offer a range of sound performance optimizations. Furthermore, by applying our approach to the secure messaging protocol OTR, we demonstrate its applicability and achieve a significant reduction of the trusted computing base. Compared to a monolithic implementation, only 29% of the partitioned protocol requires confidentiality guarantees with a process overhead comparable to common sandboxing techniques.