# Automated Synthesis of Secure Platform Mappings

## TL;DR

This paper presents a formal method for automatically synthesizing platform mappings that preserve security properties from high-level designs to low-level implementations, demonstrated through real-world web protocol case studies.

## Contribution

It introduces the problem of property-preserving platform mapping synthesis, formalizes it, and proposes a symbolic constraint search technique with a prototype implementation.

## Key findings

- Successfully synthesized secure mappings for OAuth protocols.
- Demonstrated the approach on real-world web authorization protocols.
- Validated the effectiveness of the symbolic constraint search method.

## Abstract

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.