SecRef*: Securely Sharing Mutable References Between Verified and Unverified Code in F*

Cezar-Constantin Andrici, Danel Ahman, Catalin Hritcu +4

We introduce SecRef*, a secure compilation framework protecting stateful programs verified in F* against linked unverified code, with which the program dynamically shares ML-style…