Operational Semantics for Secure Interoperation
2014 (English)In: Proceedings of the Ninth Workshop on Programming Languages and Analysis for Security, 2014Conference paper (Refereed)
Modern software systems are commonly programmed in multiple languages. Research into the security and correctness of such multi-language programs has generally relied on static methods that check both the individual components 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 technique to specify operational semantics that securely combine an abstraction-rich language with a model of an arbitrary attacker, without relying on any static checks. The resulting operational semantics, instead, lifts a proven memory isolation mechanism into the resulting multi-language system. We establish the security benefits of our technique by proving 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.
Place, publisher, year, edition, pages
bisimulation, fully abstract compilation, memory protection
Research subject Computer Science
IdentifiersURN: urn:nbn:se:uu:diva-234648ISBN: 978-1-4503-2862-3OAI: oai:DiVA.org:uu-234648DiVA: diva2:757389
ACM Ninth Workshop on Programming Languages and Analysis for Security (PLAS 2014), Uppsala, Sweden