Automated synthesis of secure platform mappings

DOI10.1007/978-3-030-25540-4_12MaRDI QIDQ6194575zbMATH OpenOpenAlexFDO

Authors Eunsuk Kang, Stéphane Lafortune, Stavros Tripakis

Publication date 16 February 2024

Published in Computer Aided Verification (Search for Journal in Brave)

Copyright license Creative Commons Attribution 4.0 International

Full work available at URL https://arxiv.org/abs/1705.03618

Mathematics Subject Classification ID

Specification and verification (program logics, model checking, etc.) (68Q60)

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.

Recommendations

• Program synthesis for interactive-security systems
• Synthesis of Trigger Properties
• Implementation issues about the embedding of existing high level synthesis algorithms in HOL
• Compositional strategy mapping
• Shield synthesis: runtime enforcement for reactive systems

This page was built for publication: Automated synthesis of secure platform mappings

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q6194575)