Operational Semantics for Secure Interoperation

Modern software systems are commonly programmed in multiple languages. Research into the security and correct-ness of such multi-language programs has generally relied on static methods that check both the individual compo-nents as well as the interoperation between them. In practice, however, components are sometimes linked in at run-time through malicious means. In this paper we introduce a tech-nique to specify operational semantics that securely combine an abstraction-rich language with a model of an arbitrary at-tacker, without relying on any static checks. The resulting operational semantics, instead, lifts a proven memory iso-lation mechanism into the resulting multi-language system. We establish the security benefits of our technique by prov-ing that the obtained multi-language system preserves and reflects the equivalences of the abstraction-rich language. To that end a notion of bisimilarity for this new type of multi-language system is developed