  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.
