Reference 1
Reference 1 RUST ——–buffer——–> Ocaml <——————— Escape Hatches: ML:C FFI Rust:unsafe Java: JNI All type soundness(safety) guarranttes are gone. Instead, use Principled FFIs: ML: linear types. Linking types: support safe initeroperability with other languages. Only need linking types extensions to interact with behavior/features inexpressible in your language. SNAPL’172: Linking Types for Multi-language Software: Have your cake eat it too. Teach Ocaml with ownership in Rust: Linking Type: linear type: cannot keep it and give it away at the same time.
Reference 1 A type system for expressive security policies. POPL, 2000. ↩
Reference 1 Language-based information-flow security. IEEE journal on selected areas in comm. 2003. ↩
If you could revise
the fundmental principles of
computer system design
to improve security...
... what would you change?