PrettyCat: Adaptive Guarantee-Driven Software Partitioning of Security Protocols
One single error can result in a total compromise of all security in today’s large, monolithic software.Simplifying the effort required to partition them into component-based systems with a minimal, trusted computing base would drastically ease code-review and verification, and lead to improved system security.
The goal of my research is to create a methodology to automatically partition cryptographic protocols while preserving their original security guarantees. So far, we developed a framework that enables us to model cryptographic protocols as processes interacting over message channels. A process is an instance of a cryptographic primitive. Each type of primitive has an associated specific set of rules which define the security guarantees assumed for a primitive’s inputs and outputs and their relationship.
Using a SAT solver, we can efficiently solve the rules for inter-connected primitives making up a cryptographic protocol. As a result, we can partition the network of primitives into domains with different security requirements. Applying this approach to both, simplified security protocols and the widely used Off-therecord messaging protocol OTR, shows that significant portions of the protocol can be realized with reduced guarantees. Our models can be executed to validate their interoperability with existing implementations. Furthermore, erroneous data flows are detected as contradictions in the model by the solver.