Automated Synthesis of Secure Platform Mappings
This addresses the challenge of ensuring secure implementations from high-level designs, particularly for web authorization protocols, though it appears incremental as it builds on existing formalization and synthesis methods.
The paper tackles the problem of synthesizing property-preserving platform mappings to prevent undesirable behavior in system implementations, and presents a technique based on symbolic constraint search, demonstrated with a real-world case study on OAuth 1.0 and 2.0 protocols.
System development often involves decisions about how a high-level design is to be implemented using primitives from a low-level platform. Certain decisions, however, may introduce undesirable behavior into the resulting implementation, possibly leading to a violation of a desired property that has already been established at the design level. In this paper, we introduce the problem of synthesizing a property-preserving platform mapping: A set of implementation decisions ensuring that a desired property is preserved from a high-level design into a low-level platform implementation. We provide a formalization of the synthesis problem and propose a technique for synthesizing a mapping based on symbolic constraint search. We describe our prototype implementation, and a real-world case study demonstrating the application of our technique to synthesizing secure mappings for the popular web authorization protocols OAuth 1.0 and 2.0.