Formalizing a secure foreign function interface
2015 (English)In: Software Engineering and Formal Methods, Springer, 2015, 215-230 p.Conference paper (Refereed)
Many high-level functional programming languages provide programmers with the ability to interoperate with untyped and low-level languages such as C and assembly. Research into the security of such interoperation has generally focused on a closed world scenario, one where both the high-level and low-level code are defined and analyzed statically. In practice, however, components are sometimes linked in at run-time through malicious means. In this paper we formalize an operational semantics that securely combines MiniML, a light-weight ML, with a model of a low-level attacker, without relying on any static checks on the attacker. We prove that the operational semantics are secure by establishing that they preserve and reflect the equivalences of MiniML. To that end a notion of bisimulation for the interaction between the attacker and MiniML is developed.
Place, publisher, year, edition, pages
Springer, 2015. 215-230 p.
, Lecture Notes in Computer Science, ISSN 0302-9743 ; 9276
IdentifiersURN: urn:nbn:se:uu:diva-267089DOI: 10.1007/978-3-319-22969-0_16ISI: 000365046400016ISBN: 978-3-319-22968-3OAI: oai:DiVA.org:uu-267089DiVA: diva2:872009
13th International Conference on Software Engineering and Formal Methods (SEFM), September 7–11, York, UK