A Framework for Composing Noninterferent Languages

Software is frequently implemented using multiple specialized languages for different tasks. Security type systems, one technique to secure software, have previously only been studied for programs written entirely in a single language. We present a framework that facilitates reasoning over composite languages. In it, guarantees of sufficiently related component languages can be lifted to the composed language. This can significantly lower the burden necessary to certify that such composite programs are safe. Our simple but powerful approach relies, at its core, on computability and security-level separability. Besides non-interference, we also show how the framework can accommodate notions of declassification. To demonstrate the applicability of this framework, we show that a standard secure while language from the literature satisfies all necessary requirements of a composition host, and sketch how to securely embed an expressive fragment of SQL.