Formalizing a Secure Foreign Function Interface

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 \(\mathrm{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 \(\mathrm{MiniML}\). To that end a notion of bisimulation for the interaction between the attacker and \(\mathrm{MiniML}\) is developed.