Previous work by Kang and Jackson proposed a modular framework for modeling implementation decisions involved when mapping a high-level design onto a low-level platform. Our recent work extends this framework in a number of ways. First, we formalize the notion of mapping composition, the key technical tool for composing formal models of a high-level design and a low-level execution platform, given a mapping capturing the implementation decisions. Second, we define the mapping synthesis problem: given a high-level model P, low-level model Q, and specification F, find a mapping M such that the mapping composition M(P,Q) satisfies F. Third, we present counter-example guided synthesis techniques to generate symbolic mappings automatically. Finally, we discuss two real-world case studies demonstrating the applicability of our technique to the synthesis of secure mappings for the popular web authorization protocols OAuth 1.0 and 2.0.
Stavros Tripakis is an Associate Professor at Northeastern University. He received his Ph.D. degree in Computer Science at the Verimag Laboratory, Joseph Fourier University, Grenoble, France, and has held positions at the University of California at Berkeley, at the French National Research Center CNRS, at Cadence Design Systems, and at Aalto University. His research interests are in the foundations of software and system design, computer-aided verification, and cyber-physical systems. Dr. Tripakis was co-Chair of the 10th ACM & IEEE Conference on Embedded Software (EMSOFT 2010), and Secretary/Treasurer (2009-2011) and Vice-Chair (2011-2013) of ACM SIGBED. His H-index is 47.