Title: Operational semantics for secure interoperation
Authors: Larmuseau, Adriaan
Patrignani, Marco
Clarke, Dave
Issue Date: 1-Aug-2014
Publisher: ACM
Host Document: Proceedings of the Ninth Workshop on Programming Languages and Analysis for Security pages:40-52
Series Title: PLAS
Conference: Workshop on Programming Languages and Analysis for Security edition:9 location:Uppsala date:1-08-2014
Abstract: 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.
Publication status: published
KU Leuven publication type: IC
Appears in Collections:Informatics Section

Files in This Item:
File Description Status SizeFormat
plas2014.pdf Published 499KbAdobe PDFView/Open


All items in Lirias are protected by copyright, with all rights reserved.