  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.
